CVS commit: pkgsrc/math/lean4

["Thomas Klausner" <wiz%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   wiz
Date:           Sat Jul 25 09:40:53 UTC 2026

Modified Files:
        pkgsrc/math/lean4: Makefile distinfo
Added Files:
        pkgsrc/math/lean4/patches: patch-src_include_lean_lean.h
            patch-stage0_src_include_lean_lean.h

Log Message:
lean4: fix alloca warning (during package build, and 'lake build')

The -std=gnu99 didn't help because alloca() was used in a C++ file.
Replace calls to alloca with __builtin_alloca instead, and get rid of
the forced gnu99.

Bump PKGREVISION.


To generate a diff of this commit:
cvs rdiff -u -r1.4 -r1.5 pkgsrc/math/lean4/Makefile
cvs rdiff -u -r1.2 -r1.3 pkgsrc/math/lean4/distinfo
cvs rdiff -u -r0 -r1.1 \
    pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h \
    pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

Modified files:

Index: pkgsrc/math/lean4/Makefile
diff -u pkgsrc/math/lean4/Makefile:1.4 pkgsrc/math/lean4/Makefile:1.5
--- pkgsrc/math/lean4/Makefile:1.4      Fri Jul 24 21:27:47 2026
+++ pkgsrc/math/lean4/Makefile  Sat Jul 25 09:40:53 2026
@@ -1,6 +1,7 @@
-# $NetBSD: Makefile,v 1.4 2026/07/24 21:27:47 wiz Exp $
+# $NetBSD: Makefile,v 1.5 2026/07/25 09:40:53 wiz Exp $
 
 DISTNAME=      lean4-4.32.1
+PKGREVISION=   1
 CATEGORIES=    math
 MASTER_SITES=  ${MASTER_SITE_GITHUB:=leanprover/}
 GITHUB_TAG=    v${PKGVERSION_NOREV}
@@ -17,10 +18,7 @@ DEPENDS+=    cadical>=3:../../math/cadical3
 USE_LANGUAGES= c c++
 USE_TOOLS+=    bash:run gmake pkg-config
 
-USE_CC_FEATURES=       c99
 USE_CXX_FEATURES=      c++20
-# for alloca()
-FORCE_C_STD=           gnu99
 
 # needed for stage0 tools that are called during build and installation
 MAKE_ENV+=     LD_LIBRARY_PATH=${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib/lean:${WRKSRC}/${CMAKE_BUILD_DIR}/stage0/lib

Index: pkgsrc/math/lean4/distinfo
diff -u pkgsrc/math/lean4/distinfo:1.2 pkgsrc/math/lean4/distinfo:1.3
--- pkgsrc/math/lean4/distinfo:1.2      Fri Jul 24 21:26:20 2026
+++ pkgsrc/math/lean4/distinfo  Sat Jul 25 09:40:53 2026
@@ -1,11 +1,13 @@
-$NetBSD: distinfo,v 1.2 2026/07/24 21:26:20 wiz Exp $
+$NetBSD: distinfo,v 1.3 2026/07/25 09:40:53 wiz Exp $
 
 BLAKE2s (lean4-4.32.1.tar.gz) = 9d98b0fcb0d958bdbbe110d108c6138c5e6f9c3e335dd16095761a13eb2da43e
 SHA512 (lean4-4.32.1.tar.gz) = c180c406c6d9b6c28705f93ac3fad64b1a975f76cc11ae8ba2b4447ff668e2babac2bf3dd997bae2a38b196767353b484b1674a6a21a145e9a37dc3879d3029f
 Size (lean4-4.32.1.tar.gz) = 75094335 bytes
 SHA1 (patch-src_CMakeLists.txt) = c6620d0ca4c6f5d2fccf4e8e97462661c1a9d38d
 SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
+SHA1 (patch-src_include_lean_lean.h) = 8051d7be7f01bb5a48974bcf777ea5bed0240f25
 SHA1 (patch-src_lake_Lake_Build_Common.lean) = 2fd83850d22ba26beb56b8bd26bb3473b897aee8
 SHA1 (patch-src_runtime_process.cpp) = fc4aeaf89ab47b0d0f6b086219a92fdc1badc2c4
 SHA1 (patch-stage0_src_CMakeLists.txt) = 9605c8287537786cec326e6d6f041faa4ce3f1ae
+SHA1 (patch-stage0_src_include_lean_lean.h) = 19e6c3e23705e03d6bb33e2e21330f007b64d761
 SHA1 (patch-stage0_src_runtime_process.cpp) = 2f4fe1485a110d545eb10bc57cd9dc9153e395c8

Added files:

Index: pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h
diff -u /dev/null pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h:1.1
--- /dev/null   Sat Jul 25 09:40:53 2026
+++ pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h     Sat Jul 25 09:40:53 2026
@@ -0,0 +1,19 @@
+$NetBSD: patch-src_include_lean_lean.h,v 1.1 2026/07/25 09:40:53 wiz Exp $
+
+Call compiler-provided alloca(). Fixes
+Warning: reference to the libc supplied alloca(3); this most likely will not work. Please use the compiler provided version of alloca(3), by supplying the appropriate compiler flags (e.g. 
-std=gnu99).
+
+--- src/include/lean/lean.h.orig       2026-07-25 09:24:11.724804692 +0000
++++ src/include/lean/lean.h
+@@ -37,7 +37,11 @@ extern "C" {
+ #include <stdnoreturn.h>
+ #define LEAN_NORETURN _Noreturn
+ #else
++#if defined(__GNUC__) || defined(__clang__)
++#define LEAN_ALLOCA(s) __builtin_alloca(s)
++#else
+ #define LEAN_ALLOCA(s) alloca(s)
++#endif
+ #define LEAN_NORETURN __attribute__((noreturn))
+ #endif
+ 
Index: pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h
diff -u /dev/null pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h:1.1
--- /dev/null   Sat Jul 25 09:40:53 2026
+++ pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h      Sat Jul 25 09:40:53 2026
@@ -0,0 +1,19 @@
+$NetBSD: patch-stage0_src_include_lean_lean.h,v 1.1 2026/07/25 09:40:53 wiz Exp $
+
+Call compiler-provided alloca(). Fixes
+Warning: reference to the libc supplied alloca(3); this most likely will not work. Please use the compiler provided version of alloca(3), by supplying the appropriate compiler flags (e.g. 
-std=gnu99).
+
+--- stage0/src/include/lean/lean.h.orig        2026-07-22 17:50:04.000000000 +0000
++++ stage0/src/include/lean/lean.h
+@@ -37,7 +37,11 @@ extern "C" {
+ #include <stdnoreturn.h>
+ #define LEAN_NORETURN _Noreturn
+ #else
++#if defined(__GNUC__) || defined(__clang__)
++#define LEAN_ALLOCA(s) __builtin_alloca(s)
++#else
+ #define LEAN_ALLOCA(s) alloca(s)
++#endif
+ #define LEAN_NORETURN __attribute__((noreturn))
+ #endif
+