unsorry: containerized cross-platform dev environment — PoC for an additive DevX proposal (Docker-first, Podman-compatible; validated Gate A/B + self-test 67/67)

00-README.md

unsorry — containerized cross-platform dev environment (PoC artifacts)

Proof-of-concept for a proposal to agenticsnz/unsorry: an additive, reproducible dev container that mirrors the environment Gate A trusts in CI (Ubuntu + elan-pinned Lean + mathlib binary cache + Python + gh). Docker-first, runs unchanged under Podman.

These files are validated end-to-end (build + Gate A --wfail + Gate B + agent.sh --self-test 67/67) on Podman/WSL2. They are shared here for inspection — happy to open a proper PR on request. Additive DevX only: no change to Gate A, Gate B, the claims substrate, AISP records, or agent behaviour. The image bakes in no repository sources and no secrets.

File → repo-path manifest

Gist filenames are flattened (gists are a flat namespace); the intended repo locations are:

Gist file	Repo destination
Dockerfile	Dockerfile
docker-compose.yml	docker-compose.yml
dockerignore	.dockerignore
devcontainer.json	.devcontainer/devcontainer.json
containerized-development.md	docs/dev/containerized-development.md
ADR-065-Containerized-Cross-Platform-DevX.md	docs/adrs/ADR-065-Containerized-Cross-Platform-DevX.md
SPEC-065-A-Containerized-DevX.md	docs/adrs/specs/SPEC-065-A-Containerized-DevX.md
devcontainer-smoke.yml	.github/workflows/devcontainer-smoke.yml
changelog__added-containerized-devx-adr065.md	changelog.d/added-containerized-devx-adr065.md

ADR/SPEC numbered 065 against current main (the live set ends at ADR-064). Re-checked if upstream advances. The .github/ workflow is CODEOWNERS-reviewed by design.

ADR-065-Containerized-Cross-Platform-DevX.md

ADR-065: Containerized Cross-Platform Development Environment

Field	Value
Decision ID	ADR-065
Initiative	unsorry contributor onboarding & cross-platform DevX
Proposed By	unsorry contributors
Date	2026-06-17
Status	Proposed

WH(Y) Decision Statement

In the context of a swarm whose proof loop is a POSIX/bash pipeline (elan, lake, gh, coreutils, locale-sensitive sort/tr) that Gate A verifies under a specific Ubuntu + pinned-Lean + mathlib-binary-cache environment in CI, and a stated onboarding goal of "the container / BYO-key client that makes 'more users' practical" (SPEC-030-A), facing contributors on Windows and macOS for whom installing the toolchain natively is friction and, on native Windows shells, actively broken — swarm/agent.sh --self-test fails on text handling (CRLF, sort locale) despite correct logic — which both blocks onboarding and produces misleading "it's broken" signals, we decided for an additive, repo-agnostic development container — a root Dockerfile (Ubuntu + elan + Python 3 + gh, non-root dev user), a docker-compose.yml that bind-mounts the repo at /workspace and persists .lake in a named volume, a .devcontainer/ that reuses the same compose, and a docs/dev/containerized-development.md runbook — that is Docker-first and OCI-portable so it runs unchanged under Podman, bakes in no repo sources and no secrets (the toolchain mechanism only; elan honours the mounted repo's lean-toolchain; credentials are injected at runtime), and is smoke-tested in CI, and neglected baking the repo and a fixed toolchain into the image (goes stale on every toolchain bump and bloats layers), committing a Nix/devbox environment (heavier adoption curve than the container the roadmap already names), a Windows-native support effort (fights the loop's POSIX assumptions for no soundness gain), and shipping separate hand-maintained Docker and Podman definitions (DRY violation — one OCI file serves both), to achieve a one-command, reproducible environment that matches the CI soundness bar on any host, so a new contributor can build the library, run both gates, author proofs with --prove-local, and run the loop without polluting their machine, accepting that this adds container files to the repo root and a CI smoke job (a .github/ change, so CODEOWNERS-reviewed), that the first build downloads the toolchain and mathlib cache (slow once, then cached in the volume), and that the image changes nothing about Gate A, Gate B, the claims substrate, or any coordination artifact — it is developer experience only, not a soundness or protocol change.

References

