git: 000e016f64cc - main - math/lean4: Fix stack overflow test

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
+done