fix: pass pkg linking args to extern lib linking

leanprover · Aug 2, 2022 · bd44264 · bd44264
1 parent 79321cd
commit bd44264
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 4 deletions.
diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean
@@ -53,7 +53,7 @@ def compileO (name : String) (oFile srcFile : FilePath)
 
 def compileStaticLib (name : String) (libFile : FilePath)
 (oFiles : Array FilePath) (ar : FilePath := "ar") : LogIO Unit := do
-  logInfo s!"Linking {name}"
+  logInfo s!"Creating {name}"
   createParentDirs libFile
   proc {
     cmd := ar.toString

diff --git a/Lake/Build/Index.lean b/Lake/Build/Index.lean
@@ -59,7 +59,7 @@ def recBuildWithIndex : (info : BuildInfo) → IndexBuildM (BuildData info.key)
 | .sharedExternLib lib =>
   mkTargetFacetBuild ExternLib.sharedFacet do
     let staticTarget := Target.active <| ← lib.static.recBuild
-    staticToLeanSharedLibTarget lib.name.toString staticTarget |>.activate
+    staticToLeanSharedLibTarget lib.name.toString staticTarget lib.linkArgs |>.activate
 | .dynlibExternLib lib =>
   mkTargetFacetBuild ExternLib.dynlibFacet do
     let sharedTarget := Target.active <| ← lib.shared.recBuild

diff --git a/Lake/Build/Targets.lean b/Lake/Build/Targets.lean
@@ -84,7 +84,8 @@ def leanExeTarget (name : String) (exeFile : FilePath)
   (extraDepTrace := getLeanTrace <&> (·.mix <| pureHash linkArgs)) fun links => do
     compileExe name exeFile links linkArgs (← getLeanc)
 
-def staticToLeanSharedLibTarget (name : String) (staticLibTarget : FileTarget) : FileTarget :=
+def staticToLeanSharedLibTarget (name : String)
+(staticLibTarget : FileTarget) (linkArgs : Array String := #[]) : FileTarget :=
   .mk <| staticLibTarget.bindSync fun staticLib staticTrace => do
     let dynlib := staticLib.withExtension sharedLibExt
     let trace ← buildFileUnlessUpToDate dynlib staticTrace do
@@ -93,7 +94,7 @@ def staticToLeanSharedLibTarget (name : String) (staticLibTarget : FileTarget) :
           #[s!"-Wl,-force_load,{staticLib}"]
         else
           #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
-      compileSharedLib name dynlib args (← getLeanc)
+      compileSharedLib name dynlib (args ++ linkArgs) (← getLeanc)
     return (dynlib, trace)
 
 def sharedToLeanDynlibTarget (sharedLibTarget : FileTarget) : DynlibTarget :=

diff --git a/Lake/Config/ExternLib.lean b/Lake/Config/ExternLib.lean
@@ -32,3 +32,10 @@ namespace ExternLib
 /-- The external library's user-defined `target`. -/
 @[inline] def target (self : ExternLib) : FileTarget :=
   self.config.target
+
+/--
+The arguments to pass to `leanc` when linking the external library.
+That is, the package's `moreLinkArgs`.
+-/
+@[inline] def linkArgs (self : ExternLib) : Array String :=
+  self.pkg.moreLinkArgs