From 898cd0b64733ed4e6990fd99d06c9bd9fe5093dd Mon Sep 17 00:00:00 2001
From: tydeu <tydeu@hatpress.net>
Date: Tue, 22 Aug 2023 20:10:39 -0400
Subject: [PATCH] fix: include `moreLinkArgs` in precompile link

---
 src/lake/Lake/Build/Module.lean            |  6 ++++--
 src/lake/test/precompileArgs/.gitignore    |  1 +
 src/lake/test/precompileArgs/Foo.lean      |  1 +
 src/lake/test/precompileArgs/Foo/Bar.lean  |  0
 src/lake/test/precompileArgs/clean.sh      |  1 +
 src/lake/test/precompileArgs/lakefile.lean | 11 +++++++++++
 src/lake/test/precompileArgs/test.sh       |  9 +++++++++
 7 files changed, 27 insertions(+), 2 deletions(-)
 create mode 100644 src/lake/test/precompileArgs/.gitignore
 create mode 100644 src/lake/test/precompileArgs/Foo.lean
 create mode 100644 src/lake/test/precompileArgs/Foo/Bar.lean
 create mode 100755 src/lake/test/precompileArgs/clean.sh
 create mode 100644 src/lake/test/precompileArgs/lakefile.lean
 create mode 100755 src/lake/test/precompileArgs/test.sh

diff --git a/src/lake/Lake/Build/Module.lean b/src/lake/Lake/Build/Module.lean
index 23e8b59c59..a6eaa7ca04 100644
--- a/src/lake/Lake/Build/Module.lean
+++ b/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)
 
diff --git a/src/lake/test/precompileArgs/.gitignore b/src/lake/test/precompileArgs/.gitignore
new file mode 100644
index 0000000000..796b96d1c4
--- /dev/null
+++ b/src/lake/test/precompileArgs/.gitignore
@@ -0,0 +1 @@
+/build
diff --git a/src/lake/test/precompileArgs/Foo.lean b/src/lake/test/precompileArgs/Foo.lean
new file mode 100644
index 0000000000..e3cdd6def7
--- /dev/null
+++ b/src/lake/test/precompileArgs/Foo.lean
@@ -0,0 +1 @@
+import Foo.Bar
diff --git a/src/lake/test/precompileArgs/Foo/Bar.lean b/src/lake/test/precompileArgs/Foo/Bar.lean
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/src/lake/test/precompileArgs/clean.sh b/src/lake/test/precompileArgs/clean.sh
new file mode 100755
index 0000000000..1582321863
--- /dev/null
+++ b/src/lake/test/precompileArgs/clean.sh
@@ -0,0 +1 @@
+rm -rf build
diff --git a/src/lake/test/precompileArgs/lakefile.lean b/src/lake/test/precompileArgs/lakefile.lean
new file mode 100644
index 0000000000..b52d6f25b8
--- /dev/null
+++ b/src/lake/test/precompileArgs/lakefile.lean
@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+package precompileArgs
+
+@[default_target]
+lean_lib Foo {
+  precompileModules := true
+  moreLinkArgs := #["-lBaz"]
+}
+
diff --git a/src/lake/test/precompileArgs/test.sh b/src/lake/test/precompileArgs/test.sh
new file mode 100755
index 0000000000..54150394d5
--- /dev/null
+++ b/src/lake/test/precompileArgs/test.sh
@@ -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"