Update lean4-git to lean4-4.33.1nb20260821 lean actial version 4.35.0-pre, commit f6c7d68c7fc27e3b60585f30740c7d141d3c5b36, Release While here, allow for lake to actually link under NetBSD.

To: pkgsrc-wip-changes%NetBSD.org@localhost
Subject: Update lean4-git to lean4-4.33.1nb20260821 lean actial version 4.35.0-pre, commit f6c7d68c7fc27e3b60585f30740c7d141d3c5b36, Release While here, allow for lake to actually link under NetBSD.
From: ci4ic4 (via pkgsrc-wip) <commit-notify%pkgsrc.org@localhost>
Date: Fri, 21 Aug 2026 20:30:05 +0000
Module Name:	pkgsrc-wip
Committed By:	ci4ic4 <ci4ic4%gmail.com@localhost>
Pushed By:	ci4ic4
Date:		Fri Aug 21 21:27:10 2026 +0100
Changeset:	2b177c232ae9f8658e0db22ec2156f0a9e360bc5

Modified Files:
	lean4-git/Makefile
	lean4-git/PLIST
	lean4-git/distinfo

Log Message:
Update lean4-git to lean4-4.33.1nb20260821
lean actial version 4.35.0-pre,
commit f6c7d68c7fc27e3b60585f30740c7d141d3c5b36, Release
While here, allow for lake to actually link under NetBSD.

To see a diff of this commit:
https://wip.pkgsrc.org/cgi-bin/gitweb.cgi?p=pkgsrc-wip.git;a=commitdiff;h=2b177c232ae9f8658e0db22ec2156f0a9e360bc5

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

diffstat:
 lean4-git/Makefile |  6 ++---
 lean4-git/PLIST    | 72 ++++++++++++++++++++++++++++++++++++++----------------
 lean4-git/distinfo |  8 +++---
 3 files changed, 58 insertions(+), 28 deletions(-)

diffs:
diff --git a/lean4-git/Makefile b/lean4-git/Makefile
index df07cc0caa..833e4aa8da 100644
--- a/lean4-git/Makefile
+++ b/lean4-git/Makefile
@@ -1,6 +1,6 @@
-# $NetBSD: Makefile,v 1.8 2026/08/11 12:55:48 wiz Exp $
+# $NetBSD: Makefile,v 1.8 2026/08/21 12:55:48 wiz Exp $
 
-DISTNAME=	lean4-4.33.0
+DISTNAME=	lean4-4.33.1
 CATEGORIES=	math
 MASTER_SITES=	${MASTER_SITE_GITHUB:=leanprover/}
 #GITHUB_TAG=	v${PKGVERSION_NOREV}
@@ -47,7 +47,7 @@ SUBST_CLASSES+=		cc
 SUBST_FILES.cc+=	src/Leanc.lean
 SUBST_FILES.cc+=	src/lake/Lake/Build/Common.lean
 SUBST_SED.cc+=		-e "s,@LEANC_CC@,${CC},"
-SUBST_SED.cc+=		-e "s!@LINKER_FLAGS@!\"${COMPILER_RPATH_FLAG}${PREFIX}/lib\", \"${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean\"!"
+SUBST_SED.cc+=          -e "s!@LINKER_FLAGS@!\"${COMPILER_RPATH_FLAG}${PREFIX}/lib\", \"${COMPILER_RPATH_FLAG}${PREFIX}/lib/lean\", \"-lgcc_s\"!"
 SUBST_STAGE.cc=		pre-configure
 SUBST_MESSAGE.cc=	Setting compiler path.
 
diff --git a/lean4-git/PLIST b/lean4-git/PLIST
index 74eeeebd2d..602e24080a 100644
--- a/lean4-git/PLIST
+++ b/lean4-git/PLIST
@@ -7522,6 +7522,12 @@ lib/lean/Lean/Elab/Tactic/Grind/Have.ir.sig
 lib/lean/Lean/Elab/Tactic/Grind/Have.olean
 lib/lean/Lean/Elab/Tactic/Grind/Have.olean.private
 lib/lean/Lean/Elab/Tactic/Grind/Have.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.ilean
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.ir
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.ir.sig
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.olean
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/LetToHave.olean.server
 lib/lean/Lean/Elab/Tactic/Grind/LiftLet.ilean
 lib/lean/Lean/Elab/Tactic/Grind/LiftLet.ir
 lib/lean/Lean/Elab/Tactic/Grind/LiftLet.ir.sig
