Skip to content

Commit

Permalink
fix: include moreLinkArgs in precompile link
Browse files Browse the repository at this point in the history
  • Loading branch information
tydeu committed Aug 23, 2023
1 parent 24cfae2 commit acc84a6
Show file tree
Hide file tree
Showing 8 changed files with 27 additions and 4 deletions.
6 changes: 4 additions & 2 deletions src/lake/Lake/Build/Module.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 0 additions & 2 deletions src/lake/examples/ffi/lib/lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@ package ffi {
precompileModules := true
}

lean_lib FFI

@[default_target] lean_exe test {
root := `Main
}
Expand Down
1 change: 1 addition & 0 deletions src/lake/test/precompileArgs/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
/build
1 change: 1 addition & 0 deletions src/lake/test/precompileArgs/Foo.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
import Foo.Bar
Empty file.
1 change: 1 addition & 0 deletions src/lake/test/precompileArgs/clean.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
rm -rf build
11 changes: 11 additions & 0 deletions src/lake/test/precompileArgs/lakefile.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
import Lake
open Lake DSL

package precompileArgs

@[default_target]
lean_lib Foo {
precompileModules := true
moreLinkArgs := #["-lBaz"]
}

9 changes: 9 additions & 0 deletions src/lake/test/precompileArgs/test.sh
Original file line number Diff line number Diff line change
@@ -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"

0 comments on commit acc84a6

Please sign in to comment.