Fix dev container: pin lean4game to a revision that exists

[gustavdelius]

The problem

"Reopen in Container" fails before the container is ever created. .devcontainer/Dockerfile derives the lean4game ref from lean-toolchain:

--branch $LEAN_VERSION    # -> --branch v4.26.0

but lean4game has no v4.26.0 tag — its tags skip v4.24–v4.27 — so the image build dies with:

fatal: Remote branch v4.26.0 not found in upstream origin

Three further failures were queued up behind that one:

1. lakefile.lean pinned GameServer to the branch chore/bump-v4.26.0, which GitHub deleted when lean4game PR #438 was merged. The lake update -R in onCreateCommand would have failed next.
2. That onCreateCommand had no lake exe cache get, so mathlib would have been compiled from scratch — hours instead of minutes. The error message it prints on failure already mentioned cache get; the command itself didn't.
3. PATH lost /usr/local/elan/bin in login shells, because Debian's /etc/profile overwrites PATH. A login shell is how VSCode starts its integrated terminal, so lake build after editing a level — the documented workflow — would have been command not found.

The fix

• Dockerfile reads the lean4game revision out of lake-manifest.json, so the frontend we serve and the GameServer we compile against cannot drift apart. It deliberately does not derive it from lean-toolchain: lean4game has no release tag for every Lean version. Also adds /etc/profile.d/elan.sh for the PATH issue.
• lakefile.lean / lake-manifest.json pin GameServer to 213bb24, the newest lean4game commit on main still on Lean v4.26.0. Its server/ tree is byte-identical to the commit that was pinned through the deleted branch (git diff between them is empty), so this is a drop-in — and it is reachable from main rather than from a branch that no longer exists.
• devcontainer.json runs lake exe cache get && lake build, and no longer runs lake update -R: re-resolving would also move mathlib's transitive dependencies, which invalidates the mathlib cache. It also replaces the backticks inside the echo "ERROR: ..." messages with quotes — the shell was treating them as command substitutions, so a failed npm install silently re-ran npm install instead of printing the error.
• .dockerignore (new): the build context is the whole repository, and the bind mount means .lake lands on the host. It measured 7.4 GB after one build, and without this it would be sent to the docker daemon on every rebuild.
• docker-compose.yml: drop the obsolete version key that Compose warns about.

Note on the commit pin

213bb24 is a bare commit rather than a version string on purpose. Upstream's convention (documented in GameSkeleton's lakefile as -- Using this assumes that each dependency has a tag of the form v4.X.0) cannot be followed here, because the v4.26.0 bump landed on lean4game main as 76e7d7f but was never tagged, while v4.23.0 and v4.28.0 both were. I have opened an upstream issue asking for the tag; if it is created, this can become "v4.26.0" again.

Verification

Ran the full container-create sequence in the built image, against a throwaway copy of the repo:

step	result
docker compose build	image built
lean4game checkout	at 213bb24, server/lean-toolchain = v4.26.0
lake --version (login and non-login shell)	Lake 5.0.0, Lean 4.26.0
npm install	exit 0
lake exe cache get	exit 0
lake build	exit 0, 2162/2162 jobs
npm start	page served HTTP 200, relay listening on 8080

No error: lines anywhere in the build. The only diagnostics were the pre-existing No translation (en) found for: warnings and lean4game's "No world introducing X" inventory warnings, both unrelated to this change.

🤖 Generated with Claude Code