undefined symbol: __libc_csu_fini

Stream: lean4

[Tomas Skrivan]

I'm trying to update LeanBLAS to newer toolchain but I'm getting some linker errors that I have no idea what to do about:

$ lake test
✖ [4/4] Building CBLASLevelOneTest:exe
trace: .> /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/bin/clang -o /home/tskrivan/Documents/LeanBLAS/.lake/build/bin/CBLASLevelOneTest  [...]
info: stderr:
ld.lld: error: undefined symbol: __libc_csu_fini
>>> referenced by start.S:101 (../sysdeps/x86_64/start.S:101)
>>>               /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/lib/Scrt1.o:(_start)

ld.lld: error: undefined symbol: __libc_csu_init
>>> referenced by start.S:102 (../sysdeps/x86_64/start.S:102)
>>>               /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/lib/Scrt1.o:(_start)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command '/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/bin/clang' exited with code 1
Some required builds logged failures:
- CBLASLevelOneTest:exe
error: build failed

What can I do about this? Probably there is some mismatch between Lean's and system's C libraries. I'm running Ubuntu 24.04 and compiling with Lean v4.22.0

[Tomas Skrivan]

The compilation command is

code

/home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/bin/clang -o /home/tskrivan/Documents/LeanBLAS/.lake/build/bin/CBLASLevelOneTest /home/tskrivan/Documents/LeanBLAS/.lake/build/ir/Test/cblas_level_one.c.o.export -L/usr/lib/x86_64-linux-gnu/ -lblas -fuse-ld=bfd -L /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/lib/lean --sysroot /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0 -L /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/lib -L /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0/lib/glibc -lc -lc_nonshared -Wl,--as-needed -l:ld.so -Wl,--no-as-needed -lpthread_nonshared -Wl,--as-needed -Wl,-Bstatic -lgmp -lunwind -luv -Wl,-Bdynamic -Wl,--no-as-needed -fuse-ld=lld -Wl,--start-group -lleancpp -lLean -Wl,--end-group -lStd -Wl,--start-group -lInit -lleanrt -Wl,--end-group -Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic -lLake -Wl,--as-needed -lgmp -luv -lpthread -ldl -lrt -Wl,--no-as-needed -lm -ldl -pthread

If I remove

--sysroot /home/tskrivan/.elan/toolchains/leanprover--lean4---v4.22.0

then it compiles fine.

[Tomas Skrivan]

Ok the problem is with OpenBLAS library is distributed on Ubuntu 24.04 for glibc 2.39 but Lean v4.22.0 uses glibc 2.26. This causes incompatibility as newer versions of glibc do not have __libc_csu_fini/init.

Not sure what to do exactly:

1. compile OpenBLAS against the C libraries distributed with the specific version of Lean
2. tell Lean to use system's C libraries (I think this is effectively removing the --sysroot flag)

What is the most future proof approach?

---

@Peiyang Song I see that Lean Copilot is building OpenBLAS from source. Did you come across with this issue? Are you using BLAS in Lean FFI? If not then you probably do not suffer from this.

[Tomas Skrivan]

@Mac Malone Any idea how set up lakefile to resolve this issue?

[Sebastian Ullrich]

I suspect the issue is adding the entire system root as a library path and doing so very early in the cmdline. Try oassing the .so directly without changing the library path?

[Tomas Skrivan]

Ohh, changing

  moreLinkArgs := #["-L/usr/lib/x86_64-linux-gnu/", "-lblas"]

to

  moreLinkArgs := #["/usr/lib/x86_64-linux-gnu/libblas.so"]

solves the issue.

[Tomas Skrivan]

Sebastian Ullrich said:

Try oassing the .so directly without changing the library path?

Is that what you had in mind? I'm not sure if I understand your suggestion correctly.

[Sebastian Ullrich]

Yes, exactly