Reference ID	Title	Type	Location
REF-1	Containerized DevX implementation & smoke contract	Specification	specs/SPEC-065-A-Containerized-DevX.md
REF-2	Lean 4 + mathlib4 pinned to release tags (never build mathlib from source)	Decision	ADR-002-Lean4-Mathlib-Pinned-Release-Tags.md
REF-3	Domain-agnostic distributed-workload engine (names the container/BYO-key client)	Specification	specs/SPEC-030-A-Distributed-Workload-Engine.md
REF-4	Gate A soundness enforcement (the environment the container mirrors)	Decision	ADR-006-Gate-A-Soundness-Enforcement.md
REF-5	CI supply-chain & workflow protection (CODEOWNERS)	Decision	ADR-019-CI-Supply-Chain-Protection.md

Status History

Status	Approver	Date
Proposed	unsorry contributors	2026-06-17

changelog__added-containerized-devx-adr065.md

Added a containerized cross-platform development environment (ADR-065 / SPEC-065-A): a repo-root Dockerfile, docker-compose.yml, .devcontainer/, .dockerignore, and a contributor runbook. It mirrors the Ubuntu + elan-pinned-Lean + mathlib-binary-cache + Python + gh environment Gate A trusts in CI, so contributors on Linux, macOS, or Windows can build the library, run both gates, author proofs with --prove-local, and run the agent loop with one command and nothing installed on the host. Docker-first and OCI-portable (runs unchanged under Podman); the image bakes in no repository sources and no secrets. Resolves the native-Windows agent-loop self-test failures (CRLF / sort-locale text handling) by providing a Linux userland. A devcontainer-smoke CI job builds the image and runs the mathlib-free checks inside it. Additive DevX only — no change to Gate A, Gate B, the claims substrate, or any coordination artifact.

containerized-development.md

Containerized Development (Docker / Podman / Dev Containers)

A reproducible, cross-platform dev environment for unsorry that mirrors the environment Gate A trusts in CI (.github/workflows/gate-a.yml): Ubuntu + elan-pinned Lean toolchain + mathlib binary cache + Python 3 + gh. Use it to build the library, run both gates, author proofs locally, and run the agent loop — on Linux, macOS, or Windows — without installing the toolchain on your host.

Motivation: SPEC-030-A names "the container / BYO-key client that makes 'more users' practical" as an onboarding goal. This is that client. It is additive DevX — it changes no gate, soundness rule, or coordination artifact.

TL;DR

# from the repo root
docker compose up -d --build          # build image + start an idle dev container
docker compose exec dev bash          # drop into the container shell (user: dev, /workspace)

# inside the container — the preflight smoke test:
lake exe cache get                    # pull mathlib BINARY cache (never builds it — ADR-002)
lake build UnsorryLibrary --wfail     # Gate A strictness bar
python3 -m tools.gate_b validate . --at "$(date -u +%Y-%m-%dT%H:%M:%SZ)"   # Gate B
python3 -m pytest tools -q            # tooling suite
./swarm/agent.sh --self-test          # agent-loop self-tests

All green ⇒ your environment matches CI and you can author proofs (--prove-local) or run the loop.

Why a container

The toolchain is POSIX-shaped (bash agent loop, elan/lake, gh, coreutils, sort/tr semantics). On native Windows shells the agent self-test fails on text handling (CRLF, sort locale) even though the logic is correct — so the loop needs a Linux userland. A container gives every contributor that identical Linux userland, pinned to the same Lean/mathlib the kernel verifies against, with one command and nothing installed on the host.

Engines

This setup is Docker-first and OCI-portable; it runs unchanged under Podman.

Docker

docker compose up -d --build
docker compose exec dev bash

Podman

Podman reads the same Dockerfile and docker-compose.yml:

podman compose up -d --build      # or: podman-compose up -d --build
podman compose exec dev bash

• Windows/macOS: Podman runs containers inside a managed VM. Start it first: podman machine init (once) then podman machine start. The WSL2 backend shares host RAM dynamically, which Gate A's kernel replay appreciates.
• Rootless Podman + bind mounts: if mounted files look root-owned, build with host id mapping: podman build --build-arg UID=$(id -u) --build-arg GID=$(id -g) -t unsorry-dev .

VS Code Dev Containers