@@ -7822,6 +7828,12 @@ lib/lean/Lean/Elab/Tactic/VCGen.ir.sig
 lib/lean/Lean/Elab/Tactic/VCGen.olean
 lib/lean/Lean/Elab/Tactic/VCGen.olean.private
 lib/lean/Lean/Elab/Tactic/VCGen.olean.server
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.ilean
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.ir
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.ir.sig
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.olean
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.olean.private
+lib/lean/Lean/Elab/Tactic/VCGen/BinderName.olean.server
 lib/lean/Lean/Elab/Tactic/VCGen/Context.ilean
 lib/lean/Lean/Elab/Tactic/VCGen/Context.ir
 lib/lean/Lean/Elab/Tactic/VCGen/Context.ir.sig
@@ -7834,12 +7846,6 @@ lib/lean/Lean/Elab/Tactic/VCGen/Driver.ir.sig
 lib/lean/Lean/Elab/Tactic/VCGen/Driver.olean
 lib/lean/Lean/Elab/Tactic/VCGen/Driver.olean.private
 lib/lean/Lean/Elab/Tactic/VCGen/Driver.olean.server
-lib/lean/Lean/Elab/Tactic/VCGen/EPost.ilean
-lib/lean/Lean/Elab/Tactic/VCGen/EPost.ir
-lib/lean/Lean/Elab/Tactic/VCGen/EPost.ir.sig
-lib/lean/Lean/Elab/Tactic/VCGen/EPost.olean
-lib/lean/Lean/Elab/Tactic/VCGen/EPost.olean.private
-lib/lean/Lean/Elab/Tactic/VCGen/EPost.olean.server
 lib/lean/Lean/Elab/Tactic/VCGen/Entails.ilean
 lib/lean/Lean/Elab/Tactic/VCGen/Entails.ir
 lib/lean/Lean/Elab/Tactic/VCGen/Entails.ir.sig
@@ -9208,6 +9214,12 @@ lib/lean/Lean/Meta/Sym/IsClass.ir.sig
 lib/lean/Lean/Meta/Sym/IsClass.olean
 lib/lean/Lean/Meta/Sym/IsClass.olean.private
 lib/lean/Lean/Meta/Sym/IsClass.olean.server
+lib/lean/Lean/Meta/Sym/LetToHave.ilean
+lib/lean/Lean/Meta/Sym/LetToHave.ir
+lib/lean/Lean/Meta/Sym/LetToHave.ir.sig
+lib/lean/Lean/Meta/Sym/LetToHave.olean
+lib/lean/Lean/Meta/Sym/LetToHave.olean.private
+lib/lean/Lean/Meta/Sym/LetToHave.olean.server
 lib/lean/Lean/Meta/Sym/LiftLet.ilean
 lib/lean/Lean/Meta/Sym/LiftLet.ir
 lib/lean/Lean/Meta/Sym/LiftLet.ir.sig
@@ -15074,12 +15086,12 @@ lib/lean/Std/WP/Conjunctive.ir.sig
 lib/lean/Std/WP/Conjunctive.olean
 lib/lean/Std/WP/Conjunctive.olean.private
 lib/lean/Std/WP/Conjunctive.olean.server
-lib/lean/Std/WP/ExceptPost.ilean
-lib/lean/Std/WP/ExceptPost.ir
-lib/lean/Std/WP/ExceptPost.ir.sig
-lib/lean/Std/WP/ExceptPost.olean
-lib/lean/Std/WP/ExceptPost.olean.private
-lib/lean/Std/WP/ExceptPost.olean.server
+lib/lean/Std/WP/EStack.ilean
+lib/lean/Std/WP/EStack.ir
+lib/lean/Std/WP/EStack.ir.sig
+lib/lean/Std/WP/EStack.olean
+lib/lean/Std/WP/EStack.olean.private
+lib/lean/Std/WP/EStack.olean.server
 lib/lean/Std/WP/Frame.ilean
 lib/lean/Std/WP/Frame.ir
 lib/lean/Std/WP/Frame.ir.sig
