diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 91829c4ed4..27940fffea 100644
--- a/src/CMakeLists.txt
+++ b/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
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index 4aa10a7f44..6cb600d16b 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/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 :=