Skip to content

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

Open
kim-em wants to merge 1 commit intoleanprover:masterfrom
kim-em:fix/response-file-all-platforms
Open

fix: use response files on all platforms to avoid ARG_MAX#12540
kim-em wants to merge 1 commit intoleanprover:masterfrom
kim-em:fix/response-file-all-platforms

Conversation

@kim-em
Copy link
Collaborator

@kim-em kim-em commented Feb 18, 2026

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

@kim-em kim-em requested a review from tydeu as a code owner February 18, 2026 00:25
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 18, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 18, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bfc5d43ad314d1e44a71c3ca761a3640ff23c4fb --onto 91bd6e19a7b7aca769f9720e1127c768df0cd2a7. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-18 01:21:41)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9a841125e75eab3c61e0b6affed684692312b668 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-03 04:27:11)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 18, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bfc5d43ad314d1e44a71c3ca761a3640ff23c4fb --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-18 01:21:43)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9a841125e75eab3c61e0b6affed684692312b668 --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-03 04:27:13)

@kim-em kim-em added the changelog-lake Lake label Mar 3, 2026
@kim-em kim-em changed the title fix(lake): use response files on all platforms to avoid ARG_MAX fix: use response files on all platforms to avoid ARG_MAX Mar 3, 2026
Lake already uses response files (`@file`) on Windows to avoid
exceeding CLI length limits. This extends that behavior to macOS
and Linux, where linking Mathlib's ~15,000 object files into a
shared library exceeds 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.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@kim-em kim-em force-pushed the fix/response-file-all-platforms branch from 0757230 to 3823d9a Compare March 3, 2026 03:35
@kim-em
Copy link
Collaborator Author

kim-em commented Mar 3, 2026

@tydeu, can I merge this? It is solving a reported user problem.

@tydeu
Copy link
Member

tydeu commented Mar 4, 2026

@kim-em I looked at this previously and shared Yury's question. With that resolved, this seems like a reasonable change. However, it should first go through release-ci with Lake tests temporarily enabled. That is, with this line temporarily uncommented.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-lake Lake toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants