docker: compose project name collides with sibling repos, silently sharing the olean volume

[raphaelrrcoelho]

the hazard

docker/docker-compose.yml declares no name:, so Compose derives the project name from the compose file's parent directory: docker. Verified:

$ docker compose -f docker/docker-compose.yml config --format json | jq -r .name
docker

Every tree laid out this way — sibling repos (formal-mathfin-contracts, mathfin-foundry) and git worktrees of this repo — derives the same project name, and therefore the same named volumes:

docker_lake_build_cache   ->  /app/.lake
docker_lean_interact_cache

So two different Lean projects share one olean store. Whichever built last owns it. Nothing warns; the symptom is a full rebuild appearing for no reason, or worse, stale oleans from another tree.

observed 2026-08-16

Two sessions hit this from both directions on the same afternoon. One session's daemon startup did a full 8989-job rebuild (~10 min) because the volume held oleans from the other tree; the handoff back cost the same again. Both sessions independently diagnosed it as a bug in their own tree first.

CLAUDE.md's 'one Lake writer at a time — never run a build in one while the other is up' is written for verify vs lean-repl within one tree. It silently under-describes the situation once a sibling repo or a worktree exists: the two writers can be in different checkouts.

fix

A hardcoded name: formal-mathfin is not sufficient, and this was the first proposal here — recording why it fails so it isn't re-proposed. docker/docker-compose.yml is a tracked file, and a git worktree gets its own full checkout of docker/, so a hardcoded name is identical in the main tree and in every worktree cut from it. That fixes sibling-repo collisions while leaving repo-vs-its-own-worktree — the case that actually bit us — untouched. The collision doesn't move, it just gets renamed.

What separates them is a per-tree value that is not in git. Compose reads .env from the project directory, which is the compose file's directory, i.e. per-worktree docker/. Verified empirically:

$ printf 'COMPOSE_PROJECT_NAME=probe-xyz\n' > docker/.env
$ docker compose -f docker/docker-compose.yml config --format json | jq -r .name
probe-xyz

and .gitignore already covers .env / .env.* (lines 27-28), so the per-tree file is untracked by construction. So:

name: ${COMPOSE_PROJECT_NAME:-formal-mathfin}

at the top of docker/docker-compose.yml, plus a gitignored docker/.env in each non-default tree. The main tree needs no setup and falls through to the default; a worktree or sibling sets COMPOSE_PROJECT_NAME=<its own name>.

two things not to be surprised by

1. This is per-clone/per-worktree setup that git does not carry — the same category as the ledger merge driver and core.hooksPath, which CLAUDE.md already documents as two setup lines per clone. Fold it into that same paragraph rather than starting a new one, or it gets missed exactly the way the merge driver was.
2. Separate projects mean separate olean volumes — that is the point, and also the cost. Today the trees clobber each other but share one warm cache. After the fix, each non-default tree starts from an empty .lake and pays one full Mathlib + BrownianMotion + MathFin build — the real one, not the ~10 min incremental. Per the memory doctrine that is CI-runner-sized work, not laptop work. Worth it to never clobber again, but schedule it deliberately.

tasks

• name: ${COMPOSE_PROJECT_NAME:-formal-mathfin} in docker/docker-compose.yml.
• CLAUDE.md: add to the existing per-clone-setup paragraph, and extend the one-writer rule to say it spans sibling checkouts.
• Note the detection commands (docker ps --format '{{.Image}}' | grep mathfin-verify plus ps -eo comm | grep -x lake) — and that neither proves the slot is free; see docs/patterns.md, 'the slot watcher that watched the wrong noun'. Only an explicit handoff does.
• After migration, remove the orphaned docker_* volumes to reclaim the space.