git: e55bf905b6d7 - main - math/lean4: update 4.33.1 → 4.34.0

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Mon, 14 Sep 2026 18:52:14 UTC
The branch main has been updated by yuri:

URL: https://cgit.FreeBSD.org/ports/commit/?id=e55bf905b6d7fb695216aae7e8bb049e710f1187

commit e55bf905b6d7fb695216aae7e8bb049e710f1187
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2026-09-14 17:11:35 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2026-09-14 18:52:04 +0000

    math/lean4: update 4.33.1 → 4.34.0
---
 math/lean4/Makefile  |   3 +-
 math/lean4/distinfo  |   6 +-
 math/lean4/pkg-plist | 301 ++++++++++++++++++++++++++++++++++++++++++++++-----
 3 files changed, 278 insertions(+), 32 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index e557cdd21938..5bd52e6d3a0a 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.33.1
+DISTVERSION=	4.34.0
 CATEGORIES=	math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
 
 MAINTAINER=	yuri@FreeBSD.org
@@ -102,5 +102,6 @@ post-install:
 		lib/lean/libLake_shared.so
 
 # tests as of 4.33.1: 100% tests passed, 0 tests failed out of 3988
+# tests as of 4.34.0: 100% tests pass (individual testsuite runs have intermittent failures with different tests, but all individual tests pass when run separately)
 
 .include <bsd.port.mk>
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index a0cba28f01b4..992460368c5a 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1788581049
-SHA256 (leanprover-lean4-v4.33.1_GH0.tar.gz) = 561b500da16419aec0baeba5dc47ad11979b5bdcd30a02aafc88c3eed599b766
-SIZE (leanprover-lean4-v4.33.1_GH0.tar.gz) = 86700313
+TIMESTAMP = 1789399297
+SHA256 (leanprover-lean4-v4.34.0_GH0.tar.gz) = c6a2f9c57cebbe390beef82fafcb3a66274301cb9f9a70ceba0b125661533981
+SIZE (leanprover-lean4-v4.34.0_GH0.tar.gz) = 87761947
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 595da85c500f..f32737d8d109 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -1881,6 +1881,12 @@ lib/lean/Init/Data/Nat/Power2/Basic.ir.sig
 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
@@ -3189,6 +3195,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
@@ -3519,6 +3621,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
@@ -3801,6 +3909,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
@@ -6993,30 +7107,6 @@ lib/lean/Lean/Elab/Tactic/BVDecide.ir.sig
 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
@@ -7173,6 +7263,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
@@ -7491,6 +7593,12 @@ lib/lean/Lean/Elab/Tactic/Grind/Annotated.ir.sig
 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
@@ -8043,6 +8151,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
@@ -8055,6 +8181,12 @@ lib/lean/Lean/Linter/ConstructorAsVariable.ir.sig
 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
@@ -8133,6 +8265,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
@@ -9423,6 +9561,12 @@ lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/Basic.ir.sig
 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
@@ -9441,6 +9585,12 @@ lib/lean/Lean/Meta/Tactic/BVDecide/Normalize/IntToBitVec.ir.sig
 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
@@ -10413,6 +10563,12 @@ lib/lean/Lean/Meta/Tactic/Grind/ForallProp.ir.sig
 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
@@ -11229,6 +11385,24 @@ lib/lean/Lean/PostprocessTraces/Basic.ir.sig
 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
@@ -13393,6 +13567,12 @@ lib/lean/Std/Http/Data/Body/Length.ir.sig
 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
@@ -13579,6 +13759,12 @@ lib/lean/Std/Http/Protocol/H1/Reader.ir.sig
 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
@@ -13645,6 +13831,12 @@ lib/lean/Std/Internal/Do/ExceptPost.ir.sig
 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
@@ -13735,6 +13927,24 @@ lib/lean/Std/Internal/Do/WP/Lemmas.ir.sig
 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
@@ -15239,6 +15449,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Nat/Order.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Power2.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Power2/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/Nat/Power2/Bitwise.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Power2/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Simproc.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Sqrt.lean
@@ -15457,6 +15668,22 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Grind/Config.lean
 %%DATADIR%%/src/lean/Init/Grind/Ext.lean
 %%DATADIR%%/src/lean/Init/Grind/FieldNormNum.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/BitVec.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/Fin.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/ISize.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/Int.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/Int16.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/Int32.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/Int64.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/Int8.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/List.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/Nat.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/UInt16.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/UInt32.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/UInt64.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/UInt8.lean
+%%DATADIR%%/src/lean/Init/Grind/Homo/USize.lean
 %%DATADIR%%/src/lean/Init/Grind/Injective.lean
 %%DATADIR%%/src/lean/Init/Grind/Interactive.lean
 %%DATADIR%%/src/lean/Init/Grind/Lemmas.lean
@@ -15512,6 +15739,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Internal/Order/Tactic.lean
 %%DATADIR%%/src/lean/Init/Internal/Order/While.lean
 %%DATADIR%%/src/lean/Init/LawfulBEqTactics.lean
+%%DATADIR%%/src/lean/Init/LetFun.lean
 %%DATADIR%%/src/lean/Init/MacroTrace.lean
 %%DATADIR%%/src/lean/Init/Meta.lean
 %%DATADIR%%/src/lean/Init/Meta/Defs.lean
@@ -15931,10 +16159,6 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/AsAuxLemma.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/AutoTry.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide.lean
-%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/BVCheck.lean
-%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/BVDecide.lean
-%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/BVTrace.lean
-%%DATADIR%%/src/lean/Lean/Elab/Tactic/BVDecide/Normalize.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Basic.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/BoolToPropSimps.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -15961,6 +16185,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/DiscrTreeKey.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/Attr.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/ConjunctivePre.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/Contract.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/Internal.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/Internal/VCGen.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Do/Internal/VCGen/Context.lean
@@ -16014,6 +16240,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Anchor.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Annotated.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/BVDecide.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Basic.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/BuiltinTactic.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Grind/Cbv.lean
@@ -16106,8 +16333,12 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Linter/Basic.lean
 %%DATADIR%%/src/lean/Lean/Linter/Builtin.lean
 %%DATADIR%%/src/lean/Lean/Linter/CheckUnivs.lean
