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

When making an extern_lib that uses symbols from an extern_lib in a dependency, an error occurs while compiling a lean file.

Context

Prior discussion on the Lean Zulip.

Steps to Reproduce

1. Define extern_lib referencing a symbol in a dependency's extern_lib
2. Build

MWE

Expected behavior: Build succeeds.

Actual behavior:

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

Versions

"4.8.0"
"4.10.0-nightly-2024-06-25"
Fedora Linux 6.8.9-300.fc40.x86_64

Impact

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