Proposal: containerized cross-platform dev environment (realizes the SPEC-030-A container/BYO-key client)

[thedavidyoungblood]

Proposal: a containerized cross-platform dev environment (additive DevX)

Hi — first, thanks for unsorry; the kernel-as-oracle + repo-as-infrastructure design is great to study.

I'd like to propose an additive development container and check whether it's wanted before opening a
PR. I have a working, validated proof-of-concept ready.

The gap

main currently ships no dev-environment tooling (no Dockerfile, .devcontainer, Nix, or Makefile),
and CONTRIBUTING.md lists the toolchain prerequisites without any OS guidance. The swarm is a POSIX/bash
pipeline, so the practical baseline is "bring your own Linux/WSL2" — which works, but new contributors
(especially on Windows/macOS) are left to assemble and match the CI environment themselves. Concretely,
./swarm/agent.sh --self-test fails on a native Windows shell purely on text handling (CRLF / sort-locale),
which reads as breakage even though the logic is fine.

This is exactly the "container / BYO-key client that makes 'more users' practical" that
SPEC-030-A already names as an onboarding goal — so this proposal aims to realize that, scoped to the
development/verification environment.

What it is

A repo-agnostic dev container that mirrors the environment Gate A trusts in CI (Ubuntu + elan-pinned Lean +
mathlib binary cache + Python 3 + gh):

• Dockerfile — Docker-first and OCI-portable, so it runs unchanged under Podman. Non-root user.
• docker-compose.yml — bind-mounts the repo at /workspace, persists .lake in a named volume.
• .devcontainer/devcontainer.json — reuses the same compose for VS Code Dev Containers.
• docs/dev/containerized-development.md — a Docker / Podman / Dev Containers runbook.
• an advisory, path-filtered devcontainer-smoke CI job that builds the image and runs the mathlib-free
  checks inside it (it deliberately does not run the mathlib build / Gate A — that stays in gate-a).

Guarantees: no change to Gate A, Gate B, the claims substrate, AISP records, or agent behaviour — DevX
only. The image is repo-agnostic (no sources baked in; elan honours the mounted repo's lean-toolchain,
so a toolchain bump needs no image change) and secret-free (credentials at runtime only; mathlib via the
binary cache, never built from source — per ADR-002).

Validated

Built and run end-to-end on Podman 5.8.3 (WSL2), repo bind-mounted:

• ./swarm/agent.sh --self-test → all 67 pass (vs. the native-Windows text-handling failures above — the
  Linux userland is the fix).
• lake build UnsorryLibrary --wfail → builds clean (mathlib via lake exe cache get).
• python3 -m tools.gate_b validate . → exit 0.
• python3 -m pytest tools -q → 486 passed / 2 skipped, with one timing test (...100_times_under_one_second)
  failing only under slow 9p bind-mount I/O on Windows; it passes on a native Linux FS (i.e. CI).

Honest scoping

• This is the dev/verify environment, not yet the full BYO-key proving client — it intentionally does
  not bundle a proof provider (Claude Code / keys stay BYO at runtime). It's the foundation toward SPEC-030-A,
  not the finished thing.
• I've prepared it to fit the project's conventions: a paired ADR-065 + SPEC-065-A (numbered against
  current main, which ends at ADR-064), a changelog fragment, a single feature/ branch / one logical change.
  I recognize a DevX PR sits outside the three documented contribution paths and that .github/ is
  CODEOWNERS-reviewed — hence asking first.

PoC artifacts

The actual files (Dockerfile, compose, devcontainer, runbook, ADR-065, SPEC-065-A, CI job, changelog
fragment) are here for inspection: https://gist.github.com/thedavidyoungblood/d57937ebaac179da768dce873171dfa6

The ask

• Is a containerized dev environment something you'd welcome?
• If so, do you prefer the full set above, or a leaner first cut (e.g. Dockerfile + compose +
  runbook, with the devcontainer/CI as follow-ups)? I'm happy to match whatever scope and conventions you prefer.
• On your go, I'll open a PR (the branch is ready) — or adapt it however you'd like first.

Thanks for considering it!