fix: include moreLinkArgs in precompile link

Author: tydeu

src/lake/Lake/Build/Module.lean

@@ -211,8 +211,10 @@ def Module.recBuildDynlib (mod : Module) : IndexBuildM (BuildJob Dynlib) := do
       let libDirs := pkgLibDirs ++ externDynlibs.filterMap (·.dir?)
       let depTrace := oTrace.mix <| libTrace.mix externTrace
       let trace ← buildFileUnlessUpToDate mod.dynlibFile depTrace do
-        let args := links.map toString ++
-          libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}")
+        let args :=
+          links.map toString ++
+          libDirs.map (s!"-L{·}") ++ libNames.map (s!"-l{·}") ++
+          mod.linkArgs
         compileSharedLib mod.name.toString mod.dynlibFile args (← getLeanc)
       return (⟨mod.dynlibFile, mod.dynlibName⟩, trace)
 

src/lake/test/precompileArgs/.gitignore

@@ -0,0 +1 @@
+/build

src/lake/test/precompileArgs/Foo.lean

@@ -0,0 +1 @@
+import Foo.Bar

src/lake/test/precompileArgs/Foo/Bar.lean

@@ -0,0 +1 @@
+rm -rf build

src/lake/test/precompileArgs/clean.sh

@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+package precompileArgs
+
+@[default_target]
+lean_lib Foo {
+  precompileModules := true
+  moreLinkArgs := #["-lBaz"]
+}
+

src/lake/test/precompileArgs/lakefile.lean

@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+set -exo pipefail
+
+LAKE=${LAKE:-../../build/bin/lake}
+
+./clean.sh
+
+# Test that `moreLinkArgs` are included when linking precompiled modules
+($LAKE build Foo 2>&1 || true) | grep -- "-lBaz"