From 10f0adc9f9dafbad3ae893eae02fe121faa680a0 Mon Sep 17 00:00:00 2001
From: Mac Malone <tydeu@hatpress.net>
Date: Thu, 20 Mar 2025 00:53:35 -0400
Subject: [PATCH] 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 | 10 +++++-----
 src/lake/Lake/Build/Common.lean  |  4 ++--
 src/lake/Lake/Build/Facets.lean  |  9 ++++++++-
 src/lake/Lake/Build/Library.lean |  7 ++++++-
 4 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/src/lake/Lake/Build/Actions.lean b/src/lake/Lake/Build/Actions.lean
index 470f266e68..2c0d1bc64d 100644
--- a/src/lake/Lake/Build/Actions.lean
+++ b/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:
diff --git a/src/lake/Lake/Build/Common.lean b/src/lake/Lake/Build/Common.lean
index 59116f37ac..031707bc38 100644
--- a/src/lake/Lake/Build/Common.lean
+++ b/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
 
 /--
diff --git a/src/lake/Lake/Build/Facets.lean b/src/lake/Lake/Build/Facets.lean
index 66ed3f7b2c..b084c5ff5e 100644
--- a/src/lake/Lake/Build/Facets.lean
+++ b/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
 
diff --git a/src/lake/Lake/Build/Library.lean b/src/lake/Lake/Build/Library.lean
index ae599fd7d1..3d7c76887f 100644
--- a/src/lake/Lake/Build/Library.lean
+++ b/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 :=