Multiple extern_lib

Stream: lean4

[Daniil Kisel]

Can multiple extern_libs use symbols from each other? Can one in package A depend on one from package B? It fails for me when compiling a lean file. The command line in the error ends with a single "--load-dynlib=.../externA.so". While looking at other threads here it seems like there also should be an "externB.so"?

[Mac Malone]

Unfortunately, the order of extern_lib within a package is not controllable and thus they cannot reliable depend on symbols from one another. Between packages, they follow the topological order of the dependencies (i.e., the order of require statements and the order in the manifest). The issue in question will be fixed in the fiuture (and the FFI experience as a whole improved), but it will still be a while until then. In the meantime, the standard workaround is define the extern_lib as an ordinary target and just link to the libraries manualyl via moreLinkArgs (and moreLeanArgs in the case of precompiled modules).

As to your second question, external libraries from the packages of imports should be inherited by modules as-is. So, that sounds like an unexpected problem. Do you have an example (ideally a #mwe) you should share?

[Daniil Kisel]

Here is a minimal example:
A, B.

trace: .> LEAN_PATH=././.lake/packages/b/.lake/build/lib:././.lake/build/lib LD_LIBRARY_PATH=././.lake/build/lib:././.lake/build/lib /home/oopa/.elan/toolchains/stable/bin/lean ././././A.lean -R ./././. -o ././.lake/build/lib/A.olean -i ././.lake/build/lib/A.ilean -c ././.lake/build/ir/A.c --load-dynlib=././.lake/build/lib/libleanffia.so --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, ././.lake/build/lib/libleanffia.so: undefined symbol: b_class
error: Lean exited with code 134
Some builds logged failures:
- A
error: build failed

[Mac Malone]

@Daniil Kisel Oh, I see that your A library / module does not import anything from the package b. This is the problem. Lake only considers the dependencies of a module to be that of its imports (not everything the package it is in depends on). Thus, to make this work you need a B module (of a lean_lib B) in the package b that the A module imports. If the goal is just to inherit the extern_lib, the B module can be empty.

[Daniil Kisel]

I've updated A to use B and it still produces the same error.

[Mac Malone]

@Daniil Kisel :sad: That does seem like a bug. I will take a deeper look into it when I can. In the meantime, could you file an issue on the lean4 repository about this? That will help me keep track of it. :thank_you:

[Daniil Kisel]

Done (lean4#4565)

[Mac Malone]

Thanks! :octopus:

[Mac Malone]

A fix for thiss issue is up at lean4#4566. I discovered that the issue here is actually that Lake is using --load-dynlib to load extern_lib of the main package (e.g., mwe-require-externlib) when it should notbe, rather than not loading the extern_lib of the dependent package when it should. That is, since precompileModules is not turned on for either package, it should not be passing any --load-dynlib at all.

[Mac Malone]

(In other words, for the examples, it should only be linking in the external libaries when building the final executable, not while compiling the Lean modules.)

[Daniil Kisel]

Recently I've tried to build raylib.lean with the nightly toolchain and it failed with a similar error. The examples linked here fail too. Tested with nightly-2025-04-27 and nightly-2025-04-14. Maybe it is a regression, or perhaps there is something that should be changed in my code because of updates?

Failure log

✖ [12/16] Building A
trace: .> LEAN_PATH=/home/oopa/Dev/prj/Lean/tmp/a/.lake/packages/b/.lake/build/lib/lean:/home/oopa/Dev/prj/Lean/tmp/a/.lake/build/lib/lean /home/oopa/.elan/toolchains/leanprover--lean4-nightly---nightly-2025-04-27/bin/lean /home/oopa/Dev/prj/Lean/tmp/a/A.lean -R /home/oopa/Dev/prj/Lean/tmp/a -o /home/oopa/Dev/prj/Lean/tmp/a/.lake/build/lib/lean/A.olean -i /home/oopa/Dev/prj/Lean/tmp/a/.lake/build/lib/lean/A.ilean -c /home/oopa/Dev/prj/Lean/tmp/a/.lake/build/ir/A.c --load-dynlib /home/oopa/Dev/prj/Lean/tmp/a/.lake/build/lib/libleanffia.so --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, /home/oopa/Dev/prj/Lean/tmp/a/.lake/build/lib/libleanffia.so: undefined symbol: b_class
error: Lean exited with code 134
Some required builds logged failures:
- A
error: build failed

[Mac Malone]

@Daniil Kisel Thanks for catching this regression! It is fixed in lean4#8152. This slipped through because the FFI example no longer uses extern_lib.

[Marcus Rossel]

@Daniil Kisel Is your problem solved on nightly-2025-04-30?

[Daniil Kisel]

I've tried with leanprover/lean4-pr-releases:pr-release-8152 and it worked