feat: lake: thin libraries for static.export (#7586)

This PR changes the `static.export` facet for Lean libraries to produce
thin static libraries.

Static libraries with explicitly exported symbols are only necessary on
Windows (where symbol counts are a concern) and are usually used as part
of local build process and not distributed (as they are in Lean's
build). Thus, it seems reasonable to make them unilaterally thin. They
also need to be thin for the Lean build with Lake.

src/lake/Lake/Build/Actions.lean

@@ -99,13 +99,13 @@ def mkArgs (basePath : FilePath) (args : Array String) : LogIO (Array String) :=
 
 def compileStaticLib
   (libFile : FilePath) (oFiles : Array FilePath)
-  (ar : FilePath := "ar")
+  (ar : FilePath := "ar") (thin := false)
 : LogIO Unit := do
   createParentDirs libFile
-  proc {
-    cmd := ar.toString
-    args := #["rcs", libFile.toString] ++ (← mkArgs libFile <| oFiles.map toString)
-  }
+  let args := #["rcs"]
+  let args := if thin then args.push "--thin" else args
+  let args := args.push libFile.toString ++ (← mkArgs libFile <| oFiles.map toString)
+  proc {cmd := ar.toString, args}
 
 private def getMacOSXDeploymentEnv : BaseIO (Array (String × Option String)) := do
   -- It is difficult to identify the correct minor version here, leading to linking warnings like:

src/lake/Lake/Build/Common.lean

@@ -353,11 +353,11 @@ def buildLeanO
 
 /-- Build a static library from object file jobs using the Lean toolchain's `ar`. -/
 def buildStaticLib
-  (libFile : FilePath) (oFileJobs : Array (Job FilePath))
+  (libFile : FilePath) (oFileJobs : Array (Job FilePath)) (thin :=  false)
 : SpawnM (Job FilePath) :=
   (Job.collectArray oFileJobs).mapM fun oFiles => do
     buildFileUnlessUpToDate' libFile do
-      compileStaticLib libFile oFiles (← getLeanAr)
+      compileStaticLib libFile oFiles (← getLeanAr) thin
     return libFile
 
 /--

src/lake/Lake/Build/Facets.lean

@@ -176,7 +176,14 @@ library_data leanArts : Unit
 abbrev LeanLib.staticFacet := `static
 library_data static : FilePath
 
-/-- A Lean library's static artifact (with exported symbols). -/
+/--
+A Lean library's static artifact (with exported symbols).
+
+Static libraries with explicit exports are built as thin libraries.
+Such libraries are usually used as part of the local build process of some
+shared artifact and not publicly distributed. Standard static libraries are
+much better for distribution.
+-/
 abbrev LeanLib.staticExportFacet := `static.export
 library_data static.export : FilePath
 

src/lake/Lake/Build/Library.lean

@@ -65,7 +65,12 @@ def LeanLib.leanArtsFacetConfig : LibraryFacetConfig leanArtsFacet :=
   let oJobs ← mods.flatMapM fun mod =>
     mod.nativeFacets shouldExport |>.mapM fun facet => fetch <| mod.facet facet.name
   let libFile := if shouldExport then self.staticExportLibFile else self.staticLibFile
-  buildStaticLib libFile oJobs
+  /-
+  Static libraries with explicit exports are built as thin libraries.
+  The Lean build itself requires a thin static library with exported symbols
+  as part of its build process on Windows. It does not distribute this library.
+  -/
+  buildStaticLib libFile oJobs (thin := shouldExport)
 
 /-- The `LibraryFacetConfig` for the builtin `staticFacet`. -/
 def LeanLib.staticFacetConfig : LibraryFacetConfig staticFacet :=