ld64.lld dynamic link errors on MacOS

Stream: lean4

[Xubai Wang]

When I try to link to a dynamic lib on MacOS (like this), leanc gives me a LC_DYLD_INFO_ONLY error, followed with a bunch of undefined symbols. The error looks like:

$ lake build
> /Users/xubaiw/.elan/toolchains/leanprover--lean4---nightly-2022-03-01/bin/leanc -o ./build/bin/foo ./build/ir/Main.o ./../.././build/ir/OpenSSL.o ./../.././build/bindings/libopenssl-shim.a /usr/local/Cellar//openssl@3/3.0.1//lib/libssl.dylib /usr/local/Cellar//openssl@3/3.0.1//lib/libcrypto.dylib
error: ld64.lld: error: LC_DYLD_INFO_ONLY not found in /usr/local/Cellar//openssl@3/3.0.1//lib/libssl.dylib
ld64.lld: error: LC_DYLD_INFO_ONLY not found in /usr/local/Cellar//openssl@3/3.0.1//lib/libcrypto.dylib

ld64.lld: error: undefined symbol: _ERR_print_errors_fp
>>> referenced by ./../.././build/bindings/libopenssl-shim.a(openssl-shim.o)

ld64.lld: error: undefined symbol: _SSL_set_bio
...

While it successfully builds when I manually link them with system clang (with --print-ldflags).

$ clang -o ./build/bin/foo ./build/ir/Main.o ./../.././build/ir/OpenSSL.o ./../.././build/bindings/libopenssl-shim.a /usr/local/Cellar//openssl@3/3.0.1//lib/libssl.dylib /usr/local/Cellar//openssl@3/3.0.1//lib/libcrypto.dylib $(leanc --print-ldflags)
$ ./build/bin/foo
Hello, OpenSSL

So I suppose the problem arises from ld64.lld. Any idea to solve this error?

[Xubai Wang]

The code also builds when linked to libcrypto.a static lib.

[Xubai Wang]

Now not sure if it's a general problem with all dynamic linking or just a OpenSSL specific problem. I'll try to work out a smaller example later tonight.

[Xubai Wang]

:thinking: Things just go more interesting when I try to minimize the problem with two lean packages, one package compiled to shared lib and the other dynamically linked to that lib.

This time dyld gives Library not loaded when I run the binary. It seems that leanc fails to link shared lib (but system clang also fails in this example).

This example is made cross-platform, so you can test if it can work on other platforms.

[Sebastian Ullrich]

That just sounds like standard library lookup troubles. Try passing the library file path directly to the linker without -l/-L, or run the executable with DYLD_LIBRARY_PATH set to the library's folder.

[Xubai Wang]

I have tried directly passing (using moreLibTargets only) and that didn't work though. DYLD_LIBRARY_PATH can run the executable but leads to a segfault.

[Xubai Wang]

For the segfault, is there any problem with this?

@[export bar1_greet] def greet (name : String) := s!"Hello, {name}!"

@[extern "bar1_greet"] constant greet' : String → String

[Sebastian Ullrich]

Not per se, as long as you call initialize_bar1 first

[Sebastian Ullrich]

Xubai Wang said:

When I try to link to a dynamic lib on MacOS (like this), leanc gives me a LC_DYLD_INFO_ONLY error, followed with a bunch of undefined symbols.

I encountered the same issue while assembling https://github.com/leanprover/lean4/pull/1076. Apparently Apple's linker recently switched to a different header format, which lld does not yet support: https://github.com/llvm/llvm-project/issues/54550
This shouldn't really matter in practice if you're also planning to distribute your software to machines running older versions of macOS, which would not understand the new format anyway. However, it turns out that Homebrew is not a great tool if you're planning to do that:https://news.ycombinator.com/item?id=12549208

[Sebastian Ullrich]

This should be fixed in the next LLVM release https://github.com/llvm/llvm-project/commit/94e0f8e001002b828c42048f383806295e7abbb2

[Ramon Fernández Mir]

Did you manage to fix the LC_DYLD_INFO_ONLY linker error? @Xubai Wang