lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

macOS clang fails to link against dylib generated by Lean

Open Kha opened this issue 1 year ago • 0 comments

% g++ test.cpp -o test -lleanshared -lreverseffiwithmathlib

ld: __DATA_CONST segment missing SG_READ_ONLY flag in '/Users/cruis/Documents/ReverseFFIwithMathlib/.lake/build/lib/libreverseffiwithmathlib.dylib'
clang: error: linker command failed with exit code 1 (use -v to see invocation)

from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Reverse.20FFI.20undefined.20reference.20for.20mathlib

We will likely need to upgrade to LLVM 16+ to fix this: https://github.com/llvm/llvm-project/commit/f7b752d27766ecf0241edfbdc4d7142fc40e7621

Kha avatar Oct 08 '24 08:10 Kha