--- src/CMakeLists.txt.orig	2026-10-12 15:51:15 UTC
+++ src/CMakeLists.txt
@@ -452,7 +452,7 @@ endif()
   endif()
 endif()
 
-include_directories(${CMAKE_BINARY_DIR}/include)
+include_directories(BEFORE ${CMAKE_BINARY_DIR}/include)
 
 # Pick up `llvm-config` to setup LLVM flags.
 if(LLVM)
@@ -594,7 +594,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")
@@ -611,6 +611,19 @@ if(CMAKE_SYSTEM_NAME MATCHES "Linux")
     " -Wl,--whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLake.a.export -Wl,--no-whole-archive ${CMAKE_BINARY_DIR}/lib/lean/libLeanExport.a.export -Wl,-soname=libLake_shared.so"
   )
   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")
@@ -783,6 +796,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}}")
@@ -1036,8 +1052,9 @@ if(NOT CMAKE_SYSTEM_NAME MATCHES "Emscripten")
     lean4lean
     PREFIX lean4lean
     EXCLUDE_FROM_ALL ON
-    GIT_REPOSITORY https://github.com/Kha/lean4lean
-    GIT_TAG lean4-bundle-4.35
+    SOURCE_DIR ${LEAN_SOURCE_DIR}/../ext/lean4lean
+    DOWNLOAD_COMMAND ""
+    UPDATE_COMMAND ""
     PATCH_COMMAND bash ${LEAN_SOURCE_DIR}/../script/lean4lean-minimal-init.sh
     CONFIGURE_COMMAND ""
     BUILD_COMMAND lake build lean4lean
@@ -1202,7 +1219,7 @@ install(
 
 install(
   DIRECTORY "${CMAKE_SOURCE_DIR}/"
-  DESTINATION src/lean
+  DESTINATION share/lean4/src/lean
   FILES_MATCHING
   PATTERN "*.lean"
   PATTERN "*.md"