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"