diff --git a/src/lake/Lake/Build/Executable.lean b/src/lake/Lake/Build/Executable.lean index 63ccbc4fa9..8dc2a437a7 100644 --- a/src/lake/Lake/Build/Executable.lean +++ b/src/lake/Lake/Build/Executable.lean @@ -36,12 +36,16 @@ private def LeanExe.recBuildExe (self : LeanExe) : FetchM (Job FilePath) := for mod in imports do for facet in mod.nativeFacets shouldExport do objJobs := objJobs.push <| ← facet.fetch mod + for link in self.moreLinkObjs do + objJobs := objJobs.push <| ← link.fetchIn self.pkg let libs := imports.foldl (·.insert ·.lib) OrdHashSet.empty |>.toArray for lib in libs do for link in lib.moreLinkObjs do objJobs := objJobs.push <| ← link.fetchIn lib.pkg for link in lib.moreLinkLibs do libJobs := libJobs.push <| ← link.fetchIn lib.pkg + for link in self.moreLinkLibs do + libJobs := libJobs.push <| ← link.fetchIn self.pkg let deps := (← (← self.pkg.transDeps.fetch).await).push self.pkg for dep in deps do for lib in dep.externLibs do diff --git a/src/lake/Lake/Config/LeanExe.lean b/src/lake/Lake/Config/LeanExe.lean index 0f3c2ab84c..be9c716056 100644 --- a/src/lake/Lake/Config/LeanExe.lean +++ b/src/lake/Lake/Config/LeanExe.lean @@ -110,6 +110,14 @@ That is, the package's `weakLinkArgs` plus the executable's `weakLinkArgs`. @[inline] public def weakLinkArgs (self : LeanExe) : Array String := self.pkg.weakLinkArgs ++ self.config.weakLinkArgs +/-- Additional objects (e.g., `.o` files, static libraries) to link to the executable. -/ +@[inline] public def moreLinkObjs (self : LeanExe) : TargetArray FilePath := + self.config.moreLinkObjs + +/-- Additional shared libraries to link to the executable. -/ +@[inline] public def moreLinkLibs (self : LeanExe) : TargetArray Dynlib := + self.config.moreLinkLibs + end LeanExe /-- Locate the named, buildable, but not necessarily importable, module in the package. -/ diff --git a/tests/lake/examples/ffi/lib/lakefile.lean b/tests/lake/examples/ffi/lib/lakefile.lean index ae4991962f..133bb704e2 100644 --- a/tests/lake/examples/ffi/lib/lakefile.lean +++ b/tests/lake/examples/ffi/lib/lakefile.lean @@ -51,3 +51,11 @@ target libleanffi_shared pkg : Dynlib := do lean_lib FFI.Shared where moreLinkLibs := #[libleanffi_shared] + +/-! ## Executable-only FFI -/ + +@[default_target] +lean_exe standalone where + root := `Standalone + moreLinkObjs := #[libleanffi_static] + moreLinkLibs := #[libleanffi_shared] diff --git a/tests/lake/examples/ffi/lib/lean/Standalone.lean b/tests/lake/examples/ffi/lib/lean/Standalone.lean new file mode 100644 index 0000000000..78b8ea856f --- /dev/null +++ b/tests/lake/examples/ffi/lib/lean/Standalone.lean @@ -0,0 +1,9 @@ +@[extern "my_add"] +opaque myAdd : UInt32 → UInt32 → UInt32 + +@[extern "my_lean_fun"] +opaque myLeanFun : IO String + +def main : IO Unit := do + IO.println (myAdd 1 2) + IO.println (← myLeanFun) diff --git a/tests/lake/examples/ffi/test.sh b/tests/lake/examples/ffi/test.sh index c241202b0b..eb1f3740b7 100755 --- a/tests/lake/examples/ffi/test.sh +++ b/tests/lake/examples/ffi/test.sh @@ -10,6 +10,7 @@ $LAKE -d lib build -v $LAKE exe -d app app $LAKE exe -d lib test +$LAKE exe -d lib standalone # Tests that a non-precompiled build does not load anything as a dynlib/plugin # https://github.com/leanprover/lean4/issues/4565