Linking issues when bumping `lean-cvc5` to v4.20.0-rc2

Stream: lean4

[George Pîrlea]

After updating to Mac OS 15.4.1, we've been hitting some linking issues that look like this (on Lean v4.19.0):

✖ [7/23] Building cvc5.Init
trace: .> LEAN_PATH=././.lake/build/lib/lean /Users/dranov/.elan/toolchains/leanprover--lean4---v4.19.0/bin/lean ././././cvc5/Init.lean -R ./././. -o ././.lake/build/lib/lean/cvc5/Init.olean -i ././.lake/build/lib/lean/cvc5/Init.ilean -c ././.lake/build/ir/cvc5/Init.c --load-dynlib ././.lake/build/lib/libffi.dylib --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(././.lake/build/lib/libffi.dylib, 0x0009): tried: '././.lake/build/lib/libffi.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS././.lake/build/lib/libffi.dylib' (no such file), '/Users/dranov/.elan/toolchains/leanprover--lean4---v4.19.0/lib/././.lake/build/lib/libffi.dylib' (no such file), '/Users/dranov/.elan/toolchains/leanprover--lean4---v4.19.0/lib/lean/././.lake/build/lib/libffi.dylib' (no such file), '/usr/lib/././.lake/build/lib/libffi.dylib' (no such file, not in dyld cache), '././.lake/build/lib/libffi.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/Users/dranov/src/lean-cvc5/.lake/build/lib/libffi.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag), '/System/Volumes/Preboot/Cryptexes/OS/Users/dranov/src/lean-cvc5/.lake/build/lib/libffi.dylib' (no such file), '/Users/dranov/src/lean-cvc5/.lake/build/lib/libffi.dylib' (__DATA_CONST segment missing SG_READ_ONLY flag)

The key part being (__DATA_CONST segment missing SG_READ_ONLY flag).

After updating to Lean v.4.20.0-rc2, we get errors that look like this:

✖ [7/23] Building cvc5.Init
trace: .> LEAN_PATH=/Users/dranov/src/lean-cvc5/.lake/build/lib/lean /Users/dranov/.elan/toolchains/leanprover--lean4---v4.20.0-rc2/bin/lean /Users/dranov/src/lean-cvc5/cvc5/Init.lean -R /Users/dranov/src/lean-cvc5 -o /Users/dranov/src/lean-cvc5/.lake/build/lib/lean/cvc5/Init.olean -i /Users/dranov/src/lean-cvc5/.lake/build/lib/lean/cvc5/Init.ilean -c /Users/dranov/src/lean-cvc5/.lake/build/ir/cvc5/Init.c --load-dynlib /Users/dranov/src/lean-cvc5/.lake/build/lib/libffi.dylib --json
info: stderr:
libc++abi: terminating due to uncaught exception of type lean::exception: error loading library, dlopen(/Users/dranov/src/lean-cvc5/.lake/build/lib/libffi.dylib, 0x0009): symbol not found in flat namespace '_except_err'
error: Lean exited with code 134

The key part being symbol not found in flat namespace '_except_err'. This seems to suggest that libffi is not properly (dynamically) linked with Lean, but I'm having a very hard time debugging this.

You can clone branch bump-v4.20.0-rc2 here, run lake run init, and then lake build to see the error.

Any idea what might be going on and how to fix it? Any help is greatly appreciated!

[Marcus Rossel]

I'm facing the same problem with lean-egg.

[Kim Morrison]

@George Pîrlea and @Marcus Rossel could you please try using the toolchain
leanprover/lean4-pr-releases:pr-release-8228?

[Kim Morrison]

also -- could you specify which OS you are seeing this on?

[Kim Morrison]

(deleting, trying to reproduce on a machine without basic things installed...)

[Kim Morrison]

@Marcus Rossel, if you have a branch on which you've tried updating to v4.20.0-rc2, could you post that so we can take a look? Just updating the toolchain on main hits many errors before anything looking like the above (e.g. starting with error: /home/kim/lean-egg/Lean/Egg/Tactic/Tags.lean:2:17: unknown constant 'Lean.HashMap').

[George Pîrlea]

@Kim Morrison

% sw_vers && xcode-select -v
ProductName:        macOS
ProductVersion:     15.4.1
BuildVersion:       24E263
xcode-select version 2409.

I'm seeing the same error (symbol not found in flat namespace) with leanprover/lean4-pr-releases:pr-release-8228.

[Yakov Pechersky]

Unfortunately, any Linux fix isn't going to affect macos due to the very different way that macos handles dynamic linking

[Yakov Pechersky]

What does otool -l .lake/build/lib/libffi.dylib give?

[Sebastian Ullrich]

The symbol is indeed listed as undefined there but it is not used by Lean at all... so I'm thinking this is a symbol in a system lib we're missing

[George Pîrlea]

@Sebastian Ullrich I think it's supposed to be a Lean symbol: https://github.com/abdoo8080/lean-cvc5/blob/main/ffi/ffi.cpp#L19

(This is not my code, so I'm not sure. Maybe @Abdalrhman M Mohamed can chime in.)

For what it's worth, I have no issues compiling the bump-v4.20.0-rc2 branch on x86_64 Ubuntu 24.04.1 LTS with glibc 2.39. The problem only arises on MacOS 15.4.1 (and did not arise on the immediately previous version I was on – 15.3.2 – from which I just upgraded today).

[George Pîrlea]

@Yakov Pechersky: otool-output.txt

[Sebastian Ullrich]

Oh! With two projects affected I didn't even consider this might be a project-local symbol. So let's see why we're not loading the implementation...

[Sebastian Ullrich]

Well we're loading the dynlib before we even get to compiling the file with the implementation, that certainly doesn't look correct. I think this is a question for @Mac Malone then how extern_lib interacts with precompileModules and what could have changed here.

[Cameron Zwarich]

@George Pîrlea What was the last version of the OS where this worked for you? Were you using 15.4.0 or something earlier?

[George Pîrlea]

@Cameron Zwarich I just checked /Library/Receipts/InstallHistory.plist and it seems I was previously on macOS 15.3.2.

[Sebastian Ullrich]

Thanks for the reports, this should be fixed by lean#8236

[George Pîrlea]

I can confirm that this works for me. Thank you very much @Sebastian Ullrich and everyone else!

[Kim Morrison]

Once #24621 has landed in Mathlib, Mathlib will be on v4.20.0-rc3, and hopefully the problems in this thread will be resolved.

[Marcus Rossel]

Building lean-egg on lean4:v4.20.0-rc3 works like a charm :innocent: Thanks for the quick fix!