Date: Sat, 28 Mar 2026 17:25:57 +0000 From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: 000e016f64cc - main - math/lean4: Fix stack overflow test Message-ID: <69c80f25.377c4.379d3367@gitrepo.freebsd.org>
index | next in thread | raw e-mail
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=000e016f64cc0b4fb7a483672c98adc451939c6d commit 000e016f64cc0b4fb7a483672c98adc451939c6d Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2026-03-28 17:20:55 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2026-03-28 17:25:55 +0000 math/lean4: Fix stack overflow test All other failing tests fail spuriously due to parallel contention. They all pass when run individually. --- math/lean4/Makefile | 3 ++- .../files/patch-src_runtime_stack__overflow.cpp | 21 ++++++++++++++++++++- .../patch-stage0_src_runtime_stack__overflow.cpp | 21 ++++++++++++++++++++- math/lean4/files/run-tests-one-by-one.sh | 14 ++++++++++++++ 4 files changed, 56 insertions(+), 3 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index d36f0279a70f..2033d6a08123 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,7 @@ 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 @@ -79,6 +80,6 @@ post-install: # 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 <bsd.port.mk> 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,4 +1,4 @@ ---- 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 <initializer_list> @@ -12,3 +12,22 @@ 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<size_t>(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,4 +1,4 @@ ---- 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. @@ -11,3 +11,22 @@ #ifdef LEAN_WINDOWS #include <windows.h> #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<size_t>(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 +donehome | help
Want to link to this message? Use this
URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?69c80f25.377c4.379d3367>