sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: use response files on all platforms to avoid ARG_MAX (#12540)

Browse Source 
This PR extends Lake's use of response files (`@file`) from Windows-only
to all platforms, avoiding `ARG_MAX` limits when invoking `clang`/`ar`
with many object files.

Lake already uses response files on Windows to avoid exceeding CLI
length limits. On macOS and Linux, linking Mathlib's ~15,000 object
files into a shared library can exceed macOS's `ARG_MAX` (262,144
bytes). Both `clang` and `gcc` support `@file` response files on all
platforms, so this is safe to enable unconditionally.

Reported as a macOS issue at
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/The.20clang.20command.20line.20with.20all.20~15.2C000.20Mathlib.20.2Ec.2Eo.2Eexport/near/574369912:
the Mathlib cache ships Linux `.so` shared libs but not macOS `.dylib`
files, so `precompileModules` on macOS triggers a full re-link that
exceeds `ARG_MAX`.

🤖 Prepared with Claude Code

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison
2026-03-17 15:14:37 +11:00
committed by GitHub
parent 50ee6dff0a
commit e96b0ff39c
1 changed files with 14 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

29
src/lake/Lake/Build/Actions.lean
View File

@@ -87,21 +87,20 @@ public def compileO
}
public def mkArgs (basePath : FilePath) (args : Array String) : LogIO (Array String) := do
if Platform.isWindows then
-- Use response file to avoid potentially exceeding CLI length limits.
let rspFile := basePath.addExtension "rsp"
let h ← IO.FS.Handle.mk rspFile .write
args.forM fun arg =>
-- Escape special characters
let arg := arg.foldl (init := "") fun s c =>
if c == '\\' || c == '"' then
s.push '\\' |>.push c
else
s.push c
h.putStr s!"\"{arg}\"\n"
return #[s!"@{rspFile}"]
else
return args
-- Use response file to avoid potentially exceeding CLI length limits.
-- On Windows this is always needed; on macOS/Linux this is needed for large
-- projects like Mathlib where the number of object files exceeds ARG_MAX.
let rspFile := basePath.addExtension "rsp"
let h ← IO.FS.Handle.mk rspFile .write
args.forM fun arg =>
-- Escape special characters
let arg := arg.foldl (init := "") fun s c =>
if c == '\\' || c == '"' then
s.push '\\' |>.push c
else
s.push c
h.putStr s!"\"{arg}\"\n"
return #[s!"@{rspFile}"]
public def compileStaticLib
(libFile : FilePath) (oFiles : Array FilePath)