fix: lake: moreLinkObjs|Libs on a lean_exe (#11117)

This PR fixes a bug where Lake ignored `moreLinkObjs` and `moreLinkLibs`
on a `lean_exe`.

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

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. -/

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]

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)

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