pkgsrc-Changes archive
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index][Old Index]
CVS commit: pkgsrc/math/lean4
Module Name: pkgsrc
Committed By: wiz
Date: Sat Sep 26 11:04:54 UTC 2026
Modified Files:
pkgsrc/math/lean4: Makefile PLIST distinfo
Log Message:
lean4: update to 4.34.1.
4.34.1
This patch release contains multiple runtime fixes
4.34.0
Lean 4.34.0 focuses on the kernel: three soundness issues, found
with AI adversarial testing, have been analyzed and fixed, and a
series of additional defensive checks have been implemented for
further reinforcement. In the automation side, bv_decide gets
integrated with sym and grind interactive modes, while being ported
to the SymM preprocessor that makes it up to six times faster. Work
has continued on the floating-point API after Float and Float32
models being introduced in 4.33.0; linters can now carry state
across commands and attach code actions to their warnings, and Lake
improves its linting, caching, and error reporting.
vcgen has also undergone significant development as part of a major
release scheduled for v4.35.0.
To generate a diff of this commit:
cvs rdiff -u -r1.10 -r1.11 pkgsrc/math/lean4/Makefile
cvs rdiff -u -r1.2 -r1.3 pkgsrc/math/lean4/PLIST
cvs rdiff -u -r1.8 -r1.9 pkgsrc/math/lean4/distinfo
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.10 pkgsrc/math/lean4/Makefile:1.11
--- pkgsrc/math/lean4/Makefile:1.10 Fri Aug 28 18:35:12 2026
+++ pkgsrc/math/lean4/Makefile Sat Sep 26 11:04:54 2026
@@ -1,7 +1,6 @@
-# $NetBSD: Makefile,v 1.10 2026/08/28 18:35:12 wiz Exp $
+# $NetBSD: Makefile,v 1.11 2026/09/26 11:04:54 wiz Exp $
-DISTNAME= lean4-4.33.1
-PKGREVISION= 1
+DISTNAME= lean4-4.34.1
CATEGORIES= math
MASTER_SITES= ${MASTER_SITE_GITHUB:=leanprover/}
GITHUB_TAG= v${PKGVERSION_NOREV}
Index: pkgsrc/math/lean4/PLIST
diff -u pkgsrc/math/lean4/PLIST:1.2 pkgsrc/math/lean4/PLIST:1.3
--- pkgsrc/math/lean4/PLIST:1.2 Tue Aug 11 12:55:48 2026
+++ pkgsrc/math/lean4/PLIST Sat Sep 26 11:04:54 2026
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.2 2026/08/11 12:55:48 wiz Exp $
+@comment $NetBSD: PLIST,v 1.3 2026/09/26 11:04:54 wiz Exp $
bin/lake
bin/lean
bin/leanc
@@ -1882,6 +1882,12 @@ lib/lean/Init/Data/Nat/Power2/Basic.ir.s
lib/lean/Init/Data/Nat/Power2/Basic.olean
lib/lean/Init/Data/Nat/Power2/Basic.olean.private
lib/lean/Init/Data/Nat/Power2/Basic.olean.server
+lib/lean/Init/Data/Nat/Power2/Bitwise.ilean
+lib/lean/Init/Data/Nat/Power2/Bitwise.ir
+lib/lean/Init/Data/Nat/Power2/Bitwise.ir.sig
+lib/lean/Init/Data/Nat/Power2/Bitwise.olean
+lib/lean/Init/Data/Nat/Power2/Bitwise.olean.private
+lib/lean/Init/Data/Nat/Power2/Bitwise.olean.server
lib/lean/Init/Data/Nat/Power2/Lemmas.ilean
lib/lean/Init/Data/Nat/Power2/Lemmas.ir
lib/lean/Init/Data/Nat/Power2/Lemmas.ir.sig
@@ -3190,6 +3196,102 @@ lib/lean/Init/Grind/FieldNormNum.ir.sig
lib/lean/Init/Grind/FieldNormNum.olean
lib/lean/Init/Grind/FieldNormNum.olean.private
lib/lean/Init/Grind/FieldNormNum.olean.server
+lib/lean/Init/Grind/Homo.ilean
+lib/lean/Init/Grind/Homo.ir
+lib/lean/Init/Grind/Homo.ir.sig
+lib/lean/Init/Grind/Homo.olean
+lib/lean/Init/Grind/Homo.olean.private
+lib/lean/Init/Grind/Homo.olean.server
+lib/lean/Init/Grind/Homo/BitVec.ilean
+lib/lean/Init/Grind/Homo/BitVec.ir
+lib/lean/Init/Grind/Homo/BitVec.ir.sig
+lib/lean/Init/Grind/Homo/BitVec.olean
+lib/lean/Init/Grind/Homo/BitVec.olean.private
+lib/lean/Init/Grind/Homo/BitVec.olean.server
+lib/lean/Init/Grind/Homo/Fin.ilean
+lib/lean/Init/Grind/Homo/Fin.ir
+lib/lean/Init/Grind/Homo/Fin.ir.sig
+lib/lean/Init/Grind/Homo/Fin.olean
+lib/lean/Init/Grind/Homo/Fin.olean.private
+lib/lean/Init/Grind/Homo/Fin.olean.server
+lib/lean/Init/Grind/Homo/ISize.ilean
+lib/lean/Init/Grind/Homo/ISize.ir
+lib/lean/Init/Grind/Homo/ISize.ir.sig
+lib/lean/Init/Grind/Homo/ISize.olean
+lib/lean/Init/Grind/Homo/ISize.olean.private
+lib/lean/Init/Grind/Homo/ISize.olean.server
+lib/lean/Init/Grind/Homo/Int.ilean
+lib/lean/Init/Grind/Homo/Int.ir
+lib/lean/Init/Grind/Homo/Int.ir.sig
+lib/lean/Init/Grind/Homo/Int.olean
+lib/lean/Init/Grind/Homo/Int.olean.private
+lib/lean/Init/Grind/Homo/Int.olean.server
+lib/lean/Init/Grind/Homo/Int16.ilean
+lib/lean/Init/Grind/Homo/Int16.ir
+lib/lean/Init/Grind/Homo/Int16.ir.sig
+lib/lean/Init/Grind/Homo/Int16.olean
+lib/lean/Init/Grind/Homo/Int16.olean.private
+lib/lean/Init/Grind/Homo/Int16.olean.server
+lib/lean/Init/Grind/Homo/Int32.ilean
+lib/lean/Init/Grind/Homo/Int32.ir
+lib/lean/Init/Grind/Homo/Int32.ir.sig
+lib/lean/Init/Grind/Homo/Int32.olean
+lib/lean/Init/Grind/Homo/Int32.olean.private
+lib/lean/Init/Grind/Homo/Int32.olean.server
+lib/lean/Init/Grind/Homo/Int64.ilean
+lib/lean/Init/Grind/Homo/Int64.ir
+lib/lean/Init/Grind/Homo/Int64.ir.sig
+lib/lean/Init/Grind/Homo/Int64.olean
+lib/lean/Init/Grind/Homo/Int64.olean.private
+lib/lean/Init/Grind/Homo/Int64.olean.server
+lib/lean/Init/Grind/Homo/Int8.ilean
+lib/lean/Init/Grind/Homo/Int8.ir
+lib/lean/Init/Grind/Homo/Int8.ir.sig
+lib/lean/Init/Grind/Homo/Int8.olean
+lib/lean/Init/Grind/Homo/Int8.olean.private
+lib/lean/Init/Grind/Homo/Int8.olean.server
+lib/lean/Init/Grind/Homo/List.ilean
+lib/lean/Init/Grind/Homo/List.ir
+lib/lean/Init/Grind/Homo/List.ir.sig
+lib/lean/Init/Grind/Homo/List.olean
+lib/lean/Init/Grind/Homo/List.olean.private
+lib/lean/Init/Grind/Homo/List.olean.server
+lib/lean/Init/Grind/Homo/Nat.ilean
+lib/lean/Init/Grind/Homo/Nat.ir
+lib/lean/Init/Grind/Homo/Nat.ir.sig
+lib/lean/Init/Grind/Homo/Nat.olean
+lib/lean/Init/Grind/Homo/Nat.olean.private
+lib/lean/Init/Grind/Homo/Nat.olean.server
+lib/lean/Init/Grind/Homo/UInt16.ilean
+lib/lean/Init/Grind/Homo/UInt16.ir
+lib/lean/Init/Grind/Homo/UInt16.ir.sig
+lib/lean/Init/Grind/Homo/UInt16.olean
+lib/lean/Init/Grind/Homo/UInt16.olean.private
+lib/lean/Init/Grind/Homo/UInt16.olean.server
+lib/lean/Init/Grind/Homo/UInt32.ilean
+lib/lean/Init/Grind/Homo/UInt32.ir
+lib/lean/Init/Grind/Homo/UInt32.ir.sig
+lib/lean/Init/Grind/Homo/UInt32.olean
+lib/lean/Init/Grind/Homo/UInt32.olean.private
+lib/lean/Init/Grind/Homo/UInt32.olean.server
+lib/lean/Init/Grind/Homo/UInt64.ilean
+lib/lean/Init/Grind/Homo/UInt64.ir
+lib/lean/Init/Grind/Homo/UInt64.ir.sig
+lib/lean/Init/Grind/Homo/UInt64.olean
+lib/lean/Init/Grind/Homo/UInt64.olean.private
+lib/lean/Init/Grind/Homo/UInt64.olean.server
+lib/lean/Init/Grind/Homo/UInt8.ilean
+lib/lean/Init/Grind/Homo/UInt8.ir
+lib/lean/Init/Grind/Homo/UInt8.ir.sig
+lib/lean/Init/Grind/Homo/UInt8.olean
+lib/lean/Init/Grind/Homo/UInt8.olean.private
+lib/lean/Init/Grind/Homo/UInt8.olean.server
+lib/lean/Init/Grind/Homo/USize.ilean
+lib/lean/Init/Grind/Homo/USize.ir
+lib/lean/Init/Grind/Homo/USize.ir.sig
+lib/lean/Init/Grind/Homo/USize.olean
+lib/lean/Init/Grind/Homo/USize.olean.private
+lib/lean/Init/Grind/Homo/USize.olean.server
lib/lean/Init/Grind/Injective.ilean
lib/lean/Init/Grind/Injective.ir
lib/lean/Init/Grind/Injective.ir.sig
@@ -3520,6 +3622,12 @@ lib/lean/Init/LawfulBEqTactics.ir.sig
lib/lean/Init/LawfulBEqTactics.olean
lib/lean/Init/LawfulBEqTactics.olean.private
lib/lean/Init/LawfulBEqTactics.olean.server
+lib/lean/Init/LetFun.ilean
+lib/lean/Init/LetFun.ir
+lib/lean/Init/LetFun.ir.sig
+lib/lean/Init/LetFun.olean
+lib/lean/Init/LetFun.olean.private
+lib/lean/Init/LetFun.olean.server
lib/lean/Init/MacroTrace.ilean
lib/lean/Init/MacroTrace.ir
lib/lean/Init/MacroTrace.ir.sig
@@ -3802,6 +3910,12 @@ lib/lean/Lake.ir.sig
lib/lean/Lake.olean
lib/lean/Lake.olean.private
lib/lean/Lake.olean.server
+lib/lean/Lake/All.ilean
+lib/lean/Lake/All.ir
+lib/lean/Lake/All.ir.sig
+lib/lean/Lake/All.olean
+lib/lean/Lake/All.olean.private
+lib/lean/Lake/All.olean.server
lib/lean/Lake/Build.ilean
lib/lean/Lake/Build.ir
lib/lean/Lake/Build.ir.sig
@@ -6994,30 +7108,6 @@ lib/lean/Lean/Elab/Tactic/BVDecide.ir.si
lib/lean/Lean/Elab/Tactic/BVDecide.olean
lib/lean/Lean/Elab/Tactic/BVDecide.olean.private
lib/lean/Lean/Elab/Tactic/BVDecide.olean.server
-lib/lean/Lean/Elab/Tactic/BVDecide/BVCheck.ilean
-lib/lean/Lean/Elab/Tactic/BVDecide/BVCheck.ir
-lib/lean/Lean/Elab/Tactic/BVDecide/BVCheck.ir.sig
-lib/lean/Lean/Elab/Tactic/BVDecide/BVCheck.olean
-lib/lean/Lean/Elab/Tactic/BVDecide/BVCheck.olean.private
-lib/lean/Lean/Elab/Tactic/BVDecide/BVCheck.olean.server
-lib/lean/Lean/Elab/Tactic/BVDecide/BVDecide.ilean
-lib/lean/Lean/Elab/Tactic/BVDecide/BVDecide.ir
-lib/lean/Lean/Elab/Tactic/BVDecide/BVDecide.ir.sig
-lib/lean/Lean/Elab/Tactic/BVDecide/BVDecide.olean
-lib/lean/Lean/Elab/Tactic/BVDecide/BVDecide.olean.private
-lib/lean/Lean/Elab/Tactic/BVDecide/BVDecide.olean.server
-lib/lean/Lean/Elab/Tactic/BVDecide/BVTrace.ilean
-lib/lean/Lean/Elab/Tactic/BVDecide/BVTrace.ir
-lib/lean/Lean/Elab/Tactic/BVDecide/BVTrace.ir.sig
-lib/lean/Lean/Elab/Tactic/BVDecide/BVTrace.olean
-lib/lean/Lean/Elab/Tactic/BVDecide/BVTrace.olean.private
-lib/lean/Lean/Elab/Tactic/BVDecide/BVTrace.olean.server
-lib/lean/Lean/Elab/Tactic/BVDecide/Normalize.ilean
-lib/lean/Lean/Elab/Tactic/BVDecide/Normalize.ir
-lib/lean/Lean/Elab/Tactic/BVDecide/Normalize.ir.sig
-lib/lean/Lean/Elab/Tactic/BVDecide/Normalize.olean
-lib/lean/Lean/Elab/Tactic/BVDecide/Normalize.olean.private
-lib/lean/Lean/Elab/Tactic/BVDecide/Normalize.olean.server
lib/lean/Lean/Elab/Tactic/Basic.ilean
lib/lean/Lean/Elab/Tactic/Basic.ir
lib/lean/Lean/Elab/Tactic/Basic.ir.sig
@@ -7174,6 +7264,18 @@ lib/lean/Lean/Elab/Tactic/Do/Attr.ir.sig
lib/lean/Lean/Elab/Tactic/Do/Attr.olean
lib/lean/Lean/Elab/Tactic/Do/Attr.olean.private
lib/lean/Lean/Elab/Tactic/Do/Attr.olean.server
+lib/lean/Lean/Elab/Tactic/Do/ConjunctivePre.ilean
+lib/lean/Lean/Elab/Tactic/Do/ConjunctivePre.ir
+lib/lean/Lean/Elab/Tactic/Do/ConjunctivePre.ir.sig
+lib/lean/Lean/Elab/Tactic/Do/ConjunctivePre.olean
+lib/lean/Lean/Elab/Tactic/Do/ConjunctivePre.olean.private
+lib/lean/Lean/Elab/Tactic/Do/ConjunctivePre.olean.server
+lib/lean/Lean/Elab/Tactic/Do/Contract.ilean
+lib/lean/Lean/Elab/Tactic/Do/Contract.ir
+lib/lean/Lean/Elab/Tactic/Do/Contract.ir.sig
+lib/lean/Lean/Elab/Tactic/Do/Contract.olean
+lib/lean/Lean/Elab/Tactic/Do/Contract.olean.private
+lib/lean/Lean/Elab/Tactic/Do/Contract.olean.server
lib/lean/Lean/Elab/Tactic/Do/Internal.ilean
lib/lean/Lean/Elab/Tactic/Do/Internal.ir
lib/lean/Lean/Elab/Tactic/Do/Internal.ir.sig
@@ -7492,6 +7594,12 @@ lib/lean/Lean/Elab/Tactic/Grind/Annotate
lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean
lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean.private
lib/lean/Lean/Elab/Tactic/Grind/Annotated.olean.server
+lib/lean/Lean/Elab/Tactic/Grind/BVDecide.ilean
+lib/lean/Lean/Elab/Tactic/Grind/BVDecide.ir
+lib/lean/Lean/Elab/Tactic/Grind/BVDecide.ir.sig
+lib/lean/Lean/Elab/Tactic/Grind/BVDecide.olean
+lib/lean/Lean/Elab/Tactic/Grind/BVDecide.olean.private
+lib/lean/Lean/Elab/Tactic/Grind/BVDecide.olean.server
lib/lean/Lean/Elab/Tactic/Grind/Basic.ilean
lib/lean/Lean/Elab/Tactic/Grind/Basic.ir
lib/lean/Lean/Elab/Tactic/Grind/Basic.ir.sig
@@ -8044,6 +8152,24 @@ lib/lean/Lean/Linter/CheckUnivs.ir.sig
lib/lean/Lean/Linter/CheckUnivs.olean
lib/lean/Lean/Linter/CheckUnivs.olean.private
lib/lean/Lean/Linter/CheckUnivs.olean.server
+lib/lean/Lean/Linter/CodeQuality.ilean
+lib/lean/Lean/Linter/CodeQuality.ir
+lib/lean/Lean/Linter/CodeQuality.ir.sig
+lib/lean/Lean/Linter/CodeQuality.olean
+lib/lean/Lean/Linter/CodeQuality.olean.private
+lib/lean/Lean/Linter/CodeQuality.olean.server
+lib/lean/Lean/Linter/CodeQuality/Basic.ilean
+lib/lean/Lean/Linter/CodeQuality/Basic.ir
+lib/lean/Lean/Linter/CodeQuality/Basic.ir.sig
+lib/lean/Lean/Linter/CodeQuality/Basic.olean
+lib/lean/Lean/Linter/CodeQuality/Basic.olean.private
+lib/lean/Lean/Linter/CodeQuality/Basic.olean.server
+lib/lean/Lean/Linter/CodeQuality/Frontend.ilean
+lib/lean/Lean/Linter/CodeQuality/Frontend.ir
+lib/lean/Lean/Linter/CodeQuality/Frontend.ir.sig
+lib/lean/Lean/Linter/CodeQuality/Frontend.olean
+lib/lean/Lean/Linter/CodeQuality/Frontend.olean.private
+lib/lean/Lean/Linter/CodeQuality/Frontend.olean.server
lib/lean/Lean/Linter/Coe.ilean
lib/lean/Lean/Linter/Coe.ir
lib/lean/Lean/Linter/Coe.ir.sig
@@ -8056,6 +8182,12 @@ lib/lean/Lean/Linter/ConstructorAsVariab
lib/lean/Lean/Linter/ConstructorAsVariable.olean
lib/lean/Lean/Linter/ConstructorAsVariable.olean.private
lib/lean/Lean/Linter/ConstructorAsVariable.olean.server
+lib/lean/Lean/Linter/CoreInternal.ilean
+lib/lean/Lean/Linter/CoreInternal.ir
+lib/lean/Lean/Linter/CoreInternal.ir.sig
+lib/lean/Lean/Linter/CoreInternal.olean
+lib/lean/Lean/Linter/CoreInternal.olean.private
+lib/lean/Lean/Linter/CoreInternal.olean.server
lib/lean/Lean/Linter/DefProp.ilean
lib/lean/Lean/Linter/DefProp.ir
lib/lean/Lean/Linter/DefProp.ir.sig
@@ -8134,6 +8266,12 @@ lib/lean/Lean/Linter/Init.ir.sig
lib/lean/Lean/Linter/Init.olean
lib/lean/Lean/Linter/Init.olean.private
lib/lean/Lean/Linter/Init.olean.server
+lib/lean/Lean/Linter/InternalModule.ilean
+lib/lean/Lean/Linter/InternalModule.ir
+lib/lean/Lean/Linter/InternalModule.ir.sig
+lib/lean/Lean/Linter/InternalModule.olean
+lib/lean/Lean/Linter/InternalModule.olean.private
+lib/lean/Lean/Linter/InternalModule.olean.server
lib/lean/Lean/Linter/List.ilean
lib/lean/Lean/Linter/List.ir
lib/lean/Lean/Linter/List.ir.sig
@@ -9424,6 +9562,12 @@ lib/lean/Lean/Meta/Tactic/BVDecide/Norma
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Basic.olean
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Basic.olean.private
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Basic.olean.server
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.ilean
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.ir
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.ir.sig
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.olean
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.olean.private
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.olean.server
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/EmbeddedConstraint.ilean
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/EmbeddedConstraint.ir
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/EmbeddedConstraint.ir.sig
@@ -9442,6 +9586,12 @@ lib/lean/Lean/Meta/Tactic/BVDecide/Norma
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/IntToBitVec.olean
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/IntToBitVec.olean.private
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/IntToBitVec.olean.server
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.ilean
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.ir
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.ir.sig
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.olean
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.olean.private
+lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.olean.server
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Rewrite.ilean
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Rewrite.ir
lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Rewrite.ir.sig
@@ -10414,6 +10564,12 @@ lib/lean/Lean/Meta/Tactic/Grind/ForallPr
lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean
lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean.private
lib/lean/Lean/Meta/Tactic/Grind/ForallProp.olean.server
+lib/lean/Lean/Meta/Tactic/Grind/Homo.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Homo.ir
+lib/lean/Lean/Meta/Tactic/Grind/Homo.ir.sig
+lib/lean/Lean/Meta/Tactic/Grind/Homo.olean
+lib/lean/Lean/Meta/Tactic/Grind/Homo.olean.private
+lib/lean/Lean/Meta/Tactic/Grind/Homo.olean.server
lib/lean/Lean/Meta/Tactic/Grind/Injection.ilean
lib/lean/Lean/Meta/Tactic/Grind/Injection.ir
lib/lean/Lean/Meta/Tactic/Grind/Injection.ir.sig
@@ -11230,6 +11386,24 @@ lib/lean/Lean/PostprocessTraces/Basic.ir
lib/lean/Lean/PostprocessTraces/Basic.olean
lib/lean/Lean/PostprocessTraces/Basic.olean.private
lib/lean/Lean/PostprocessTraces/Basic.olean.server
+lib/lean/Lean/PostprocessTraces/PostprocessTracesCommand.ilean
+lib/lean/Lean/PostprocessTraces/PostprocessTracesCommand.ir
+lib/lean/Lean/PostprocessTraces/PostprocessTracesCommand.ir.sig
+lib/lean/Lean/PostprocessTraces/PostprocessTracesCommand.olean
+lib/lean/Lean/PostprocessTraces/PostprocessTracesCommand.olean.private
+lib/lean/Lean/PostprocessTraces/PostprocessTracesCommand.olean.server
+lib/lean/Lean/PostprocessTraces/Postprocessors.ilean
+lib/lean/Lean/PostprocessTraces/Postprocessors.ir
+lib/lean/Lean/PostprocessTraces/Postprocessors.ir.sig
+lib/lean/Lean/PostprocessTraces/Postprocessors.olean
+lib/lean/Lean/PostprocessTraces/Postprocessors.olean.private
+lib/lean/Lean/PostprocessTraces/Postprocessors.olean.server
+lib/lean/Lean/PostprocessTraces/StoredTraces.ilean
+lib/lean/Lean/PostprocessTraces/StoredTraces.ir
+lib/lean/Lean/PostprocessTraces/StoredTraces.ir.sig
+lib/lean/Lean/PostprocessTraces/StoredTraces.olean
+lib/lean/Lean/PostprocessTraces/StoredTraces.olean.private
+lib/lean/Lean/PostprocessTraces/StoredTraces.olean.server
lib/lean/Lean/PrettyPrinter.ilean
lib/lean/Lean/PrettyPrinter.ir
lib/lean/Lean/PrettyPrinter.ir.sig
@@ -13394,6 +13568,12 @@ lib/lean/Std/Http/Data/Body/Length.ir.si
lib/lean/Std/Http/Data/Body/Length.olean
lib/lean/Std/Http/Data/Body/Length.olean.private
lib/lean/Std/Http/Data/Body/Length.olean.server
+lib/lean/Std/Http/Data/Body/Replayable.ilean
+lib/lean/Std/Http/Data/Body/Replayable.ir
+lib/lean/Std/Http/Data/Body/Replayable.ir.sig
+lib/lean/Std/Http/Data/Body/Replayable.olean
+lib/lean/Std/Http/Data/Body/Replayable.olean.private
+lib/lean/Std/Http/Data/Body/Replayable.olean.server
lib/lean/Std/Http/Data/Body/Stream.ilean
lib/lean/Std/Http/Data/Body/Stream.ir
lib/lean/Std/Http/Data/Body/Stream.ir.sig
@@ -13580,6 +13760,12 @@ lib/lean/Std/Http/Protocol/H1/Reader.ir.
lib/lean/Std/Http/Protocol/H1/Reader.olean
lib/lean/Std/Http/Protocol/H1/Reader.olean.private
lib/lean/Std/Http/Protocol/H1/Reader.olean.server
+lib/lean/Std/Http/Protocol/H1/Redirect.ilean
+lib/lean/Std/Http/Protocol/H1/Redirect.ir
+lib/lean/Std/Http/Protocol/H1/Redirect.ir.sig
+lib/lean/Std/Http/Protocol/H1/Redirect.olean
+lib/lean/Std/Http/Protocol/H1/Redirect.olean.private
+lib/lean/Std/Http/Protocol/H1/Redirect.olean.server
lib/lean/Std/Http/Protocol/H1/Writer.ilean
lib/lean/Std/Http/Protocol/H1/Writer.ir
lib/lean/Std/Http/Protocol/H1/Writer.ir.sig
@@ -13646,6 +13832,12 @@ lib/lean/Std/Internal/Do/ExceptPost.ir.s
lib/lean/Std/Internal/Do/ExceptPost.olean
lib/lean/Std/Internal/Do/ExceptPost.olean.private
lib/lean/Std/Internal/Do/ExceptPost.olean.server
+lib/lean/Std/Internal/Do/Gadget/ForIn.ilean
+lib/lean/Std/Internal/Do/Gadget/ForIn.ir
+lib/lean/Std/Internal/Do/Gadget/ForIn.ir.sig
+lib/lean/Std/Internal/Do/Gadget/ForIn.olean
+lib/lean/Std/Internal/Do/Gadget/ForIn.olean.private
+lib/lean/Std/Internal/Do/Gadget/ForIn.olean.server
lib/lean/Std/Internal/Do/Order/Basic.ilean
lib/lean/Std/Internal/Do/Order/Basic.ir
lib/lean/Std/Internal/Do/Order/Basic.ir.sig
@@ -13736,6 +13928,24 @@ lib/lean/Std/Internal/Do/WP/Lemmas.ir.si
lib/lean/Std/Internal/Do/WP/Lemmas.olean
lib/lean/Std/Internal/Do/WP/Lemmas.olean.private
lib/lean/Std/Internal/Do/WP/Lemmas.olean.server
+lib/lean/Std/Internal/ForIn.ilean
+lib/lean/Std/Internal/ForIn.ir
+lib/lean/Std/Internal/ForIn.ir.sig
+lib/lean/Std/Internal/ForIn.olean
+lib/lean/Std/Internal/ForIn.olean.private
+lib/lean/Std/Internal/ForIn.olean.server
+lib/lean/Std/Internal/ForIn/Basic.ilean
+lib/lean/Std/Internal/ForIn/Basic.ir
+lib/lean/Std/Internal/ForIn/Basic.ir.sig
+lib/lean/Std/Internal/ForIn/Basic.olean
+lib/lean/Std/Internal/ForIn/Basic.olean.private
+lib/lean/Std/Internal/ForIn/Basic.olean.server
+lib/lean/Std/Internal/ForIn/Lemmas.ilean
+lib/lean/Std/Internal/ForIn/Lemmas.ir
+lib/lean/Std/Internal/ForIn/Lemmas.ir.sig
+lib/lean/Std/Internal/ForIn/Lemmas.olean
+lib/lean/Std/Internal/ForIn/Lemmas.olean.private
+lib/lean/Std/Internal/ForIn/Lemmas.olean.server
lib/lean/Std/Internal/Parsec.ilean
lib/lean/Std/Internal/Parsec.ir
lib/lean/Std/Internal/Parsec.ir.sig
@@ -15242,6 +15452,7 @@ src/lean/Init/Data/Nat/Mod.lean
src/lean/Init/Data/Nat/Order.lean
src/lean/Init/Data/Nat/Power2.lean
src/lean/Init/Data/Nat/Power2/Basic.lean
+src/lean/Init/Data/Nat/Power2/Bitwise.lean
src/lean/Init/Data/Nat/Power2/Lemmas.lean
src/lean/Init/Data/Nat/Simproc.lean
src/lean/Init/Data/Nat/Sqrt.lean
@@ -15460,6 +15671,22 @@ src/lean/Init/Grind/Cases.lean
src/lean/Init/Grind/Config.lean
src/lean/Init/Grind/Ext.lean
src/lean/Init/Grind/FieldNormNum.lean
+src/lean/Init/Grind/Homo.lean
+src/lean/Init/Grind/Homo/BitVec.lean
+src/lean/Init/Grind/Homo/Fin.lean
+src/lean/Init/Grind/Homo/ISize.lean
+src/lean/Init/Grind/Homo/Int.lean
+src/lean/Init/Grind/Homo/Int16.lean
+src/lean/Init/Grind/Homo/Int32.lean
+src/lean/Init/Grind/Homo/Int64.lean
+src/lean/Init/Grind/Homo/Int8.lean
+src/lean/Init/Grind/Homo/List.lean
+src/lean/Init/Grind/Homo/Nat.lean
+src/lean/Init/Grind/Homo/UInt16.lean
+src/lean/Init/Grind/Homo/UInt32.lean
+src/lean/Init/Grind/Homo/UInt64.lean
+src/lean/Init/Grind/Homo/UInt8.lean
+src/lean/Init/Grind/Homo/USize.lean
src/lean/Init/Grind/Injective.lean
src/lean/Init/Grind/Interactive.lean
src/lean/Init/Grind/Lemmas.lean
@@ -15515,6 +15742,7 @@ src/lean/Init/Internal/Order/MonadTail.l
src/lean/Init/Internal/Order/Tactic.lean
src/lean/Init/Internal/Order/While.lean
src/lean/Init/LawfulBEqTactics.lean
+src/lean/Init/LetFun.lean
src/lean/Init/MacroTrace.lean
src/lean/Init/Meta.lean
src/lean/Init/Meta/Defs.lean
@@ -15934,10 +16162,6 @@ src/lean/Lean/Elab/Tactic.lean
src/lean/Lean/Elab/Tactic/AsAuxLemma.lean
src/lean/Lean/Elab/Tactic/AutoTry.lean
src/lean/Lean/Elab/Tactic/BVDecide.lean
-src/lean/Lean/Elab/Tactic/BVDecide/BVCheck.lean
-src/lean/Lean/Elab/Tactic/BVDecide/BVDecide.lean
-src/lean/Lean/Elab/Tactic/BVDecide/BVTrace.lean
-src/lean/Lean/Elab/Tactic/BVDecide/Normalize.lean
src/lean/Lean/Elab/Tactic/Basic.lean
src/lean/Lean/Elab/Tactic/BoolToPropSimps.lean
src/lean/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -15964,6 +16188,8 @@ src/lean/Lean/Elab/Tactic/Delta.lean
src/lean/Lean/Elab/Tactic/DiscrTreeKey.lean
src/lean/Lean/Elab/Tactic/Do.lean
src/lean/Lean/Elab/Tactic/Do/Attr.lean
+src/lean/Lean/Elab/Tactic/Do/ConjunctivePre.lean
+src/lean/Lean/Elab/Tactic/Do/Contract.lean
src/lean/Lean/Elab/Tactic/Do/Internal.lean
src/lean/Lean/Elab/Tactic/Do/Internal/VCGen.lean
src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
@@ -16017,6 +16243,7 @@ src/lean/Lean/Elab/Tactic/Generalize.lea
src/lean/Lean/Elab/Tactic/Grind.lean
src/lean/Lean/Elab/Tactic/Grind/Anchor.lean
src/lean/Lean/Elab/Tactic/Grind/Annotated.lean
+src/lean/Lean/Elab/Tactic/Grind/BVDecide.lean
src/lean/Lean/Elab/Tactic/Grind/Basic.lean
src/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
src/lean/Lean/Elab/Tactic/Grind/Cbv.lean
@@ -16109,8 +16336,12 @@ src/lean/Lean/Linter/AmbiguousOpen.lean
src/lean/Lean/Linter/Basic.lean
src/lean/Lean/Linter/Builtin.lean
src/lean/Lean/Linter/CheckUnivs.lean
+src/lean/Lean/Linter/CodeQuality.lean
+src/lean/Lean/Linter/CodeQuality/Basic.lean
+src/lean/Lean/Linter/CodeQuality/Frontend.lean
src/lean/Lean/Linter/Coe.lean
src/lean/Lean/Linter/ConstructorAsVariable.lean
+src/lean/Lean/Linter/CoreInternal.lean
src/lean/Lean/Linter/DefProp.lean
src/lean/Lean/Linter/Deprecated.lean
src/lean/Lean/Linter/DocsOnAlt.lean
@@ -16124,6 +16355,7 @@ src/lean/Lean/Linter/Extra/UnreachableTa
src/lean/Lean/Linter/Extra/UnusedDecidableInType.lean
src/lean/Lean/Linter/GlobalAttributeIn.lean
src/lean/Lean/Linter/Init.lean
+src/lean/Lean/Linter/InternalModule.lean
src/lean/Lean/Linter/List.lean
src/lean/Lean/Linter/MissingDocs.lean
src/lean/Lean/Linter/Omit.lean
@@ -16339,9 +16571,11 @@ src/lean/Lean/Meta/Tactic/BVDecide/Norma
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/AndFlatten.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/ApplyControlFlow.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Basic.lean
+src/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/EmbeddedConstraint.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Enums.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/IntToBitVec.lean
+src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Rewrite.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/ShortCircuit.lean
src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Simproc.lean
@@ -16504,6 +16738,7 @@ src/lean/Lean/Meta/Tactic/Grind/Extensio
src/lean/Lean/Meta/Tactic/Grind/Filter.lean
src/lean/Lean/Meta/Tactic/Grind/Finish.lean
src/lean/Lean/Meta/Tactic/Grind/ForallProp.lean
+src/lean/Lean/Meta/Tactic/Grind/Homo.lean
src/lean/Lean/Meta/Tactic/Grind/Injection.lean
src/lean/Lean/Meta/Tactic/Grind/Injective.lean
src/lean/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -16640,6 +16875,9 @@ src/lean/Lean/ParserCompiler.lean
src/lean/Lean/ParserCompiler/Attribute.lean
src/lean/Lean/PostprocessTraces.lean
src/lean/Lean/PostprocessTraces/Basic.lean
+src/lean/Lean/PostprocessTraces/PostprocessTracesCommand.lean
+src/lean/Lean/PostprocessTraces/Postprocessors.lean
+src/lean/Lean/PostprocessTraces/StoredTraces.lean
src/lean/Lean/PrettyPrinter.lean
src/lean/Lean/PrettyPrinter/Basic.lean
src/lean/Lean/PrettyPrinter/Delaborator.lean
@@ -17003,6 +17241,7 @@ src/lean/Std/Http/Data/Body/Basic.lean
src/lean/Std/Http/Data/Body/Empty.lean
src/lean/Std/Http/Data/Body/Full.lean
src/lean/Std/Http/Data/Body/Length.lean
+src/lean/Std/Http/Data/Body/Replayable.lean
src/lean/Std/Http/Data/Body/Stream.lean
src/lean/Std/Http/Data/Chunk.lean
src/lean/Std/Http/Data/Extensions.lean
@@ -17034,6 +17273,7 @@ src/lean/Std/Http/Protocol/H1/Event.lean
src/lean/Std/Http/Protocol/H1/Message.lean
src/lean/Std/Http/Protocol/H1/Parser.lean
src/lean/Std/Http/Protocol/H1/Reader.lean
+src/lean/Std/Http/Protocol/H1/Redirect.lean
src/lean/Std/Http/Protocol/H1/Writer.lean
src/lean/Std/Http/Server.lean
src/lean/Std/Http/Server/Config.lean
@@ -17045,6 +17285,7 @@ src/lean/Std/Internal.lean
src/lean/Std/Internal/Do.lean
src/lean/Std/Internal/Do/Assertion.lean
src/lean/Std/Internal/Do/ExceptPost.lean
+src/lean/Std/Internal/Do/Gadget/ForIn.lean
src/lean/Std/Internal/Do/Order/Basic.lean
src/lean/Std/Internal/Do/Order/Heyting.lean
src/lean/Std/Internal/Do/Order/Instances.lean
@@ -17060,6 +17301,9 @@ src/lean/Std/Internal/Do/WP/Basic.lean
src/lean/Std/Internal/Do/WP/Conjunctive.lean
src/lean/Std/Internal/Do/WP/Frame.lean
src/lean/Std/Internal/Do/WP/Lemmas.lean
+src/lean/Std/Internal/ForIn.lean
+src/lean/Std/Internal/ForIn/Basic.lean
+src/lean/Std/Internal/ForIn/Lemmas.lean
src/lean/Std/Internal/Parsec.lean
src/lean/Std/Internal/Parsec/Basic.lean
src/lean/Std/Internal/Parsec/ByteArray.lean
@@ -17258,6 +17502,7 @@ src/lean/Std/Time/Zoned/TimeZone.lean
src/lean/Std/Time/Zoned/ZoneRules.lean
src/lean/cmake/Modules/README.md
src/lean/lake/Lake.lean
+src/lean/lake/Lake/All.lean
src/lean/lake/Lake/Build.lean
src/lean/lake/Lake/Build/Actions.lean
src/lean/lake/Lake/Build/Common.lean
Index: pkgsrc/math/lean4/distinfo
diff -u pkgsrc/math/lean4/distinfo:1.8 pkgsrc/math/lean4/distinfo:1.9
--- pkgsrc/math/lean4/distinfo:1.8 Fri Aug 28 18:35:12 2026
+++ pkgsrc/math/lean4/distinfo Sat Sep 26 11:04:54 2026
@@ -1,8 +1,8 @@
-$NetBSD: distinfo,v 1.8 2026/08/28 18:35:12 wiz Exp $
+$NetBSD: distinfo,v 1.9 2026/09/26 11:04:54 wiz Exp $
-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
+BLAKE2s (lean4-4.34.1.tar.gz) = 1590c61336410c0d4be667d4c0170a9af6f05a007df1b91aa6d7ddc721d700e8
+SHA512 (lean4-4.34.1.tar.gz) = d8024237a6741fd2391e7127d2de80178b4e1dc811220c51c04890b5575e4075a10de82ca950d352aa605043596673d45ed9c851f2735ea29b5992cf4612477f
+Size (lean4-4.34.1.tar.gz) = 87768894 bytes
SHA1 (patch-src_CMakeLists.txt) = c6620d0ca4c6f5d2fccf4e8e97462661c1a9d38d
SHA1 (patch-src_Leanc.lean) = 156025c502ceb1afc67288c107cdca99b6968cc6
SHA1 (patch-src_include_lean_lean.h) = 017a9c5b5ac185a122a831f6fe4a64e94d9caad9
Home |
Main Index |
Thread Index |
Old Index