Open the folder and "Reopen in Container" (uses .devcontainer/devcontainer.json, which reuses this compose file). For Podman, set the Dev Containers extension's Docker Path to podman.

What the image is (and isn't)

• Is: Ubuntu 24.04 + elan (pre-warmed with the current pinned toolchain) + Python 3.12 + git + gh, running as a non-root dev user.
• Isn't: it does not bake in the repo, mathlib, or any secret. The repo is bind-mounted at /workspace at runtime, so host edits are live and the image stays generic and never goes stale on a toolchain bump — elan installs whatever lean-toolchain the mounted repo pins.
• Persistence: a named volume holds /workspace/.lake, so the mathlib binary cache and library oleans survive container restarts (fast subsequent builds).

Authoring proofs locally

Inside the container (see CONTRIBUTING.md for the full loop):

./swarm/agent.sh --prove-local --goal <id> --dry-run    # plan only, no model spend
./swarm/agent.sh --prove-local --goal <id>              # real attempt, no claim/PR

--prove-local verifies on your machine without touching the shared claims branch or opening a PR — the recommended way to experiment.

Going live (claims / PRs)

Live operation needs credentials, which are never baked into the image:

# pass secrets at RUNTIME only — e.g. an .env file the container reads:
docker compose --env-file .env up -d        # .env is git-ignored; see .env.example
docker compose exec dev gh auth login        # or mount an existing gh auth

Set UNSORRY_SOLVER, provider keys (OPENAI_API_KEY/OPENAI_BASE_URL for OpenAI-compatible endpoints), etc. via the environment — see CONTRIBUTING.md and the agent's --help.

Memory & performance

• The full Gate A axiom audit / kernel replay (leanchecker) holds a mathlib image resident (several GB). Give the engine adequate RAM (Docker Desktop / podman machine settings; WSL2 shares host RAM automatically).
• First lake exe cache get downloads the mathlib cache (network + a few GB); subsequent runs reuse the .lake volume.
• Never let lake build compile mathlib from source — if it does, the cache fetch failed; fix that first (ADR-002).

Troubleshooting

Symptom	Cause	Fix
lake build compiling mathlib	cache miss	re-run lake exe cache get; check network
mounted files root-owned (Podman)	rootless id map	rebuild with --build-arg UID/GID
podman compose not found	older Podman	use podman-compose, or upgrade Podman
replay OOM	engine RAM too low	raise Docker/Podman memory; ensure mathlib is cached not building
slow first build	toolchain + cache download	expected once; the .lake volume makes reruns fast

Cleanup

docker compose down            # stop + remove the container (keeps volumes)
docker compose down -v         # also remove the .lake cache volume

devcontainer-smoke.yml

name: devcontainer-smoke

# Advisory DevX check (ADR-065 / SPEC-065-A): proves the development image BUILDS
# and that the mathlib-free checks pass INSIDE it. It deliberately does NOT run the
# full mathlib build or Gate A replay — that cost stays in the gate-a workflow; this
# only validates the *environment*. Touches .github/, so it is CODEOWNERS-reviewed
# (ADR-019). Uses the docker CLI directly (no third-party build action) to keep the
# supply-chain surface minimal.

on:
  pull_request:
    paths:
      - 'Dockerfile'
      - 'docker-compose.yml'
      - '.dockerignore'
      - '.devcontainer/**'
      - 'docs/dev/containerized-development.md'
      - '.github/workflows/devcontainer-smoke.yml'
  push:
    branches: [main]
    paths:
      - 'Dockerfile'
      - 'docker-compose.yml'
      - '.dockerignore'
      - '.devcontainer/**'
      - '.github/workflows/devcontainer-smoke.yml'

permissions:
  contents: read

concurrency:
  group: devcontainer-smoke-${{ github.event.pull_request.number || github.ref }}
  cancel-in-progress: true

jobs:
  smoke:
    runs-on: ubuntu-latest
    timeout-minutes: 20
    steps:
      - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3

      - name: Build dev image
        run: docker build -t unsorry-dev:ci .

      - name: Sterilization scan (no secrets/identifiers in DevX artifacts)
        run: |
          set -euo pipefail
          files="Dockerfile docker-compose.yml .dockerignore .devcontainer docs/dev/containerized-development.md .github/workflows/devcontainer-smoke.yml"
          # No private keys, tokens, or absolute host paths baked into DevX files.
          if grep -RInE '(BEGIN [A-Z ]*PRIVATE KEY|ghp_[A-Za-z0-9]{20,}|sk-[A-Za-z0-9]{20,}|[A-Za-z]:\\\\Users\\\\)' $files; then
            echo "::error::potential secret or absolute host path in DevX artifacts"; exit 1
          fi
          echo "sterilization scan clean"

      - name: Mathlib-free checks inside the container
        run: |
          set -euo pipefail
          docker run --rm -v "$PWD:/workspace" -w /workspace unsorry-dev:ci bash -lc '
            set -euo pipefail
            python3 -m tools.gate_b validate . --at "$(date -u +%Y-%m-%dT%H:%M:%SZ)"
            python3 -m pytest tools -q
            ./swarm/agent.sh --self-test
          '

devcontainer.json

{
  "// about": "VS Code / Dev Containers config — reuses the repo-root docker-compose.yml so the editor, terminal, and CLI all share one toolchain definition. Docker-first; works under Podman (set the Dev Containers 'Docker Path' to 'podman').",
  "name": "unsorry-dev",
  "dockerComposeFile": ["../docker-compose.yml"],
  "service": "dev",
  "workspaceFolder": "/workspace",
  "remoteUser": "dev",
  "overrideCommand": false,
  "// postCreate": "Pull the mathlib binary cache once (never builds mathlib from source — ADR-002). Safe to re-run.",
  "postCreateCommand": "lake exe cache get || true",
  "customizations": {
    "vscode": {
      "extensions": [
        "leanprover.lean4",
        "ms-python.python"
      ],
      "settings": {
        "lean4.toolchainPath": "/home/dev/.elan"
      }
    }
  }
}

docker-compose.yml

# unsorry — development container compose (Docker-first; Podman-compatible)
#
#   Docker:  docker compose up -d && docker compose exec dev bash
#   Podman:  podman compose up -d && podman compose exec dev bash
#            (or: podman-compose up -d && podman-compose exec dev bash)
#
# Placed at the repo root, the bind mount `.:/workspace` mounts the project into
# the container. Nothing is copied into the image, so edits on the host are live
# inside the container and no sources are baked into a layer.
services:
  dev:
    build:
      context: .
      dockerfile: Dockerfile
      args:
        # Pre-warm hint; elan still honours the mounted repo's lean-toolchain.
        LEAN_TOOLCHAIN: ${LEAN_TOOLCHAIN:-leanprover/lean4:v4.30.0}
    image: unsorry-dev:local
    working_dir: /workspace
    volumes:
      # The repository. Use :ro for read-only research; :rw to author proofs.
      - .:/workspace:rw
      # Persist the mathlib BINARY cache + library oleans across runs so
      # `lake exe cache get` / `lake build` are fast after the first time.
      # (Overlays the host .lake, which is git-ignored anyway.)
      - unsorry-lake:/workspace/.lake
    environment:
      # Sensible defaults; override via the shell or an --env-file (see runbook).
      - UNSORRY_PROVIDER=${UNSORRY_PROVIDER:-claude}
      - UNSORRY_MODEL=${UNSORRY_MODEL:-}
      - UNSORRY_EFFORT=${UNSORRY_EFFORT:-}
    # Keep an idle shell alive so you can `exec` into it.
    command: ["sleep", "infinity"]
    tty: true
    stdin_open: true

volumes:
  unsorry-lake:

Dockerfile

# syntax=docker/dockerfile:1
# ─────────────────────────────────────────────────────────────────────────────
# unsorry — cross-platform development container (Docker-first; Podman-compatible)
#
# Mirrors the environment Gate A trusts in CI (.github/workflows/gate-a.yml):
#   Ubuntu + elan-pinned Lean toolchain + mathlib BINARY cache + Python 3 + gh.
# The image is REPO-AGNOSTIC: it ships the toolchain *mechanism* only. The repo is
# bind-mounted at runtime (see docker-compose.yml), and elan installs whatever
# `lean-toolchain` the mounted repo pins — so this image never goes stale on a
# toolchain bump and never bakes project sources or secrets into a layer.
#
# Build (Docker):  docker build -t unsorry-dev .
# Build (Podman):  podman build  -t unsorry-dev .     # reads this Dockerfile natively
# ─────────────────────────────────────────────────────────────────────────────
FROM ubuntu:24.04

# Pre-warm the common toolchain (overridable). elan still auto-installs whatever
# the mounted repo's lean-toolchain pins, so this is a speed hint, not a lock.
ARG LEAN_TOOLCHAIN=leanprover/lean4:v4.30.0
# Non-root by default; override to map host UID/GID on Linux for clean file perms.
ARG USER=dev
ARG UID=1000
ARG GID=1000

ENV DEBIAN_FRONTEND=noninteractive \
    LANG=C.UTF-8 \
    LC_ALL=C.UTF-8 \
    ELAN_HOME=/home/${USER}/.elan \
    PATH=/home/${USER}/.elan/bin:/home/${USER}/.local/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin

# --- system deps: matches what lean-action + the tooling need ---------------
#   git, curl, ca-certificates  → fetch toolchain + mathlib cache, run gh
#   build-essential             → linker/libc for Lean native steps
#   python3 (3.12 on 24.04)     → Gate B validator + tools/ (stdlib-only)
#   gh                          → only needed for LIVE operation (PRs/claims)
RUN apt-get update && apt-get install -y --no-install-recommends \
        ca-certificates curl git build-essential \
        python3 python3-venv python3-pip python-is-python3 \
        python3-pytest python3-requests \
        passwd adduser unzip jq \
    && install -d -m 0755 /etc/apt/keyrings \
    && curl -fsSL https://cli.github.com/packages/githubcli-archive-keyring.gpg \
        -o /etc/apt/keyrings/githubcli-archive-keyring.gpg \
    && chmod go+r /etc/apt/keyrings/githubcli-archive-keyring.gpg \
    && echo "deb [arch=$(dpkg --print-architecture) signed-by=/etc/apt/keyrings/githubcli-archive-keyring.gpg] https://cli.github.com/packages stable main" \
        > /etc/apt/sources.list.d/github-cli.list \
    && apt-get update && apt-get install -y --no-install-recommends gh \
    && rm -rf /var/lib/apt/lists/*

# --- non-root dev user ------------------------------------------------------
# Ubuntu 24.04 ships a stock uid-1000 `ubuntu` user. Remove it so `dev` can own
# uid/gid 1000 cleanly (override UID/GID at build time to match a Linux host for
# rootless bind-mount ownership). Fallbacks keep the build green if 1000 is busy.
RUN if getent passwd ${UID} >/dev/null; then \
        userdel -r "$(getent passwd ${UID} | cut -d: -f1)" 2>/dev/null || true; \
    fi; \
    groupadd -g ${GID} ${USER} 2>/dev/null || groupadd ${USER}; \
    useradd -m -u ${UID} -g ${USER} -s /bin/bash ${USER} 2>/dev/null \
        || useradd -m -g ${USER} -s /bin/bash ${USER}; \
    getent passwd ${USER} >/dev/null   # fail the build if the user wasn't created
USER ${USER}
WORKDIR /workspace

# --- elan + pinned toolchain (as the dev user) ------------------------------
RUN curl -fsSL https://elan.lean-lang.org/elan-init.sh \
        | sh -s -- -y --default-toolchain "${LEAN_TOOLCHAIN}" \
    && elan --version && lean --version && lake --version

# Repo is bind-mounted here at runtime; nothing is COPYed in (keeps the image
# generic + sterile). First `lake exe cache get` pulls the mathlib binary cache
# into the persisted .lake volume — never builds mathlib from source (ADR-002).
CMD ["bash"]

dockerignore

# Build context exclusions for the dev image.
# The image COPYs nothing (repo is bind-mounted at runtime), so this mainly keeps
# the build context small/fast and guarantees no local state or secrets are ever
# sent to the builder.
.git
.lake
**/.lake
__pycache__/
**/__pycache__/
*.py[cod]
.pytest_cache/

# Secrets / local env — never into a build context or an image layer.
.env
**/.env
*.local
prove-attempt-*.log

# Editor / OS noise
.vscode/
.idea/
.DS_Store
Thumbs.db

SPEC-065-A-Containerized-DevX.md

SPEC-065-A: Containerized Cross-Platform DevX

Implements: ADR-065 · Also honours ADR-002, ADR-019 · Status: Living · Updated: 2026-06-17

Scope: an additive developer-experience container. It introduces no change to Gate A, Gate B, the claims substrate, AISP records, or any agent behaviour. Everything below is verifiable from the artifacts and the CI smoke job.

Artifacts (repo-root placement)

Path	Purpose
Dockerfile	Canonical OCI image definition (Docker + Podman read it). Ubuntu + elan + Python 3 + gh, non-root dev user.
docker-compose.yml	Bind-mounts the repo at /workspace; persists .lake in a named volume; idle shell.
.dockerignore	Keeps the build context minimal; excludes .git, .lake, __.ignore*, .env, logs.
.devcontainer/devcontainer.json	VS Code Dev Containers config; reuses docker-compose.yml.
docs/dev/containerized-development.md	Contributor runbook (Docker / Podman / Dev Containers).
.github/workflows/devcontainer-smoke.yml	CI smoke test that the image builds and the no-mathlib checks pass inside it.

Image contract

1. Repo-agnostic. The image MUST NOT COPY/ADD repository sources. The repo is bind-mounted at runtime. (Keeps the image generic and prevents source/secret bake-in.)
2. Secret-free. No credential, token, key, email, or personal identifier appears in any image layer, Dockerfile, or compose file. Credentials are supplied only at runtime (environment / --env-file / mounted auth).
3. Toolchain mechanism, not lock. elan is installed; the default toolchain is a pre-warm hint (ARG LEAN_TOOLCHAIN). At runtime, elan MUST honour the mounted repo's lean-toolchain, so a toolchain bump needs no image change.
4. Mathlib by binary cache only. The runbook and devcontainer use lake exe cache get; nothing in the image builds mathlib from source (ADR-002).
5. Non-root. Default process user is dev (uid/gid overridable via build args for host id mapping under rootless Podman).
6. Engine-portable. The same Dockerfile/docker-compose.yml build and run under Docker and Podman with no per-engine fork (DRY).

Runtime contract (inside the container, from /workspace)

The environment MUST be able to run the full local preflight:

lake exe cache get
lake build UnsorryLibrary --wfail                                  # Gate A strictness bar
python3 -m tools.gate_b validate . --at "<ISO8601Z>"               # Gate B
python3 -m pytest tools -q                                         # tooling suite
./swarm/agent.sh --self-test                                       # agent-loop self-tests
./swarm/agent.sh --prove-local --goal <id> --dry-run               # authoring path (no remote)

Acceptance: with a warm .lake volume, lake build UnsorryLibrary --wfail succeeds, Gate B exits 0 on a clean tree, and agent.sh --self-test passes all tests (the native-Windows text-handling failures the container exists to eliminate do not occur in the Linux userland).

CI smoke contract (devcontainer-smoke.yml)

Triggered only when DevX artifacts change (path filter on the files above). It MUST:

1. Build the image (docker build / buildx).
2. Run, inside the image with the repo mounted, the mathlib-free checks that fit a fast CI job:
   • python3 -m tools.gate_b validate . --at "$(date -u +%Y-%m-%dT%H:%M:%SZ)"
   • python3 -m pytest tools -q
   • ./swarm/agent.sh --self-test
3. NOT attempt the full mathlib build/Gate A replay (cost belongs to the existing gate-a workflow); the smoke proves the environment, not the library.
4. Be a non-required, advisory check unless maintainers choose otherwise (it is DevX, not a soundness gate). It touches .github/, so it is CODEOWNERS-reviewed (ADR-019).

Sterilization invariants (CI-checkable)

• grep-clean of all DevX artifacts for personal identifiers, absolute host paths, prompt text, and the __.ignore* scratch convention. (A reviewer or a lint step can assert this; the contributor runs it before submission.)
• .dockerignore and the repository .gitignore both exclude .env and __.ignore*, so local secrets and scratch never enter a build context, image, or commit.

Non-goals

• Native-Windows-shell support for the agent loop (out of scope; the container is the cross-platform answer).
• Changing mathlib provisioning, caching strategy, or any gate.
• Production runtime/orchestration images (this is a development container; see SPEC-030-A for the distributed-workload direction).