fix: lake: extern_lib linking (#7987)

This PR fixes a bug in #7967 that broke external library linking.

This is slipped through because the FFI example no longer uses
`extern_lib`. As such, a separate `extern_lib` test has been added.

src/lake/Lake/Build/ExternLib.lean

@@ -42,7 +42,8 @@ def buildLeanSharedLibOfStatic
           #[s!"-Wl,-force_load,{staticLib}"]
         else
           #["-Wl,--whole-archive", staticLib.toString, "-Wl,--no-whole-archive"]
-      let args := baseArgs ++ weakArgs ++ traceArgs ++ lean.ccLinkSharedFlags
+      let args := baseArgs ++ weakArgs ++ traceArgs ++
+        #["-L", lean.leanLibDir.toString] ++ lean.ccLinkSharedFlags
       compileSharedLib dynlib args lean.cc
     return dynlib
 

src/lake/examples/ffi/test.sh

@@ -16,6 +16,6 @@ $LAKE exe -d lib test
 $LAKE -d app build -v | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
 $LAKE -d lib build -v | (grep --color -E 'load-dynlib|plugin' && exit 1 || true)
 
-# Tests the successful precompilation of an `extern_lib`
+# Tests the successful precompilation of an FFI library
 # Also tests a module with `precompileModules` always precompiles its imports
 $LAKE -d app build Test

src/lake/tests/externLib/Main.lean

@@ -0,0 +1,4 @@
+import FFI
+
+def main : IO Unit :=
+  IO.println <| myAdd 1 2

src/lake/tests/externLib/Test.lean

@@ -0,0 +1,3 @@
+import FFI
+
+#eval myAdd 3 4

src/lake/tests/externLib/clean.sh

@@ -0,0 +1,3 @@
+rm -f produced.out
+rm -rf .lake lake-manifest.json
+rm -rf ffi/.lake ffi/lake-manifest.json

src/lake/tests/externLib/ffi/FFI.lean

@@ -0,0 +1,2 @@
+@[extern "my_add"]
+opaque myAdd : UInt32 → UInt32 → UInt32

src/lake/tests/externLib/ffi/Main.lean

@@ -0,0 +1,4 @@
+import FFI
+
+def main : IO Unit :=
+  IO.println <| myAdd 1 2

src/lake/tests/externLib/ffi/ffi.c

@@ -0,0 +1,5 @@
+#include <stdint.h>
+
+uint32_t my_add(uint32_t a, uint32_t b) {
+  return a + b;
+}

src/lake/tests/externLib/ffi/lakefile.lean

@@ -0,0 +1,20 @@
+import Lake
+open System Lake DSL
+
+package ffi
+
+lean_lib FFI
+
+lean_exe test where
+  root := `Main
+
+target ffi.o pkg : FilePath := do
+  let oFile := pkg.buildDir / "c" / "ffi.o"
+  let srcJob ← inputTextFile <| pkg.dir / "ffi.c"
+  let weakArgs := #["-I", (← getLeanIncludeDir).toString]
+  buildO oFile srcJob weakArgs #["-fPIC"] "cc" getLeanTrace
+
+extern_lib libleanffi pkg := do
+  let ffiO ← ffi.o.fetch
+  let name := nameToStaticLib "leanffi"
+  buildStaticLib (pkg.staticLibDir / name) #[ffiO]

src/lake/tests/externLib/lakefile.toml

@@ -0,0 +1,13 @@
+name = "test"
+
+[[require]]
+name = "ffi"
+path = "ffi"
+
+[[lean_lib]]
+name = "Test"
+precompileModules = true
+
+[[lean_exe]]
+name = "test"
+root = "Main"

src/lake/tests/externLib/test.sh

@@ -0,0 +1,16 @@
+#!/usr/bin/env bash
+source ../common.sh
+
+./clean.sh
+
+# Tests the successful compilation of an `extern_lib`
+test_run -d ffi -v exe test
+
+# Tests the successful precompilation of an `extern_lib` (from a dep)
+test_run -v build Test
+
+# Tests the successful compilation of an `extern_lib` from a dep
+test_run -v exe test
+
+# Cleanup
+rm -f produced.out