From 2a891a3889a2cf1ac9e0499b4d11b596bfd9d410 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 3 Dec 2024 17:14:22 +0100
Subject: [PATCH] chore: `CMAKE_CXX_SYSROOT_FLAG` is also needed for linking
 (#6297)

Fixes #6296
---
 src/CMakeLists.txt | 17 +++++++++--------
 src/bin/leanc.in   |  2 +-
 src/util/ffi.cpp   |  2 +-
 3 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 7ad5d59766b4..95eece17470a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -122,7 +122,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
     # From https://emscripten.org/docs/compiling/WebAssembly.html#backends:
     # > The simple and safe thing is to pass all -s flags at both compile and link time.
     set(EMSCRIPTEN_SETTINGS "-s ALLOW_MEMORY_GROWTH=1 -fwasm-exceptions -pthread -flto")
-    string(APPEND LEANC_EXTRA_FLAGS " -pthread")
+    string(APPEND LEANC_EXTRA_CC_FLAGS " -pthread")
     string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_EMSCRIPTEN ${EMSCRIPTEN_SETTINGS}")
     string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${EMSCRIPTEN_SETTINGS}")
 endif()
@@ -157,11 +157,11 @@ if ((${MULTI_THREAD} MATCHES "ON") AND (${CMAKE_SYSTEM_NAME} MATCHES "Darwin"))
 endif ()
 
 # We want explicit stack probes in huge Lean stack frames for robust stack overflow detection
-string(APPEND LEANC_EXTRA_FLAGS " -fstack-clash-protection")
+string(APPEND LEANC_EXTRA_CC_FLAGS " -fstack-clash-protection")
 
 # This makes signed integer overflow guaranteed to match 2's complement.
 string(APPEND CMAKE_CXX_FLAGS " -fwrapv")
-string(APPEND LEANC_EXTRA_FLAGS " -fwrapv")
+string(APPEND LEANC_EXTRA_CC_FLAGS " -fwrapv")
 
 if(NOT MULTI_THREAD)
   message(STATUS "Disabled multi-thread support, it will not be safe to run multiple threads in parallel")
@@ -451,7 +451,7 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
     string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
   endif()
   string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
-  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fPIC")
   string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
   string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
@@ -464,7 +464,7 @@ elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath,@executable_path/../lib -Wl,-rpath,@executable_path/../lib/lean")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten")
   string(APPEND CMAKE_CXX_FLAGS " -fPIC")
-  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fPIC")
 elseif(${CMAKE_SYSTEM_NAME} MATCHES "Windows")
   string(APPEND LAKESHARED_LINKER_FLAGS " -Wl,--out-implib,${CMAKE_BINARY_DIR}/lib/lean/libLake_shared.dll.a -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/temp/libLake.a.export -Wl,--no-whole-archive")
 endif()
@@ -479,7 +479,7 @@ if(NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND NOT(${CMAKE_SYSTEM_NAME} MATC
   string(APPEND CMAKE_EXE_LINKER_FLAGS " -rdynamic")
   # hide all other symbols
   string(APPEND CMAKE_CXX_FLAGS " -fvisibility=hidden -fvisibility-inlines-hidden")
-  string(APPEND LEANC_EXTRA_FLAGS " -fvisibility=hidden")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " -fvisibility=hidden")
 endif()
 
 # On Windows, add bcrypt for random number generation
@@ -544,9 +544,10 @@ include_directories(${CMAKE_BINARY_DIR}/include)  # config.h etc., "public" head
 string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE)
 string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}")
 
-# Do embed flag for finding system libraries in dev builds
+# Do embed flag for finding system headers and libraries in dev builds
 if(CMAKE_OSX_SYSROOT AND NOT LEAN_STANDALONE)
-  string(APPEND LEANC_EXTRA_FLAGS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
+  string(APPEND LEANC_EXTRA_CC_FLAGS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
+  string(APPEND LEAN_EXTRA_LINKER_FLAGS " ${CMAKE_CXX_SYSROOT_FLAG}${CMAKE_OSX_SYSROOT}")
 endif()
 
 add_subdirectory(initialize)
diff --git a/src/bin/leanc.in b/src/bin/leanc.in
index 11fe5cdbf6f9..3307553435ec 100755
--- a/src/bin/leanc.in
+++ b/src/bin/leanc.in
@@ -7,7 +7,7 @@ for arg in "$@"; do
     [[ "$arg" = "-c" ]] && ldflags=()
     [[ "$arg" = "-v" ]] && v=1
 done
-cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument)
+cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_FLAGS@ @LEANC_INTERNAL_FLAGS@ "$@" "${ldflags[@]}" -Wno-unused-command-line-argument)
 cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g")
 [[ $v == 1 ]] && echo $cmd
 eval $cmd
diff --git a/src/util/ffi.cpp b/src/util/ffi.cpp
index ee8dcf77288d..be2f82d74547 100644
--- a/src/util/ffi.cpp
+++ b/src/util/ffi.cpp
@@ -10,7 +10,7 @@ Author: Sebastian Ullrich
 
 namespace lean {
 LEAN_EXPORT extern "C" object * lean_get_leanc_extra_flags(object *) {
-    return lean_mk_string("@LEANC_EXTRA_FLAGS@");
+    return lean_mk_string("@LEANC_EXTRA_CC_FLAGS@");
 }
 
 LEAN_EXPORT extern "C" object * lean_get_leanc_internal_flags(object *) {