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

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

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

src/CMakeLists.txt

@@ -945,6 +945,7 @@ install(
   PATTERN "*.hash" EXCLUDE
   PATTERN "*.trace" EXCLUDE
   PATTERN "*.rsp" EXCLUDE
+  PATTERN "*.filelist" EXCLUDE
 )
 
 # symlink source into expected installation location for go-to-definition, if file system allows it

src/lake/Lake/Build/Library.lean

@@ -12,6 +12,7 @@ import Lake.Build.Targets
 import Lake.Build.Job.Register
 import Lake.Build.Target.Fetch
 import Lake.Build.Infos
+import Lake.Util.Proc
 
 /-! # Library Facet Builds
 Build function definitions for a library's builtin facets.
@@ -77,14 +78,31 @@ public def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
     mod.nativeFacets shouldExport |>.mapM (·.fetch mod)
   let moreOJobs ← self.moreLinkObjs.mapM (·.fetchIn self.pkg)
   let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
-  /-
-  The Lean core build requires a thin static library with exported symbols
-  as part of its build process on Windows. However, core is also built without the
-  bundled `llvm-ar`, which is usually a version of `ar` without support for thin archives
-  on macOS. Thus, we have to special case using thin archives on the Windows core build.
-  -/
-  let thin := self.pkg.bootstrap && System.Platform.isWindows && shouldExport
-  buildStaticLib libFile (oJobs ++ moreOJobs) (thin := thin)
+  let bootstrap := self.pkg.bootstrap
+  (Job.collectArray (oJobs ++ moreOJobs) "objs").mapM fun oFiles => do
+    let art ← buildArtifactUnlessUpToDate libFile (ext := "a") (restore := true) do
+      if bootstrap then
+        -- The Lean core build is not built with the bundled `llvm-ar`,
+        -- so it must be special-cased to resolve issues with the system `ar`.
+        if System.Platform.isOSX then
+          -- macOS BSD `ar` does not support `@file` response files.
+          -- Use `libtool -static -filelist` instead, which handles long argument lists natively.
+          createParentDirs libFile
+          let filelistPath := libFile.addExtension "filelist"
+          let h ← IO.FS.Handle.mk filelistPath .write
+          oFiles.forM fun f => h.putStr s!"{f}\n"
+          proc {cmd := "libtool", args := #["-static", "-o", libFile.toString,
+            "-filelist", filelistPath.toString]}
+        else if System.Platform.isWindows then
+          -- The Lean core build requires a thin static library
+          -- with exported symbols as part of its build process on Windows.
+          compileStaticLib libFile oFiles (← getLeanAr) (thin := shouldExport)
+        else
+          -- The normal build process currently works fine on Linux.
+          compileStaticLib libFile oFiles (← getLeanAr)
+      else
+        compileStaticLib libFile oFiles (← getLeanAr)
+    return art.path
 
 /-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
 public def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=