@@ -15104,12 +15116,6 @@ lib/lean/Std/WP/Monad.ir.sig
 lib/lean/Std/WP/Monad.olean
 lib/lean/Std/WP/Monad.olean.private
 lib/lean/Std/WP/Monad.olean.server
-lib/lean/Std/WP/Monad/Adequacy.ilean
-lib/lean/Std/WP/Monad/Adequacy.ir
-lib/lean/Std/WP/Monad/Adequacy.ir.sig
-lib/lean/Std/WP/Monad/Adequacy.olean
-lib/lean/Std/WP/Monad/Adequacy.olean.private
-lib/lean/Std/WP/Monad/Adequacy.olean.server
 lib/lean/Std/WP/Monad/Basic.ilean
 lib/lean/Std/WP/Monad/Basic.ir
 lib/lean/Std/WP/Monad/Basic.ir.sig
@@ -15140,6 +15146,12 @@ lib/lean/Std/WP/Monad/Lemmas.ir.sig
 lib/lean/Std/WP/Monad/Lemmas.olean
 lib/lean/Std/WP/Monad/Lemmas.olean.private
 lib/lean/Std/WP/Monad/Lemmas.olean.server
+lib/lean/Std/WP/Monad/Sound.ilean
+lib/lean/Std/WP/Monad/Sound.ir
+lib/lean/Std/WP/Monad/Sound.ir.sig
+lib/lean/Std/WP/Monad/Sound.olean
+lib/lean/Std/WP/Monad/Sound.olean.private
+lib/lean/Std/WP/Monad/Sound.olean.server
 lib/lean/Std/WP/Triple.ilean
 lib/lean/Std/WP/Triple.ir
 lib/lean/Std/WP/Triple.ir.sig
@@ -15152,6 +15164,12 @@ lib/lean/Std/WP/Triple/Basic.ir.sig
 lib/lean/Std/WP/Triple/Basic.olean
 lib/lean/Std/WP/Triple/Basic.olean.private
 lib/lean/Std/WP/Triple/Basic.olean.server
+lib/lean/Std/WP/Triple/Conjunctive.ilean
+lib/lean/Std/WP/Triple/Conjunctive.ir
+lib/lean/Std/WP/Triple/Conjunctive.ir.sig
+lib/lean/Std/WP/Triple/Conjunctive.olean
+lib/lean/Std/WP/Triple/Conjunctive.olean.private
+lib/lean/Std/WP/Triple/Conjunctive.olean.server
 lib/lean/Std/WP/Triple/Monad.ilean
 lib/lean/Std/WP/Triple/Monad.ir
 lib/lean/Std/WP/Triple/Monad.ir.sig
@@ -16273,6 +16291,7 @@ src/lean/Lean/Elab/Tactic/Grind/DSimprocDSL.lean
 src/lean/Lean/Elab/Tactic/Grind/DSimprocDSLBuiltin.lean
 src/lean/Lean/Elab/Tactic/Grind/Filter.lean
 src/lean/Lean/Elab/Tactic/Grind/Have.lean
+src/lean/Lean/Elab/Tactic/Grind/LetToHave.lean
 src/lean/Lean/Elab/Tactic/Grind/LiftLet.lean
 src/lean/Lean/Elab/Tactic/Grind/Lint.lean
 src/lean/Lean/Elab/Tactic/Grind/LintExceptions.lean
@@ -16323,9 +16342,9 @@ src/lean/Lean/Elab/Tactic/TreeTacAttr.lean
 src/lean/Lean/Elab/Tactic/Try.lean
 src/lean/Lean/Elab/Tactic/Unfold.lean
 src/lean/Lean/Elab/Tactic/VCGen.lean
+src/lean/Lean/Elab/Tactic/VCGen/BinderName.lean
 src/lean/Lean/Elab/Tactic/VCGen/Context.lean
 src/lean/Lean/Elab/Tactic/VCGen/Driver.lean
-src/lean/Lean/Elab/Tactic/VCGen/EPost.lean
 src/lean/Lean/Elab/Tactic/VCGen/Entails.lean
 src/lean/Lean/Elab/Tactic/VCGen/FrameProc.lean
 src/lean/Lean/Elab/Tactic/VCGen/FrameProcAttr.lean
@@ -16554,6 +16573,7 @@ src/lean/Lean/Meta/Sym/InstantiateMVarsS.lean
 src/lean/Lean/Meta/Sym/InstantiateS.lean
 src/lean/Lean/Meta/Sym/Intro.lean
 src/lean/Lean/Meta/Sym/IsClass.lean
