Cannot import precompiled module that uses an `extern`al definition

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

• Define an extern_lib that provides the implementation my_add for some axiom or opaque definition myAdd annotated with @[extern "my_add"]
• Add a use of that extern definition three := myAdd 1 2 to the same pre-compiled library
• Import the module defining three in the Main module of an executable
• Observe that step "Building Main" fails with symbol lookup error: ././.lake/build/lib/libFFI-1.so: undefined symbol: my_add

Context

[Broader context that the issue occurred in. If there was any prior discussion on the Lean Zulip, link it here as well.]

Steps to Reproduce

$ git clone https://github.com/leanprover/lean4
$ cd lean4/
$ patch -p1 << EOF
> diff --git a/src/lake/examples/ffi/lib/lakefile.lean b/src/lake/examples/ffi/lib/lakefile.lean
index 18d3af3..412df95 100644
--- a/src/lake/examples/ffi/lib/lakefile.lean
+++ b/src/lake/examples/ffi/lib/lakefile.lean
@@ -4,7 +4,8 @@ open System Lake DSL
 package ffi where
   srcDir := "lean"

-lean_lib FFI
+lean_lib FFI where
+  precompileModules := true

 @[default_target]
 lean_exe test where
@@ -14,7 +15,7 @@ target ffi.o pkg : FilePath := do
   let oFile := pkg.buildDir / "c" / "ffi.o"
   let srcJob ← inputTextFile <| pkg.dir / "c" / "ffi.cpp"
   let weakArgs := #["-I", (← getLeanIncludeDir).toString]
-  buildO oFile srcJob weakArgs #["-fPIC"] "c++" getLeanTrace
+  buildO oFile srcJob weakArgs #["-fPIC"] "leanc" getLeanTrace

 extern_lib libleanffi pkg := do
   let ffiO ← ffi.o.fetch
diff --git a/src/lake/examples/ffi/lib/lean-toolchain b/src/lake/examples/ffi/lib/lean-toolchain
new file mode 100644
index 0000000..98556ba
--- /dev/null
+++ b/src/lake/examples/ffi/lib/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.12.0-rc1
diff --git a/src/lake/examples/ffi/lib/lean/FFI.lean b/src/lake/examples/ffi/lib/lean/FFI.lean
index 35c838b..6039512 100644
--- a/src/lake/examples/ffi/lib/lean/FFI.lean
+++ b/src/lake/examples/ffi/lib/lean/FFI.lean
@@ -1,2 +1,4 @@
 import FFI.Fn
 import FFI.Add
+
+def three : UInt32 := myAdd 1 2
EOF
$ cd src/lake/examples/ffi/lib/
$ lake build -v
...
✖ [16/18] Building Main
trace: .> LEAN_PATH=././.lake/build/lib LD_LIBRARY_PATH=././.lake/build/lib:././.lake/build/lib /home/sgraf/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/lean ././lean/./Main.lean -R ././lean/. -o ././.lake/build/lib/Main.olean -i ././.lake/build/lib/Main.ilean -c ././.lake/build/ir/Main.c --load-dynlib=././.lake/build/lib/libleanffi.so --load-dynlib=././.lake/build/lib/libFFI-Fn-1.so --load-dynlib=././.lake/build/lib/libFFI-Add-1.so --load-dynlib=././.lake/build/lib/libFFI-1.so --json
info: stderr:
/home/sgraf/.elan/toolchains/leanprover--lean4---v4.12.0-rc1/bin/lean: symbol lookup error: ././.lake/build/lib/libFFI-1.so: undefined symbol: my_add
error: Lean exited with code 127
Some required builds logged failures:
- Main
error: build failed

Expected behavior: Successful build

Actual behavior: Linker error

Versions

4.12.0-rc1
NixOS

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start in src/lake/examples/ffi/lib and reproduce the failure with lake build -v after enabling precompileModules in lakefile.lean and adding three in lean/FFI.lean. Trace how the precompiled FFI library and its extern_lib are loaded during Building Main; done means the example builds successfully without the undefined my_add symbol.