diff --git a/Lake/Build/Actions.lean b/Lake/Build/Actions.lean index 81a2111..b37542a 100644 --- 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 index 304714b..1cde47d 100644 --- 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 index 473951d..28c341e 100644 --- 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 index 0ed452e..5a0f772 100644 --- 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