Skip to content

fix: use libtool instead of ar for static libs on macOS#12957

Merged
tydeu merged 4 commits intomasterfrom
fix-macos-ar-response-files
Mar 18, 2026
Merged

fix: use libtool instead of ar for static libs on macOS#12957
tydeu merged 4 commits intomasterfrom
fix-macos-ar-response-files

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

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

This PR fixes a build failure on macOS introduced by #12540. macOS BSD ar does not support the @file response file syntax that #12540 enabled unconditionally. On macOS, when building core (i.e., bootsrap := true), recBuildStatic now uses libtool -static -filelist, which handles long argument lists natively.

Includes a stage0/src/stdlib_flags.h trigger so CI will automatically run update-stage0 after merge.

🤖 Prepared with Claude Code

Implementation adjusted by @tydeu

@kim-em kim-em requested a review from tydeu as a code owner March 18, 2026 00:04
@kim-em kim-em added the changelog-lake Lake label Mar 18, 2026
@kim-em kim-em force-pushed the fix-macos-ar-response-files branch 2 times, most recently from c0359e2 to 7f86d69 Compare March 18, 2026 00:31
@kim-em kim-em added the lake-ci Run all Lake tests label Mar 18, 2026
This PR fixes a build failure on macOS introduced by #12540. macOS BSD
`ar` does not support the `@file` response file syntax that #12540
enabled unconditionally. On macOS, when no archiver has been explicitly
configured (via `LEAN_AR`, bundled `llvm-ar`, or `AR`),
`compileStaticLib` now uses `libtool -static -filelist` instead, which
handles long argument lists natively. When an archiver has been
explicitly configured, it is used directly with response files as before.

To track this, `LeanInstall.ar` is changed to `LeanInstall.ar?` (an
`Option FilePath`), with `none` meaning no archiver was found and the
system default should be used.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
@kim-em kim-em force-pushed the fix-macos-ar-response-files branch from 7f86d69 to b9f8f00 Compare March 18, 2026 00:41
@tydeu
Copy link
Copy Markdown
Member

tydeu commented Mar 18, 2026

If I understand correctly, this is just for core, right? I do not like that this makes the ar generally optional in the toolchain.

Instead, for example, the Lean library in recBuildStatic could set some option for buildStaticLib (e.g., useLibtool or even bootstrap) indicating one should use libtool on macOS when in core -- i.e., self.pkg.bootstrap is true . There is already a special case there for the use of thin in core. Alternatively, it could just inline the buildStaticLib code and pass none for compileStaticLib's AR when bootstrapping.

In essence, I think we should make this as local as possible to the case where things break (i.e., bootstrapping core) and minimally impact the API in doing so.

@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 Mar 18, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing bot commented Mar 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 bf4f51e70471a4828855f69967345c27869ad2ad --onto 6714601ee4a123fef0f6ff3e44f01086ba78dfce. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-18 02:01:31)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase bf4f51e70471a4828855f69967345c27869ad2ad --onto 61a3443a9569d548a235f785b9a33984bb7ff622. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-18 13:13:59)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase bf4f51e70471a4828855f69967345c27869ad2ad --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-18 02:01:32)

@tydeu tydeu added the release-ci Enable all CI checks for a PR, like is done for releases label Mar 18, 2026
@tydeu tydeu enabled auto-merge March 18, 2026 04:35
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
@Kha Kha removed release-ci Enable all CI checks for a PR, like is done for releases lake-ci Run all Lake tests labels Mar 18, 2026
@tydeu tydeu added this pull request to the merge queue Mar 18, 2026
Merged via the queue into master with commit 7ee8c4a Mar 18, 2026
16 of 22 checks passed
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