lean4
lean4 copied to clipboard
macOS clang fails to link against dylib generated by Lean
% 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