Match Lake's trace githash to the toolchain that built the Mathlib cache

[jwiegley]

Summary

Every consumer of this flake has been recompiling all of Mathlib on every build, because Lake's build traces are keyed on the compiler's githash and the two Leans involved disagree about it:

• the Mathlib artifact cache is produced by the official leanprover/lean4:v4.30.0 release, whose lean --githash is d024af099ca4bf2c86f649261ebf59565dc8c622;
• nixpkgs' lean4 4.30.0 is built from the same source but reports the literal tag, v4.30.0.

So every artifact lake exe cache get fetched failed the trace check, and lake build Mathlib in the deps derivation rebuilt 8,474 jobs from source: 4h19m of a 4h27m cold deps build on ubuntu-latest (this repo's own CI, 03abb3e), and the same hours on every nix build of the C++ ledger repository, which cannot cache a 10 GB output. The proof is in the artifacts: every .olean in the current deps output carries githash v4.30.0; in the pre-03abb3e91 output, 7,370 still carried d024af0… and only the 731 in the import closure had been rebuilt. That mismatch is also why the earlier derivation rebuilt the import closure at all, and why an added import then tried to rebuild inside the read-only store.

Fix: pin the release commit as leanGithash and export it as LEAN_GITHASH wherever lake runs (deps, oracle, dev shell). Lake honours it as the detected githash (Lake/Config/Env.lean), so lake build Mathlib becomes a replay.

Measured (nix build .#deps -L, no module compiled):

platform	machine	deps derivation
x86_64-linux	256-core builder	1m53s – 2m16s
aarch64-linux	10-core builder	2m09s – 4m05s
aarch64-darwin	M3 Ultra	~6.5 min

One hash for every platform. Refreshing the hashes with full-tree checksums (119,869 files) showed that the only files that ever differed between platforms were the natively compiled products of lake exe cache: the .c.o.export objects under build/ir with their .hash/.trace records, and the Cache.* modules' own artifacts, whose traces embed the native facet. The oracle imports none of it, so the cleanup now removes it, and the normalized tree is byte-identical on x86_64-linux, aarch64-linux and aarch64-darwin (also reproduced across two different x86_64 machines). The per-kernel outputHash and the case-insensitive-filesystem hypothesis are gone. The scrub's greps are made tolerant of an empty match set, which stdenv's pipefail otherwise turns into a silent build failure.

Consumers. Lake keys its cached lakefile elaboration on the githash as well, so a downstream that runs the oracle in place with a lake reporting a different githash (the C++ ledger's check phase: this flake's lean on PATH, lake env lean --run in the store tree) fails with "permission denied" on .lake/config/0/lakefile.olean.lock. The second commit wraps the lean package's lake to set LEAN_GITHASH, verified by running the oracle driver from the store tree with only that toolchain on PATH and no variable in the environment.

Docs: AGENTS.md records leanGithash as the fifth pin that must move with the toolchain; the CI comment describes the measurement legs in terms of the single hash (x86_64-darwin remains the one platform not yet seen to reproduce it).

Test plan

• nix build .#deps -L on x86_64-linux (two machines), aarch64-linux and aarch64-darwin: identical hash, all 8,474 Mathlib jobs replayed.
• nix build .#oracle -L on aarch64-darwin builds against the new tree; the driver smoke test from ci.yml passes.
• CI here (ubuntu-latest, macos-latest, plus the two measurement legs) should now take minutes instead of hours; the C++ repository's flake will be bumped in a follow-up PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_01XEq9CB5JypSjKRn8MjRg72