I built clean and veil from scratch to verify that build_config/ works as intended, and both builds fail.
build_config/ pins both repositories to Mathlib v4.24.0, but at the commits specified in repos.json, both repositories were actually written against Mathlib v4.23.x. This one-version gap breaks three files. I cloned each repository fresh at its exact pinned commit, applied build_config/ exactly as scripts/build_repo.sh does, and ran lake build. The errors below are copied directly from those build logs.
I reproduced this using:
bash scripts/build_repo.sh clean --clone build_config /tmp/out
bash scripts/build_repo.sh veil --clone build_config /tmp/out
Both fail. The toolchain is leanprover/lean4:v4.24.0, with Mathlib pinned to revision f897ebcf72cd16f89ab4577d0c826cd14afaafc7 — matching what build_config/clean and build_config/veil both specify.
clean: Clean/Gadgets/Equality.lean
At commit a134f91f, where the repository's own Mathlib pin is v4.23.0-rc2:
Clean/Gadgets/Equality.lean:41:2: Type mismatch
[`circuit_norm]
has type
List Lean.Name
but is expected to have type
Array Lean.Syntax
Mathlib changed the type of Simps.Config.attrs between v4.23 and v4.24, which is the source of this failure. A fix already exists in scripts/docker_repo_patches.sh, which rewrites the @[simps! ...] attribute — but that script only runs after the repository has already built, against files in data/lean_repos/, and it is never copied into build_config/clean/. As a result, running scripts/setup_repos.sh --clone on its own produces a hard failure here, and the script exits before the patch step is ever reached. The Dockerfile happens to tolerate this because it wraps the clean/veil build steps in || echo "WARNING: ..." before invoking the patch script, so the Docker image still comes out fine — but that masks the underlying issue rather than confirming that build_config/ is correct.
clean: Clean/Tables/Fibonacci8.lean
Same commit as above:
Clean/Tables/Fibonacci8.lean:64:3: unknown tactic
Clean/Tables/Fibonacci8.lean:63:51: unsolved goals
n : ℕ
⊢ fib8 n < 256
...
Clean/Tables/Fibonacci8.lean:104:5: unknown tactic
Clean/Tables/Fibonacci8.lean:99:15: unsolved goals
...
This one remains unresolved. There is an untracked draft rewrite at build_config/clean/Fibonacci8.lean, but nothing copies it into place or references it in any script, so it has no bearing on the current build. It may not even be the correct fix regardless — its own comment notes that it compensates for a behavior change introduced in Lean 4.25.0-rc2, not v4.24.0, which is the version actually pinned here.
veil: Veil/DSL/Specification/Lang.lean
At commit 4a17cf16, where the repository's own Mathlib pin is v4.23.0:
Veil/DSL/Specification/Lang.lean:212:17: overloaded, errors
212:25 Application type mismatch: The argument
`Nonempty
has type
Name
but is expected to have type
SourceInfo
in the application
Parser.mkIdent `Nonempty
Type mismatch
Lean.mkIdent `Nonempty
has type
Ident
but is expected to have type
TSyntax `Lean.Parser.Command.derivingClass
This originates from the following line:
deriving $(mkIdent ``Nonempty))
Whatever the deriving clause parser expects changed between v4.23 and v4.24, and that is the cause of this failure. No fix currently exists for this issue. build_config/veil/ contains only lakefile.lean, lake-manifest.json, and lean-toolchain, and docker_repo_patches.sh makes no mention of veil.
I built clean and veil from scratch to verify that build_config/ works as intended, and both builds fail.
build_config/ pins both repositories to Mathlib v4.24.0, but at the commits specified in repos.json, both repositories were actually written against Mathlib v4.23.x. This one-version gap breaks three files. I cloned each repository fresh at its exact pinned commit, applied build_config/ exactly as scripts/build_repo.sh does, and ran lake build. The errors below are copied directly from those build logs.
I reproduced this using:
Both fail. The toolchain is leanprover/lean4:v4.24.0, with Mathlib pinned to revision f897ebcf72cd16f89ab4577d0c826cd14afaafc7 — matching what build_config/clean and build_config/veil both specify.
clean: Clean/Gadgets/Equality.lean
At commit a134f91f, where the repository's own Mathlib pin is v4.23.0-rc2:
Mathlib changed the type of Simps.Config.attrs between v4.23 and v4.24, which is the source of this failure. A fix already exists in scripts/docker_repo_patches.sh, which rewrites the @[simps! ...] attribute — but that script only runs after the repository has already built, against files in data/lean_repos/, and it is never copied into build_config/clean/. As a result, running scripts/setup_repos.sh --clone on its own produces a hard failure here, and the script exits before the patch step is ever reached. The Dockerfile happens to tolerate this because it wraps the clean/veil build steps in
|| echo "WARNING: ..."before invoking the patch script, so the Docker image still comes out fine — but that masks the underlying issue rather than confirming that build_config/ is correct.clean: Clean/Tables/Fibonacci8.lean
Same commit as above:
This one remains unresolved. There is an untracked draft rewrite at build_config/clean/Fibonacci8.lean, but nothing copies it into place or references it in any script, so it has no bearing on the current build. It may not even be the correct fix regardless — its own comment notes that it compensates for a behavior change introduced in Lean 4.25.0-rc2, not v4.24.0, which is the version actually pinned here.
veil: Veil/DSL/Specification/Lang.lean
At commit 4a17cf16, where the repository's own Mathlib pin is v4.23.0:
This originates from the following line:
deriving $(mkIdent ``Nonempty))Whatever the deriving clause parser expects changed between v4.23 and v4.24, and that is the cause of this failure. No fix currently exists for this issue. build_config/veil/ contains only lakefile.lean, lake-manifest.json, and lean-toolchain, and docker_repo_patches.sh makes no mention of veil.