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.txt13
-rw-r--r--math/lean4/files/patch-src_bin_leanc.in11
-rw-r--r--math/lean4/files/patch-src_runtime_io.cpp4
-rw-r--r--math/lean4/files/patch-src_runtime_process.cpp22
-rw-r--r--math/lean4/files/patch-src_runtime_stack__overflow.cpp6
-rw-r--r--math/lean4/files/patch-stage0_src_CMakeLists.txt13
-rw-r--r--math/lean4/files/patch-stage0_src_bin_leanc.in11
-rw-r--r--math/lean4/files/patch-stage0_src_runtime_io.cpp4
-rw-r--r--math/lean4/files/patch-stage0_src_runtime_process.cpp22
-rw-r--r--math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp6
10 files changed, 90 insertions, 22 deletions
diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt
index 98298fd62d75..d7658e68a521 100644
--- a/math/lean4/files/patch-src_CMakeLists.txt
+++ b/math/lean4/files/patch-src_CMakeLists.txt
@@ -1,9 +1,9 @@
---- src/CMakeLists.txt.orig 2024-03-06 02:11:32 UTC
+--- src/CMakeLists.txt.orig 2025-05-07 10:26:21 UTC
+++ src/CMakeLists.txt
-@@ -362,6 +362,15 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
- string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
- string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+ 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 "FreeBSD")
+ if(BSYMBOLIC)
+ string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
@@ -12,11 +12,12 @@
+ 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 CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
++ 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")
-@@ -624,7 +633,7 @@ endif()
+@@ -801,7 +811,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
new file mode 100644
index 000000000000..6b110ae220b3
--- /dev/null
+++ b/math/lean4/files/patch-src_bin_leanc.in
@@ -0,0 +1,11 @@
+--- 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 767ad0a1625f..2e185dfb816c 100644
--- a/math/lean4/files/patch-src_runtime_io.cpp
+++ b/math/lean4/files/patch-src_runtime_io.cpp
@@ -1,6 +1,6 @@
---- src/runtime/io.cpp.orig 2024-01-13 17:13:25 UTC
+--- src/runtime/io.cpp.orig 2025-05-06 09:12:17 UTC
+++ src/runtime/io.cpp
-@@ -855,7 +855,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar
+@@ -1253,7 +1253,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();
diff --git a/math/lean4/files/patch-src_runtime_process.cpp b/math/lean4/files/patch-src_runtime_process.cpp
new file mode 100644
index 000000000000..b13998f4743f
--- /dev/null
+++ b/math/lean4/files/patch-src_runtime_process.cpp
@@ -0,0 +1,22 @@
+--- src/runtime/process.cpp.orig 2025-05-06 09:12:17 UTC
++++ src/runtime/process.cpp
+@@ -31,6 +31,10 @@ Author: Jared Roesch
+ #include <sys/syscall.h>
+ #endif
+
++#ifdef __FreeBSD__
++#include <pthread_np.h>
++#endif
++
+ #include "runtime/object.h"
+ #include "runtime/io.h"
+ #include "runtime/array_ref.h"
+@@ -342,6 +346,8 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg
+ lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
+ #elif defined(LEAN_EMSCRIPTEN)
+ tid = 0;
++#elif defined(__FreeBSD__)
++ tid = (pid_t)pthread_getthreadid_np();
+ #else
+ // since Linux 2.4.11, our glibc 2.27 requires at least 3.2
+ // glibc 2.30 would provide a wrapper
diff --git a/math/lean4/files/patch-src_runtime_stack__overflow.cpp b/math/lean4/files/patch-src_runtime_stack__overflow.cpp
index 06914304dbaa..cdd63ffde32a 100644
--- a/math/lean4/files/patch-src_runtime_stack__overflow.cpp
+++ b/math/lean4/files/patch-src_runtime_stack__overflow.cpp
@@ -1,7 +1,7 @@
---- src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC
+--- src/runtime/stack_overflow.cpp.orig 2025-05-06 09:12:17 UTC
+++ src/runtime/stack_overflow.cpp
-@@ -20,6 +20,9 @@ Port of the corresponding Rust code (see links below).
- #include <lean/lean.h>
+@@ -21,6 +21,9 @@ Port of the corresponding Rust code (see links below).
+ #include <initializer_list>
#include "runtime/stack_overflow.h"
+#include <pthread_np.h>
diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt
index ec7e8f739ef0..184415ffa3d9 100644
--- a/math/lean4/files/patch-stage0_src_CMakeLists.txt
+++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt
@@ -1,9 +1,9 @@
---- stage0/src/CMakeLists.txt.orig 2024-03-06 02:11:32 UTC
+--- stage0/src/CMakeLists.txt.orig 2025-05-06 09:12:17 UTC
+++ stage0/src/CMakeLists.txt
-@@ -362,6 +362,15 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
- string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
+@@ -472,6 +472,16 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
- string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+ 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 "FreeBSD")
+ if(BSYMBOLIC)
+ string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
@@ -12,11 +12,12 @@
+ 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 CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
++ 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")
-@@ -624,7 +633,7 @@ endif()
+@@ -798,7 +808,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
new file mode 100644
index 000000000000..a6f3f345b929
--- /dev/null
+++ b/math/lean4/files/patch-stage0_src_bin_leanc.in
@@ -0,0 +1,11 @@
+--- 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_io.cpp b/math/lean4/files/patch-stage0_src_runtime_io.cpp
index 67d799f2a916..9b00b760a7a8 100644
--- a/math/lean4/files/patch-stage0_src_runtime_io.cpp
+++ b/math/lean4/files/patch-stage0_src_runtime_io.cpp
@@ -1,6 +1,6 @@
---- stage0/src/runtime/io.cpp.orig 2024-01-13 09:36:50 UTC
+--- stage0/src/runtime/io.cpp.orig 2025-05-06 09:12:17 UTC
+++ stage0/src/runtime/io.cpp
-@@ -855,7 +855,13 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_ar
+@@ -1253,7 +1253,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();
diff --git a/math/lean4/files/patch-stage0_src_runtime_process.cpp b/math/lean4/files/patch-stage0_src_runtime_process.cpp
new file mode 100644
index 000000000000..8b8fb1a9e008
--- /dev/null
+++ b/math/lean4/files/patch-stage0_src_runtime_process.cpp
@@ -0,0 +1,22 @@
+--- stage0/src/runtime/process.cpp.orig 2025-05-06 09:12:17 UTC
++++ stage0/src/runtime/process.cpp
+@@ -31,6 +31,10 @@ Author: Jared Roesch
+ #include <sys/syscall.h>
+ #endif
+
++#ifdef __FreeBSD__
++#include <pthread_np.h>
++#endif
++
+ #include "runtime/object.h"
+ #include "runtime/io.h"
+ #include "runtime/array_ref.h"
+@@ -342,6 +346,8 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg
+ lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
+ #elif defined(LEAN_EMSCRIPTEN)
+ tid = 0;
++#elif defined(__FreeBSD__)
++ tid = (pid_t)pthread_getthreadid_np();
+ #else
+ // since Linux 2.4.11, our glibc 2.27 requires at least 3.2
+ // glibc 2.30 would provide a wrapper
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 5296c0cf49c2..638daf3af176 100644
--- a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp
+++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp
@@ -1,4 +1,4 @@
---- stage0/src/runtime/stack_overflow.cpp.orig 2023-12-21 22:11:33 UTC
+--- stage0/src/runtime/stack_overflow.cpp.orig 2025-05-06 09:12:17 UTC
+++ stage0/src/runtime/stack_overflow.cpp
@@ -7,6 +7,10 @@ Port of the corresponding Rust code (see links below).
Print a nicer error message on stack overflow.
@@ -11,9 +11,9 @@
#ifdef LEAN_WINDOWS
#include <windows.h>
#else
-@@ -19,6 +23,7 @@ Port of the corresponding Rust code (see links below).
- #include <cstring>
+@@ -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"
+
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-15 12:48:48 +0000