Reverse FFI undefined reference to symbol

Stream: lean4

[Leni Aniva]

I have a tiny reverse FFI example that works on Lean 4.7.0-rc2. However when I try to call the lean_initialize_thread function in the FFI manual:

lean_initialize_thread();

There is an error about undefined symbol:

  = note: /nix/store/p0p56gzz837fgmfd7lyisghcd7x2fdlc-binutils-2.40/bin/ld: /home/aniva/Projects/examples/rust-call-lean/target/debug/deps/caller-932217f92f536a11.52zithdtfqc2z9d9.rcgu.o: in function `caller::main':
          /home/aniva/Projects/examples/rust-call-lean/src/main.rs:154: undefined reference to `lean_initialize_thread'
          clang-16: error: linker command failed with exit code 1 (use -v to see invocation)

Without calling lean_initialize_thread, the whole example works with no problems.

The Reverse FFI example in the Lean repository calls for linking

$(OUT_DIR)/main: main.c lake | $(OUT_DIR)
# Add library paths for Lake package and for Lean itself
    cc -o $@ $< -I $(LEAN_SYSROOT)/include -L $(LEAN_LIBDIR) -L lib/.lake/build/lib -lRFFI -lInit_shared -lleanshared $(LINK_FLAGS)

and I currently have linker flags for libInit_shared.so and libleanshared.so. Is there anything I need to link against for this to work?

I also tried linking with libleanrt.a and it still has the same issue

[Leni Aniva]

The relevant linker flags are:

"-Wl,-Bdynamic" "-lleanshared" "-lInit_shared" "-lCallee" "-Wl,-Bstatic" "-lleanrt"

There are no errors from the linker about missing libraries so all these libraries were found

[Sebastian Ullrich]

This symbol only exists on master/4.8.0

[Leni Aniva]

Sebastian Ullrich said:

This symbol only exists on master/4.8.0

why is it in the FFI guide? is there an equivalent form of this symbol before 4.8.0?

[Jon Eugster]

I'd assume the docs follow the latest master.

Do you find what your looking for at this older version of the guide (v4.7.0-rc2)

[Leni Aniva]

Jon Eugster said:

I'd assume the docs follow the latest master.

Do you find what your looking for at this older version of the guide (v4.7.0-rc2)

There is no mention of calling Lean from multiple threads, and when I try to do it Lean segfaults

[Mac Malone]

@Leni Aniva yes, calling Lean from multiple threads in reverse FFI is a newly supported feature in master/4.8.0 with those new functions (e.g., lean_initialize_thread). It was added in lean4#3632.