summaryrefslogtreecommitdiff
path: root/math/lean4/files
diff options
context:
space:
mode:
Diffstat (limited to 'math/lean4/files')
-rw-r--r--math/lean4/files/patch-src_CMakeLists.txt17
-rw-r--r--math/lean4/files/patch-src_bin_leanc.in11
-rw-r--r--math/lean4/files/patch-src_runtime_io.cpp7
-rw-r--r--math/lean4/files/patch-src_runtime_stack__overflow.cpp6
-rw-r--r--math/lean4/files/patch-stage0_src_CMakeLists.txt17
-rw-r--r--math/lean4/files/patch-stage0_src_bin_leanc.in11
-rw-r--r--math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp8
-rw-r--r--math/lean4/files/patch-tests_lakefile.toml10
8 files changed, 45 insertions, 42 deletions
diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt
index d7658e68a521..d71c117b8802 100644
--- a/math/lean4/files/patch-src_CMakeLists.txt
+++ b/math/lean4/files/patch-src_CMakeLists.txt
@@ -1,6 +1,6 @@
---- src/CMakeLists.txt.orig 2025-05-07 10:26:21 UTC
+--- src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC
+++ src/CMakeLists.txt
-@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
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")
@@ -14,10 +14,21 @@
+ 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")
++ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]")
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")
-@@ -801,7 +811,7 @@ endif()
+@@ -586,6 +597,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}}")
+@@ -814,7 +828,7 @@ endif()
file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
endif()
diff --git a/math/lean4/files/patch-src_bin_leanc.in b/math/lean4/files/patch-src_bin_leanc.in
deleted file mode 100644
index 6b110ae220b3..000000000000
--- a/math/lean4/files/patch-src_bin_leanc.in
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/bin/leanc.in.orig 2025-05-07 10:26:21 UTC
-+++ src/bin/leanc.in
-@@ -7,7 +7,7 @@ done
- [[ "$arg" = "-c" ]] && ldflags=()
- [[ "$arg" = "-v" ]] && v=1
- done
--cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_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 -fPIC)
- cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g")
- [[ $v == 1 ]] && echo $cmd
- eval $cmd
diff --git a/math/lean4/files/patch-src_runtime_io.cpp b/math/lean4/files/patch-src_runtime_io.cpp
index 2e185dfb816c..8fe17f4e138b 100644
--- a/math/lean4/files/patch-src_runtime_io.cpp
+++ b/math/lean4/files/patch-src_runtime_io.cpp
@@ -1,12 +1,11 @@
---- src/runtime/io.cpp.orig 2025-05-06 09:12:17 UTC
+--- src/runtime/io.cpp.orig 2025-11-18 02:29:21 UTC
+++ src/runtime/io.cpp
-@@ -1253,7 +1253,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar
+@@ -1365,7 +1365,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar
char dest[PATH_MAX];
memset(dest, 0, PATH_MAX);
pid_t pid = getpid();
-- snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
+#if defined(__linux__)
-+ snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
+ snprintf(path, PATH_MAX, "/proc/%d/exe", pid);
+#elif defined(__FreeBSD__)
+ snprintf(path, PATH_MAX, "/proc/%d/file", pid);
+#else
diff --git a/math/lean4/files/patch-src_runtime_stack__overflow.cpp b/math/lean4/files/patch-src_runtime_stack__overflow.cpp
index cdd63ffde32a..e888a55cfead 100644
--- a/math/lean4/files/patch-src_runtime_stack__overflow.cpp
+++ b/math/lean4/files/patch-src_runtime_stack__overflow.cpp
@@ -1,11 +1,13 @@
---- src/runtime/stack_overflow.cpp.orig 2025-05-06 09:12:17 UTC
+--- src/runtime/stack_overflow.cpp.orig 2025-11-18 02:29:21 UTC
+++ src/runtime/stack_overflow.cpp
-@@ -21,6 +21,9 @@ Port of the corresponding Rust code (see links below).
+@@ -21,6 +21,11 @@ Port of the corresponding Rust code (see links below).
#include <initializer_list>
#include "runtime/stack_overflow.h"
++#if defined(__FreeBSD__)
+#include <pthread_np.h>
+#define pthread_getattr_np pthread_attr_get_np
++#endif
+
namespace lean {
// stack guard of the main thread
diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt
index 184415ffa3d9..7ec7241aa2f2 100644
--- a/math/lean4/files/patch-stage0_src_CMakeLists.txt
+++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt
@@ -1,6 +1,6 @@
---- stage0/src/CMakeLists.txt.orig 2025-05-06 09:12:17 UTC
+--- stage0/src/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC
+++ stage0/src/CMakeLists.txt
-@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+@@ -473,6 +473,17 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
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")
@@ -14,10 +14,21 @@
+ 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")
++ set(LEAN_EXTRA_LAKEFILE_TOML "weakLeancArgs = [\"-fPIC\"]")
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")
-@@ -798,7 +808,7 @@ endif()
+@@ -586,6 +597,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}}")
+@@ -814,7 +828,7 @@ endif()
file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
endif()
diff --git a/math/lean4/files/patch-stage0_src_bin_leanc.in b/math/lean4/files/patch-stage0_src_bin_leanc.in
deleted file mode 100644
index a6f3f345b929..000000000000
--- a/math/lean4/files/patch-stage0_src_bin_leanc.in
+++ /dev/null
@@ -1,11 +0,0 @@
---- stage0/src/bin/leanc.in.orig 2025-05-07 10:26:21 UTC
-+++ stage0/src/bin/leanc.in
-@@ -7,7 +7,7 @@ done
- [[ "$arg" = "-c" ]] && ldflags=()
- [[ "$arg" = "-v" ]] && v=1
- done
--cmd=(${LEAN_CC:-@CMAKE_C_COMPILER@} "-I$root/include" @LEANC_EXTRA_CC_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 -fPIC)
- cmd=$(printf '%q ' "${cmd[@]}" | sed "s!ROOT!$root!g")
- [[ $v == 1 ]] && echo $cmd
- eval $cmd
diff --git a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp
index 638daf3af176..cb4949c8e4d2 100644
--- a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp
+++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp
@@ -11,11 +11,3 @@
#ifdef LEAN_WINDOWS
#include <windows.h>
#else
-@@ -20,6 +24,7 @@ Port of the corresponding Rust code (see links below).
- #include <lean/lean.h>
- #include <initializer_list>
- #include "runtime/stack_overflow.h"
-+
-
- namespace lean {
- // stack guard of the main thread
diff --git a/math/lean4/files/patch-tests_lakefile.toml b/math/lean4/files/patch-tests_lakefile.toml
new file mode 100644
index 000000000000..3a01b013943d
--- /dev/null
+++ b/math/lean4/files/patch-tests_lakefile.toml
@@ -0,0 +1,10 @@
+--- tests/lakefile.toml.orig 2025-11-17 18:29:21 UTC
++++ tests/lakefile.toml
+@@ -1,5 +1,7 @@
+ name = "tests"
+
++weakLeancArgs = ["-fPIC"]
++
+ # Allow `module` in tests when opened in the language server.
+ # Enabled during actual test runs in the respective test_single.sh.
+ moreGlobalServerArgs = ["-Dexperimental.module=true"]
generated by cgit v1.2.3 (git 2.25.1) at 2025-12-16 13:07:23 +0000