+src/lean/Lean/Meta/Sym/LetToHave.lean
 src/lean/Lean/Meta/Sym/LiftLet.lean
 src/lean/Lean/Meta/Sym/LitValues.lean
 src/lean/Lean/Meta/Sym/LooseBVarsS.lean
@@ -17534,19 +17554,20 @@ src/lean/Std/WP.lean
 src/lean/Std/WP/Assertion.lean
 src/lean/Std/WP/Basic.lean
 src/lean/Std/WP/Conjunctive.lean
-src/lean/Std/WP/ExceptPost.lean
+src/lean/Std/WP/EStack.lean
 src/lean/Std/WP/Frame.lean
 src/lean/Std/WP/Gadget/Assert.lean
 src/lean/Std/WP/Gadget/ForIn.lean
 src/lean/Std/WP/Monad.lean
-src/lean/Std/WP/Monad/Adequacy.lean
 src/lean/Std/WP/Monad/Basic.lean
 src/lean/Std/WP/Monad/Conjunctive.lean
 src/lean/Std/WP/Monad/Frame.lean
 src/lean/Std/WP/Monad/Instances.lean
 src/lean/Std/WP/Monad/Lemmas.lean
+src/lean/Std/WP/Monad/Sound.lean
 src/lean/Std/WP/Triple.lean
 src/lean/Std/WP/Triple/Basic.lean
+src/lean/Std/WP/Triple/Conjunctive.lean
 src/lean/Std/WP/Triple/Monad.lean
 src/lean/Std/WP/Triple/SpecLemmas.lean
 src/lean/cmake/Modules/README.md
@@ -17712,3 +17733,12 @@ src/lean/lake/Lake/Util/Version.lean
 src/lean/lake/Lake/Version.lean
 src/lean/lake/LakeMain.lean
 src/lean/lake/README.md
+@pkgdir src/lean/util
+@pkgdir src/lean/shell
+@pkgdir src/lean/runtime/uv
+@pkgdir src/lean/library/constructions
+@pkgdir src/lean/lake/schemas
+@pkgdir src/lean/kernel
+@pkgdir src/lean/initialize
+@pkgdir src/lean/include/lean
+@pkgdir src/lean/bin
diff --git a/lean4-git/distinfo b/lean4-git/distinfo
index 047afa37b0..38f42c3b7e 100644
--- a/lean4-git/distinfo
+++ b/lean4-git/distinfo
@@ -1,8 +1,8 @@
-$NetBSD: distinfo,v 1.6 2026/08/11 12:55:48 wiz Exp $
+$NetBSD$
 
-BLAKE2s (lean4-4.33.0.tar.gz) = b927ea9d3bb6b62527cecdf4c898702d0783a2a2328413b6d2f6b9b74bab5953
-SHA512 (lean4-4.33.0.tar.gz) = 76cc04f43fd25c482fab228264ed69045e2fe1c0b4de265d43d74a2565f18467393e76002f2029016a86d7ec90e1a5ec585f328a60556cd0d4003c4a710a7b5e
-Size (lean4-4.33.0.tar.gz) = 86677749 bytes
+BLAKE2s (lean4-4.33.1.tar.gz) = 8639ccf7f54d47e4e90e21cd266b71698f7f9009fb2126b48553195308a4d335
+SHA512 (lean4-4.33.1.tar.gz) = 72808891827abfa02c52e15cf64fc96c48a02738f5aac0331a009772512e8cad0cae18373615a734e850328d8422d32e374289805bfcaef2852efc8234867c76
+Size (lean4-4.33.1.tar.gz) = 86700313 bytes
 SHA1 (patch-src_CMakeLists.txt) = c6620d0ca4c6f5d2fccf4e8e97462661c1a9d38d
 SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
 SHA1 (patch-src_include_lean_lean.h) = 017a9c5b5ac185a122a831f6fe4a64e94d9caad9
Prev by Date: modular-xorg-xephyr: add conversion to meson
Next by Date: ocaml: Note test failures remain
Previous by Thread: modular-xorg-xephyr: add conversion to meson
Next by Thread: ocaml: Note test failures remain
Indexes:
Home | Main Index | Thread Index | Old Index