From 5b16ea98f537e4da6c072d00fe89eef6eb4ce6bf Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Thu, 17 Apr 2025 15:33:22 -0400 Subject: [PATCH] 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 | 3 ++- src/lake/examples/ffi/test.sh | 2 +- src/lake/tests/externLib/Main.lean | 4 ++++ src/lake/tests/externLib/Test.lean | 3 +++ src/lake/tests/externLib/clean.sh | 3 +++ src/lake/tests/externLib/ffi/FFI.lean | 2 ++ src/lake/tests/externLib/ffi/Main.lean | 4 ++++ src/lake/tests/externLib/ffi/ffi.c | 5 +++++ src/lake/tests/externLib/ffi/lakefile.lean | 20 ++++++++++++++++++++ src/lake/tests/externLib/lakefile.toml | 13 +++++++++++++ src/lake/tests/externLib/test.sh | 16 ++++++++++++++++ 11 files changed, 73 insertions(+), 2 deletions(-) create mode 100644 src/lake/tests/externLib/Main.lean create mode 100644 src/lake/tests/externLib/Test.lean create mode 100755 src/lake/tests/externLib/clean.sh create mode 100644 src/lake/tests/externLib/ffi/FFI.lean create mode 100644 src/lake/tests/externLib/ffi/Main.lean create mode 100644 src/lake/tests/externLib/ffi/ffi.c create mode 100644 src/lake/tests/externLib/ffi/lakefile.lean create mode 100644 src/lake/tests/externLib/lakefile.toml create mode 100755 src/lake/tests/externLib/test.sh diff --git a/src/lake/Lake/Build/ExternLib.lean b/src/lake/Lake/Build/ExternLib.lean index 02f4ce6734..c8124e6de6 100644 --- a/src/lake/Lake/Build/ExternLib.lean +++ b/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 diff --git a/src/lake/examples/ffi/test.sh b/src/lake/examples/ffi/test.sh index 9484811875..c241202b0b 100755 --- a/src/lake/examples/ffi/test.sh +++ b/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 diff --git a/src/lake/tests/externLib/Main.lean b/src/lake/tests/externLib/Main.lean new file mode 100644 index 0000000000..e763be6b15 --- /dev/null +++ b/src/lake/tests/externLib/Main.lean @@ -0,0 +1,4 @@ +import FFI + +def main : IO Unit := + IO.println <| myAdd 1 2 diff --git a/src/lake/tests/externLib/Test.lean b/src/lake/tests/externLib/Test.lean new file mode 100644 index 0000000000..5131ef7b8a --- /dev/null +++ b/src/lake/tests/externLib/Test.lean @@ -0,0 +1,3 @@ +import FFI + +#eval myAdd 3 4 diff --git a/src/lake/tests/externLib/clean.sh b/src/lake/tests/externLib/clean.sh new file mode 100755 index 0000000000..0ec4c74010 --- /dev/null +++ b/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 diff --git a/src/lake/tests/externLib/ffi/FFI.lean b/src/lake/tests/externLib/ffi/FFI.lean new file mode 100644 index 0000000000..cb6091bcaa --- /dev/null +++ b/src/lake/tests/externLib/ffi/FFI.lean @@ -0,0 +1,2 @@ +@[extern "my_add"] +opaque myAdd : UInt32 → UInt32 → UInt32 diff --git a/src/lake/tests/externLib/ffi/Main.lean b/src/lake/tests/externLib/ffi/Main.lean new file mode 100644 index 0000000000..e763be6b15 --- /dev/null +++ b/src/lake/tests/externLib/ffi/Main.lean @@ -0,0 +1,4 @@ +import FFI + +def main : IO Unit := + IO.println <| myAdd 1 2 diff --git a/src/lake/tests/externLib/ffi/ffi.c b/src/lake/tests/externLib/ffi/ffi.c new file mode 100644 index 0000000000..e09ff2a861 --- /dev/null +++ b/src/lake/tests/externLib/ffi/ffi.c @@ -0,0 +1,5 @@ +#include + +uint32_t my_add(uint32_t a, uint32_t b) { + return a + b; +} diff --git a/src/lake/tests/externLib/ffi/lakefile.lean b/src/lake/tests/externLib/ffi/lakefile.lean new file mode 100644 index 0000000000..e1b3b64589 --- /dev/null +++ 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] diff --git a/src/lake/tests/externLib/lakefile.toml b/src/lake/tests/externLib/lakefile.toml new file mode 100644 index 0000000000..7989803191 --- /dev/null +++ b/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" diff --git a/src/lake/tests/externLib/test.sh b/src/lake/tests/externLib/test.sh new file mode 100755 index 0000000000..a3c730f96e --- /dev/null +++ b/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