diff options
| -rw-r--r-- | math/lean4/files/patch-src_bin_leanc.in | 11 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_runtime_io.cpp | 7 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_runtime_stack__overflow.cpp | 6 | ||||
| -rw-r--r-- | math/lean4/files/patch-src_shell_CMakeLists.txt | 8 | ||||
| -rw-r--r-- | math/lean4/files/patch-stage0_src_bin_leanc.in | 11 | ||||
| -rw-r--r-- | math/lean4/files/patch-stage0_src_shell_CMakeLists.txt | 8 |
6 files changed, 15 insertions, 36 deletions
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-src_shell_CMakeLists.txt b/math/lean4/files/patch-src_shell_CMakeLists.txt index 3858f69f9aa7..68de472208ff 100644 --- a/math/lean4/files/patch-src_shell_CMakeLists.txt +++ b/math/lean4/files/patch-src_shell_CMakeLists.txt @@ -1,11 +1,11 @@ ---- src/shell/CMakeLists.txt.orig 2025-11-17 18:29:21 UTC +--- src/shell/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +++ src/shell/CMakeLists.txt -@@ -57,7 +57,7 @@ if(${EMSCRIPTEN}) +@@ -57,7 +57,7 @@ endif() endif() # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers -set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") +set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") - set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${LEAN_BIN}) - + # LEAN TESTS + file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") 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_shell_CMakeLists.txt b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt index 075908dbdd63..bd9010ce3d9b 100644 --- a/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt +++ b/math/lean4/files/patch-stage0_src_shell_CMakeLists.txt @@ -1,11 +1,11 @@ ---- stage0/src/shell/CMakeLists.txt.orig 2025-11-17 18:29:21 UTC +--- stage0/src/shell/CMakeLists.txt.orig 2025-11-18 02:29:21 UTC +++ stage0/src/shell/CMakeLists.txt -@@ -57,7 +57,7 @@ if(${EMSCRIPTEN}) +@@ -57,7 +57,7 @@ endif() endif() # LEANC_OPTS in CXX is necessary for macOS c++ to find its headers -set(TEST_VARS "PATH=${LEAN_BIN}:$PATH ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") +set(TEST_VARS "PATH=${LEAN_BIN}:$PATH LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}/lib/lean:\${LD_LIBRARY_PATH:-} ${LEAN_TEST_VARS} CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}' LEANC_OPTS='${LEANC_OPTS}'") - set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${LEAN_BIN}) - + # LEAN TESTS + file(GLOB LEANTESTS "${LEAN_SOURCE_DIR}/../tests/lean/*.lean") |