ld64.lld: error: undefined symbol: _lean_alloc_mpz

Stream: lean4

[Ramon Fernández Mir]

I'm trying to use the FFI together with GMP but I get the following error when I lake build:

[0/4] Compiling ffigmp.c
[0/4] Creating libffigmp.a
[0/4] Linking libffigmp.dylib
stderr:
ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
[0/4] Building FFIGMP
[1/4] Compiling FFIGMP
[1/4] Building Main
[2/4] Compiling Main
[4/4] Linking fFIGMP
error: > /Users/ramonfernandezmir/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/leanc -o ./build/bin/fFIGMP ./build/ir/Main.o ./build/ir/FFIGMP.o ./build/lib/libffigmp.a -lgmp
error: stderr:
ld64.lld: warning: directory not found for option -L/Applications/Xcode_14.2.app/Contents/Developer/Platforms/MacOSX.platform/Developer/SDKs/MacOSX13.1.sdk/usr/lib
ld64.lld: warning: /usr/lib/system/libsystem_kernel.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_platform.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: warning: /usr/lib/system/libsystem_pthread.dylib has version 13.4.0, which is newer than target minimum of 13.0.0
ld64.lld: error: undefined symbol: _lean_alloc_mpz
>>> referenced by ./build/lib/libffigmp.a(ffigmp.o):(symbol _my_fun+0x3c)
clang: error: linker command failed with exit code 1 (use -v to see invocation)
error: external command `/Users/ramonfernandezmir/.elan/toolchains/leanprover--lean4---nightly-2023-06-20/bin/leanc` exited with code 1

This is from a mwe I uploaded to https://github.com/ramonfmir/FFIGMP . The C code is simply:

#include <lean/lean.h>
#include <lean/lean_gmp.h>

lean_obj_res my_fun(lean_obj_arg x) {
    mpz_t y;
    mpz_init(y);
    mpz_set_ui(y, 123);
    return lean_alloc_mpz(y);
}

I'm running it on an M1 mac with Lean installed natively. I'm pretty sure that the exact same approach worked a couple of months ago but I think I was running it with Rosetta and on an older Mac OS version. The warnings are also new, I noticed some other people are experiencing the same recently (#new members > Warnings from lake build on macOS , #lean4 > error: permission denied ), I wonder if it's related.

[Sebastian Ullrich]

ARM releases are not linked against GMP, see LEAN_USE_GMP references in the Lean source

[Ramon Fernández Mir]

Ah, I see, so the only way to make this work on my machine is to use Rosetta?

[Sebastian Ullrich]

What is your goal? Eventually no version of Lean 4 will use GMP, but you could still use GMP internally in your library

[Ramon Fernández Mir]

I'm using another library (Arblib) that depends on GMP and I want an interface to it from Lean.

[Sebastian Ullrich]

You could use Rosetta for now, but if you want to make your code future-proof, you should translate between Lean's representation and GMP's. Which you would probably be the first one to do!

[Ramon Fernández Mir]

Right, so if I assume that at the interface level I have regular Nats/Ints (which is probably a fair assumption) then I can get rid of lean_alloc_mpz/lean_extract_mpz_value but I still can use GMP at the library level and it all works nicely.

[Ramon Fernández Mir]

Sebastian Ullrich said:

You could use Rosetta for now, but if you want to make your code future-proof, you should translate between Lean's representation and GMP's. Which you would probably be the first one to do!

Or I guess I could do that, it seems like a bit more work though hahah