lake build fails with 'no such file or directory (error code: 2)' on Apple Silicon

[kieranmcshane]

Description

lake build fails for any module target with a generic "no such file or directory" error. This is reproducible across multiple files (tested with both existing 522.lean and new 524.lean), so it is an environmental issue rather than a file-specific one.

Steps to Reproduce

git clone https://github.com/google-deepmind/formal-conjectures.git
cd formal-conjectures
lake build FormalConjectures.ErdosProblems.522

Expected Behavior

Build succeeds (or fails with Lean compilation errors).

Actual Behavior

✔ [0/2] Ran job computation
✔ [1/2] Ran formal_conjectures:extraDep
✖ [2/2] Running FormalConjectures.ErdosProblems.522
error: no such file or directory (error code: 2)
  file: 
Some required targets logged failures:
- FormalConjectures.ErdosProblems.522
error: build failed

Note that lake env lean FormalConjectures/ErdosProblems/522.lean succeeds — only lake build fails.

The same failure occurs for any module target (e.g., FormalConjectures.ErdosProblems.524).

Environment

• Platform: macOS (Darwin 25.4.0), Apple Silicon (arm64)
• Lean toolchain: leanprover/lean4:v4.27.0 (from lean-toolchain)
• Lake: version 5.0.0-src+db93fe1 (Lean version 4.27.0)
• elan installed toolchains: v4.27.0, v4.28.0, v4.29.0, v4.29.0-rc8, v4.29.1 (stable)

Verbose trace (lake build -v)

✔ [0/2] Ran job computation
✔ [1/2] Ran formal_conjectures:extraDep
✖ [2/2] Running FormalConjectures.ErdosProblems.524
error: no such file or directory (error code: 2)
  file: 

The file: field is empty, suggesting Lake is attempting to invoke a binary or path that doesn't resolve on this platform.

Suspected Cause

Likely a Lake/elan toolchain resolution issue specific to Apple Silicon (arm64-apple-darwin). The extraDep step succeeds but the subsequent module compilation step fails to locate a required binary or path.