max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: extern_lib and precompileModules on macOS (#8236)

Browse source 
This PR fixes an issue where the combination of `extern_lib` and
`precompileModules` would lead to "symbol not found" errors.
This commit is contained in:
Sebastian Ullrich 2025-05-05 16:59:50 +02:00 • committed by GitHub
parent 9576e48e1a
commit 9c7cb147b9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/CMakeLists.txt
View file

@ -511,7 +511,10 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
# import libraries created by the stdlib.make targets
string(APPEND LEANC_SHARED_LINKER_FLAGS " -lInit_shared -lleanshared_1 -lleanshared")
elseif("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin")
string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup")
# The second flag is necessary to even *load* dylibs without resolved symbols, as can happen
# if a Lake `extern_lib` depends on a symbols defined by the Lean library but is loaded even
# before definition.
string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-undefined,dynamic_lookup -Wl,-no_fixup_chains")
endif()
# Linux ignores undefined symbols in shared libraries by default