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 11:24:52 UTC 2026

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

Log Message:
lean4: another patch filed upstream


To generate a diff of this commit:
cvs rdiff -u -r1.3 -r1.4 pkgsrc/math/lean4/distinfo
cvs rdiff -u -r1.1 -r1.2 \
    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, 3.3 KB)
Modified files:

Index: pkgsrc/math/lean4/distinfo
diff -u pkgsrc/math/lean4/distinfo:1.3 pkgsrc/math/lean4/distinfo:1.4
--- pkgsrc/math/lean4/distinfo:1.3	Sat Jul 25 09:40:53 2026
+++ pkgsrc/math/lean4/distinfo	Sat Jul 25 11:24:52 2026
@@ -1,13 +1,13 @@
-$NetBSD: distinfo,v 1.3 2026/07/25 09:40:53 wiz Exp $
+$NetBSD: distinfo,v 1.4 2026/07/25 11:24:52 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_include_lean_lean.h) = 017a9c5b5ac185a122a831f6fe4a64e94d9caad9
 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_include_lean_lean.h) = b138c9a082107a667ee3df0623c2ab0e6b2a546f
 SHA1 (patch-stage0_src_runtime_process.cpp) = 2f4fe1485a110d545eb10bc57cd9dc9153e395c8

Index: pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h
diff -u pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h:1.1 pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h:1.2
--- pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h:1.1	Sat Jul 25 09:40:53 2026
+++ pkgsrc/math/lean4/patches/patch-src_include_lean_lean.h	Sat Jul 25 11:24:52 2026
@@ -1,7 +1,8 @@
-$NetBSD: patch-src_include_lean_lean.h,v 1.1 2026/07/25 09:40:53 wiz Exp $
+$NetBSD: patch-src_include_lean_lean.h,v 1.2 2026/07/25 11:24:52 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).
+https://github.com/leanprover/lean4/pull/14543
 
 --- src/include/lean/lean.h.orig	2026-07-25 09:24:11.724804692 +0000
 +++ src/include/lean/lean.h
Index: pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h
diff -u pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h:1.1 pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h:1.2
--- pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h:1.1	Sat Jul 25 09:40:53 2026
+++ pkgsrc/math/lean4/patches/patch-stage0_src_include_lean_lean.h	Sat Jul 25 11:24:52 2026
@@ -1,7 +1,8 @@
-$NetBSD: patch-stage0_src_include_lean_lean.h,v 1.1 2026/07/25 09:40:53 wiz Exp $
+$NetBSD: patch-stage0_src_include_lean_lean.h,v 1.2 2026/07/25 11:24:52 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).
+https://github.com/leanprover/lean4/pull/14543
 
 --- stage0/src/include/lean/lean.h.orig	2026-07-22 17:50:04.000000000 +0000
 +++ stage0/src/include/lean/lean.h
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.