CVS commit: pkgsrc/math/lean4
"Thomas Klausner" <[email protected]>
| Newsgroups | gmane.os.netbsd.devel.pkgsrc.cvs |
|---|---|
| Message-ID | <[email protected]> |
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.
(unnamed)
(text/x-diff, 4.2 KB)
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
+