From 9c7cb147b91fd1330764de7336c2ad2745e73f52 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 5 May 2025 16:59:50 +0200 Subject: [PATCH] fix: `extern_lib` and `precompileModules` on macOS (#8236) This PR fixes an issue where the combination of `extern_lib` and `precompileModules` would lead to "symbol not found" errors. --- src/CMakeLists.txt | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b95396d641..f074c862fc 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -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