diff --git a/math/lean4/Makefile b/math/lean4/Makefile index d36f0279a70f..2033d6a08123 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,84 +1,85 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v DISTVERSION= 4.29.0 +PORTREVISION= 1 CATEGORIES= math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment MAINTAINER= yuri@FreeBSD.org COMMENT= Theorem prover and functional language for math (new gen) WWW= https://lean-lang.org/ \ https://github.com/leanprover/lean4 LICENSE= APACHE20 LICENSE_FILE= ${WRKSRC}/LICENSE BROKEN_FreeBSD_13= compilation fails: error: use of undeclared identifier 'clearenv' BROKEN_armv7= compilation fails: ../../.build/stage1/lib/temp/Init/Coe.depend: No such file or directory BROKEN_i386= linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter) BUILD_DEPENDS= bash:shells/bash \ cadical:math/cadical LIB_DEPENDS= libgmp.so:math/gmp \ libuv.so:devel/libuv RUN_DEPENDS= cadical:math/cadical USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # ninja fails + gmake scripts are included in the project USE_GITHUB= yes GH_ACCOUNT= leanprover CFLAGS+= -fPIC CXXFLAGS+= -fPIC CMAKE_OFF= USE_MIMALLOC #MAKE_ARGS+= V=1 VERBOSE=1 MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} pre-everything:: @${ECHO_MSG} "" @${ECHO_MSG} "Please note that build Lean requires /proc to be mounted." @${ECHO_MSG} "" @${ECHO_MSG} " The usual way to do this is to add this line to /etc/fstab:" @${ECHO_MSG} " proc /proc procfs rw 0 0" @${ECHO_MSG} "" @${ECHO_MSG} " and then run this command as root:" @${ECHO_MSG} " # mount /proc" @${ECHO_MSG} "" post-patch: # Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files @${FIND} ${WRKSRC}/tests -name "lakefile.toml" | while read f; do \ ${GREP} -q "weakLeancArgs" "$$f" || \ ( ${PRINTF} 'weakLeancArgs = ["-fPIC"]\n\n' | cat - "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f" ); \ done # Add weakLeancArgs to lakefile.lean files that define packages @${FIND} ${WRKSRC}/tests -name "lakefile.lean" | while read f; do \ if ${GREP} -q "^package .* where" "$$f" && ! ${GREP} -q "weakLeancArgs" "$$f"; then \ ${AWK} '/^package .* where$$/ {print; print " weakLeancArgs := #[\"-fPIC\"]"; next} 1' "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f"; \ fi; \ done post-install: # remove empty dirs @${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete # remove stray files @${RM} ${STAGEDIR}${PREFIX}/LICENSE* # remove bin/cadical, workaround for https://github.com/leanprover/lean4/issues/5603 @${RM} ${STAGEDIR}${PREFIX}/bin/cadical # strip binaries @cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \ bin/lake \ bin/lean \ bin/leanc \ lib/lean/libInit_shared.so \ lib/lean/libleanshared.so \ lib/lean/libleanshared_1.so \ lib/lean/libLake_shared.so # tests as of 4.25.2-20251201: 100% tests passed, 0 tests failed out of 3367 # tests as of 4.29.0-rc2: 99% tests passed, 12 tests failed out of 3584, see https://github.com/leanprover/lean4/issues/12721 -# tests as of 4.29.0: 99% tests passed, 19 tests failed out of 3582 +# tests as of 4.29.0: 99% tests passed, 18 tests failed out of 3582 .include diff --git a/math/lean4/files/patch-src_runtime_stack__overflow.cpp b/math/lean4/files/patch-src_runtime_stack__overflow.cpp index e888a55cfead..15e3f049261b 100644 --- a/math/lean4/files/patch-src_runtime_stack__overflow.cpp +++ b/math/lean4/files/patch-src_runtime_stack__overflow.cpp @@ -1,14 +1,33 @@ ---- src/runtime/stack_overflow.cpp.orig 2025-11-18 02:29:21 UTC +--- src/runtime/stack_overflow.cpp.orig 2026-03-27 12:45:03 UTC +++ src/runtime/stack_overflow.cpp @@ -21,6 +21,11 @@ Port of the corresponding Rust code (see links below). #include #include "runtime/stack_overflow.h" +#if defined(__FreeBSD__) +#include +#define pthread_getattr_np pthread_attr_get_np +#endif + namespace lean { // stack guard of the main thread static stack_guard * g_stack_guard; +@@ -64,8 +69,18 @@ bool is_within_stack_guard(void * addr) { + #endif + // close enough; the actual guard might be bigger, but it's unlikely a Lean function will have stack frames that big + size_t guardsize = static_cast(sysconf(_SC_PAGESIZE)); ++#if defined(__FreeBSD__) ++ // On FreeBSD the guard page position depends on how the thread was created: ++ // - Main thread with ulimit: guard is below stackaddr (Linux-style, linux_check) ++ // - Spawned threads with explicit stacksize: guard is the first page of the ++ // region starting at stackaddr (freebsd_check) ++ // Accept either convention. ++ return (stackaddr - guardsize <= addr && addr < stackaddr) || ++ (stackaddr <= addr && addr < stackaddr + guardsize); ++#else + // the stack guard is *below* the stack + return stackaddr - guardsize <= addr && addr < stackaddr; ++#endif + } + + extern "C" LEAN_EXPORT void segv_handler(int signum, siginfo_t * info, void *) { 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 cb4949c8e4d2..c1fa5ae36845 100644 --- a/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp +++ b/math/lean4/files/patch-stage0_src_runtime_stack__overflow.cpp @@ -1,13 +1,32 @@ ---- stage0/src/runtime/stack_overflow.cpp.orig 2025-05-06 09:12:17 UTC +--- stage0/src/runtime/stack_overflow.cpp.orig 2026-03-27 12:45:03 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. Port of the corresponding Rust code (see links below). */ + +#include +#define pthread_getattr_np pthread_attr_get_np + #ifdef LEAN_WINDOWS #include #else +@@ -64,8 +68,18 @@ bool is_within_stack_guard(void * addr) { + #endif + // close enough; the actual guard might be bigger, but it's unlikely a Lean function will have stack frames that big + size_t guardsize = static_cast(sysconf(_SC_PAGESIZE)); ++#if defined(__FreeBSD__) ++ // On FreeBSD the guard page position depends on how the thread was created: ++ // - Main thread with ulimit: guard is below stackaddr (Linux-style, linux_check) ++ // - Spawned threads with explicit stacksize: guard is the first page of the ++ // region starting at stackaddr (freebsd_check) ++ // Accept either convention. ++ return (stackaddr - guardsize <= addr && addr < stackaddr) || ++ (stackaddr <= addr && addr < stackaddr + guardsize); ++#else + // the stack guard is *below* the stack + return stackaddr - guardsize <= addr && addr < stackaddr; ++#endif + } + + extern "C" LEAN_EXPORT void segv_handler(int signum, siginfo_t * info, void *) { diff --git a/math/lean4/files/run-tests-one-by-one.sh b/math/lean4/files/run-tests-one-by-one.sh new file mode 100755 index 000000000000..351b92009cb3 --- /dev/null +++ b/math/lean4/files/run-tests-one-by-one.sh @@ -0,0 +1,14 @@ +cd /usr/ports/math/lean4/work/lean4-`make -V PORTVERSION`/tests/lean/run +export PATH=/usr/ports/math/lean4/work/.build/stage1/bin:$PATH + +for t in letToHave.lean 983.lean ExprLens.lean try_heartbeats.lean collectLooseBVars.lean whereCmd.lean async_select_channel.lean; do + echo "==> Running test: $t" + result=$(bash test_single.sh $t 2>&1; echo "exit=$?") + echo "... output for $t: $result" + + if [ "$result" == "exit=0" ]; then + echo "<== Test $t passed." + else + echo "<== Test $t failed. Output: $result" + fi +done