+%%DATADIR%%/src/lean/Lean/Linter/CodeQuality.lean
+%%DATADIR%%/src/lean/Lean/Linter/CodeQuality/Basic.lean
+%%DATADIR%%/src/lean/Lean/Linter/CodeQuality/Frontend.lean
 %%DATADIR%%/src/lean/Lean/Linter/Coe.lean
 %%DATADIR%%/src/lean/Lean/Linter/ConstructorAsVariable.lean
+%%DATADIR%%/src/lean/Lean/Linter/CoreInternal.lean
 %%DATADIR%%/src/lean/Lean/Linter/DefProp.lean
 %%DATADIR%%/src/lean/Lean/Linter/Deprecated.lean
 %%DATADIR%%/src/lean/Lean/Linter/DocsOnAlt.lean
@@ -16121,6 +16352,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Linter/Extra/UnusedDecidableInType.lean
 %%DATADIR%%/src/lean/Lean/Linter/GlobalAttributeIn.lean
 %%DATADIR%%/src/lean/Lean/Linter/Init.lean
+%%DATADIR%%/src/lean/Lean/Linter/InternalModule.lean
 %%DATADIR%%/src/lean/Lean/Linter/List.lean
 %%DATADIR%%/src/lean/Lean/Linter/MissingDocs.lean
 %%DATADIR%%/src/lean/Lean/Linter/Omit.lean
@@ -16336,9 +16568,11 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/AndFlatten.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/ApplyControlFlow.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Basic.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/CollectHyps.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/EmbeddedConstraint.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Enums.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/IntToBitVec.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Reduction.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Rewrite.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/ShortCircuit.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/BVDecide/Normalize/Simproc.lean
@@ -16501,6 +16735,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Filter.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Finish.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/ForallProp.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Homo.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Injection.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Injective.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Internalize.lean
@@ -16637,6 +16872,9 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/ParserCompiler/Attribute.lean
 %%DATADIR%%/src/lean/Lean/PostprocessTraces.lean
 %%DATADIR%%/src/lean/Lean/PostprocessTraces/Basic.lean
+%%DATADIR%%/src/lean/Lean/PostprocessTraces/PostprocessTracesCommand.lean
+%%DATADIR%%/src/lean/Lean/PostprocessTraces/Postprocessors.lean
+%%DATADIR%%/src/lean/Lean/PostprocessTraces/StoredTraces.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Basic.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator.lean
@@ -17000,6 +17238,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Std/Http/Data/Body/Empty.lean
 %%DATADIR%%/src/lean/Std/Http/Data/Body/Full.lean
 %%DATADIR%%/src/lean/Std/Http/Data/Body/Length.lean
+%%DATADIR%%/src/lean/Std/Http/Data/Body/Replayable.lean
 %%DATADIR%%/src/lean/Std/Http/Data/Body/Stream.lean
 %%DATADIR%%/src/lean/Std/Http/Data/Chunk.lean
 %%DATADIR%%/src/lean/Std/Http/Data/Extensions.lean
@@ -17031,6 +17270,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Std/Http/Protocol/H1/Message.lean
 %%DATADIR%%/src/lean/Std/Http/Protocol/H1/Parser.lean
 %%DATADIR%%/src/lean/Std/Http/Protocol/H1/Reader.lean
+%%DATADIR%%/src/lean/Std/Http/Protocol/H1/Redirect.lean
 %%DATADIR%%/src/lean/Std/Http/Protocol/H1/Writer.lean
 %%DATADIR%%/src/lean/Std/Http/Server.lean
 %%DATADIR%%/src/lean/Std/Http/Server/Config.lean
@@ -17042,6 +17282,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Std/Internal/Do.lean
 %%DATADIR%%/src/lean/Std/Internal/Do/Assertion.lean
 %%DATADIR%%/src/lean/Std/Internal/Do/ExceptPost.lean
+%%DATADIR%%/src/lean/Std/Internal/Do/Gadget/ForIn.lean
 %%DATADIR%%/src/lean/Std/Internal/Do/Order/Basic.lean
 %%DATADIR%%/src/lean/Std/Internal/Do/Order/Heyting.lean
 %%DATADIR%%/src/lean/Std/Internal/Do/Order/Instances.lean
@@ -17057,6 +17298,9 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Std/Internal/Do/WP/Conjunctive.lean
 %%DATADIR%%/src/lean/Std/Internal/Do/WP/Frame.lean
 %%DATADIR%%/src/lean/Std/Internal/Do/WP/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Internal/ForIn.lean
+%%DATADIR%%/src/lean/Std/Internal/ForIn/Basic.lean
+%%DATADIR%%/src/lean/Std/Internal/ForIn/Lemmas.lean
 %%DATADIR%%/src/lean/Std/Internal/Parsec.lean
 %%DATADIR%%/src/lean/Std/Internal/Parsec/Basic.lean
 %%DATADIR%%/src/lean/Std/Internal/Parsec/ByteArray.lean
@@ -17255,6 +17499,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Std/Time/Zoned/ZoneRules.lean
 %%DATADIR%%/src/lean/cmake/Modules/README.md
 %%DATADIR%%/src/lean/lake/Lake.lean
+%%DATADIR%%/src/lean/lake/Lake/All.lean
 %%DATADIR%%/src/lean/lake/Lake/Build.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Common.lean