--- src/CMakeLists.txt.orig 2026-02-24 00:20:30 UTC +++ src/CMakeLists.txt @@ -517,7 +517,7 @@ endif() string(APPEND LEAN_EXTRA_LINKER_FLAGS " -lm") endif() -if(CMAKE_SYSTEM_NAME MATCHES "Linux") +if(CMAKE_SYSTEM_NAME MATCHES "Linux|FreeBSD") if(BSYMBOLIC) string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") @@ -530,6 +530,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux") " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive" ) string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD") + if(BSYMBOLIC) + string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic") + 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 TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN") + string( + APPEND LAKESHARED_LINKER_FLAGS + " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive" + ) + string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=$ORIGIN/../lib:$ORIGIN/../lib/lean") elseif(CMAKE_SYSTEM_NAME MATCHES "Darwin") string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec") string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib") @@ -653,6 +666,9 @@ string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/inclu # Lean code only needs this one include string(APPEND LEANC_OPTS " -I${CMAKE_BINARY_DIR}/include") +# Include extra flags (e.g., -fPIC on FreeBSD) +string(APPEND LEANC_OPTS " ${LEANC_EXTRA_FLAGS}") + # Use CMake profile C++ flags for building Lean libraries, but do not embed in `leanc` string(TOUPPER "${CMAKE_BUILD_TYPE}" uppercase_CMAKE_BUILD_TYPE) string(APPEND LEANC_OPTS " ${CMAKE_CXX_FLAGS_${uppercase_CMAKE_BUILD_TYPE}}") @@ -939,7 +955,7 @@ install( install( DIRECTORY "${CMAKE_SOURCE_DIR}/" - DESTINATION src/lean + DESTINATION share/lean4/src/lean FILES_MATCHING PATTERN "*.lean" PATTERN "*.md"