FFI with rust package that uses pthreads

Stream: lean4

[Jesse Wright]

EDIT: I now have this working; and the library is published to https://github.com/jeswr/RDF.lean

I'm trying to put together an RDF library for lean, rather than building parsers and serialisers from the ground up - I am trying to use FFI with existing rust crates used in Oxigraph. This works for some functionalities, but fails to build when using the oxigraph parsers with the error below. Is there some way of configuring the linker from the lakefile so that it can find the pthread_atfork symbol?

My code is at https://github.com/jeswr/RustFFI.lean, and the error can be reproduced by running lake exe ffi

info: stderr:
   Compiling libc v0.2.152
   Compiling cfg-if v1.0.0
   Compiling ppv-lite86 v0.2.17
   Compiling oxiri v0.2.3-alpha.1
   Compiling oxilangtag v0.1.3
   Compiling memchr v2.7.1
   Compiling getrandom v0.2.12
   Compiling rand_core v0.6.4
   Compiling rand_chacha v0.3.1
   Compiling rand v0.8.5
   Compiling oxrdf v0.2.0-alpha.2
   Compiling oxttl v0.1.0-alpha.2
   Compiling some_rust_lib v0.1.0 (/home/jesght/Documents/GitHub/RustFFI.lean)
    Finished release [optimized] target(s) in 2.38s
info: [0/2] Linking libsome_rust_lib.so
info: [0/2] Compiling ffi.c
info: [0/2] Creating libffi.a
info: [0/2] Linking libffi.so
info: [0/2] Building Main
info: [1/2] Compiling Main
info: [2/2] Linking ffi
error: > /home/jesght/.elan/toolchains/leanprover--lean4---stable/bin/leanc -o ./.lake/build/bin/ffi ./.lake/build/ir/Main.c.o ./.lake/build/libsome_rust_lib.a ./.lake/build/libffi.a
error: stderr:
ld.lld: error: undefined symbol: pthread_atfork
>>> referenced by rand.bc76296bf3435627-cgu.1
>>>               rand-3f442ab5a627cfd5.rand.bc76296bf3435627-cgu.1.rcgu.o:(std::sys_common::once::futex::Once::call::h8aa64e5ca0a6779a) in archive ./.lake/build/libsome_rust_lib.a
>>> did you mean: pthread_atfork@GLIBC_2.2.5
>>> defined in: /home/jesght/.elan/toolchains/leanprover--lean4---stable/lib/glibc/libpthread.so
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/home/jesght/.elan/toolchains/leanprover--lean4---stable/bin/leanc` exited with code

[Sebastian Ullrich]

While I'm responsible for that part of the toolchain I'm afraid I still don't understand Linux symbol versioning enough to pinpoint the issue. Two general remarks:

• You can force Lean to use the system linker (and C compiler) like Rust using the environment variable LEANC_CC=cc
• Alternatively, using dynamic instead of static linking can simplify linking since then the Rust toolchain is responsible for linking Rust code

[Jesse Wright]

You can force Lean to use the system linker (and C compiler) like Rust using the environment variable LEANC_CC=cc

Doing this boils up new errors (below) that I fear will be a rabbit hole so leaving continuing with this pathway as a last resort

error: > /home/jesght/.elan/toolchains/leanprover--lean4---stable/bin/leanc -o ./.lake/build/bin/ffi ./.lake/build/ir/Main.c.o ./.lake/build/libsome_rust_lib.a ./.lake/build/libffi.a
error: stderr:
/usr/bin/ld: cannot find -lc++: No such file or directory
/usr/bin/ld: cannot find -lc++abi: No such file or directory
/usr/bin/ld: cannot find -lgmp: No such file or directory
collect2: error: ld returned 1 exit status
error: external command `/home/jesght/.elan/toolchains/leanprover--lean4---stable/bin/leanc` exited with code 1

Alternatively, using dynamic instead of static linking can simplify linking since then the Rust toolchain is responsible for linking Rust code

Do you have pointers to an example of how to configure this in Lean? I'm struggling to find any relevant resources - presumably I should be replacing buildStaticLib with a dynamic equivalent; I just cant work out what that should be.

[Jesse Wright]

Turns this is something ChatGPT can answer with a bit of the right prompting (https://chat.openai.com/share/403f7afb-a66c-4095-916f-27ab418b5dbd). Working code is now pushed to https://github.com/jeswr/RustFFI.lean.