git: 1fde20b526dd - main - math/lean4: update 4.10.0 → 4.11.0

Go to: [ bottom of page ] [ top of archives ] [ this month ]
From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Mon, 02 Sep 2024 07:54:57 UTC
The branch main has been updated by yuri:

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

commit 1fde20b526ddc12811e0af7ee6a71e1f732eaf5b
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2024-09-02 07:54:32 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2024-09-02 07:54:45 +0000

    math/lean4: update 4.10.0 → 4.11.0
---
 math/lean4/Makefile  |   2 +-
 math/lean4/distinfo  |   6 +-
 math/lean4/pkg-plist | 220 ++++++++++++++++++++++++++++++++++++++++++++++++---
 3 files changed, 215 insertions(+), 13 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 562dad632944..abfc3004d07b 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.10.0
+DISTVERSION=	4.11.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
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index 1ca0f069d7a4..fd56f3893df9 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1722411891
-SHA256 (leanprover-lean4-v4.10.0_GH0.tar.gz) = dee5d1dbcea924fa3f4500c1f4854ea5953f471e3600dac71421c742c844b094
-SIZE (leanprover-lean4-v4.10.0_GH0.tar.gz) = 25013155
+TIMESTAMP = 1725254182
+SHA256 (leanprover-lean4-v4.11.0_GH0.tar.gz) = 8b7fc8e71e107250c7bbf911eb1f450379d874857a26236577aaa624dd5962b5
+SIZE (leanprover-lean4-v4.11.0_GH0.tar.gz) = 25790812
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 65859221ae90..365f371356e4 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -54,6 +54,8 @@ lib/lean/Init/Data/AC.ilean
 lib/lean/Init/Data/AC.olean
 lib/lean/Init/Data/Array.ilean
 lib/lean/Init/Data/Array.olean
+lib/lean/Init/Data/Array/Attach.ilean
+lib/lean/Init/Data/Array/Attach.olean
 lib/lean/Init/Data/Array/Basic.ilean
 lib/lean/Init/Data/Array/Basic.olean
 lib/lean/Init/Data/Array/BasicAux.ilean
@@ -74,6 +76,10 @@ lib/lean/Init/Data/Array/Subarray.ilean
 lib/lean/Init/Data/Array/Subarray.olean
 lib/lean/Init/Data/Array/Subarray/Split.ilean
 lib/lean/Init/Data/Array/Subarray/Split.olean
+lib/lean/Init/Data/Array/TakeDrop.ilean
+lib/lean/Init/Data/Array/TakeDrop.olean
+lib/lean/Init/Data/BEq.ilean
+lib/lean/Init/Data/BEq.olean
 lib/lean/Init/Data/Basic.ilean
 lib/lean/Init/Data/Basic.olean
 lib/lean/Init/Data/BitVec.ilean
@@ -106,6 +112,8 @@ lib/lean/Init/Data/Fin.ilean
 lib/lean/Init/Data/Fin.olean
 lib/lean/Init/Data/Fin/Basic.ilean
 lib/lean/Init/Data/Fin/Basic.olean
+lib/lean/Init/Data/Fin/Bitwise.ilean
+lib/lean/Init/Data/Fin/Bitwise.olean
 lib/lean/Init/Data/Fin/Fold.ilean
 lib/lean/Init/Data/Fin/Fold.olean
 lib/lean/Init/Data/Fin/Iterate.ilean
@@ -154,20 +162,48 @@ lib/lean/Init/Data/Int/Pow.ilean
 lib/lean/Init/Data/Int/Pow.olean
 lib/lean/Init/Data/List.ilean
 lib/lean/Init/Data/List.olean
+lib/lean/Init/Data/List/Attach.ilean
+lib/lean/Init/Data/List/Attach.olean
 lib/lean/Init/Data/List/Basic.ilean
 lib/lean/Init/Data/List/Basic.olean
 lib/lean/Init/Data/List/BasicAux.ilean
 lib/lean/Init/Data/List/BasicAux.olean
 lib/lean/Init/Data/List/Control.ilean
 lib/lean/Init/Data/List/Control.olean
+lib/lean/Init/Data/List/Count.ilean
+lib/lean/Init/Data/List/Count.olean
+lib/lean/Init/Data/List/Erase.ilean
+lib/lean/Init/Data/List/Erase.olean
+lib/lean/Init/Data/List/Find.ilean
+lib/lean/Init/Data/List/Find.olean
 lib/lean/Init/Data/List/Impl.ilean
 lib/lean/Init/Data/List/Impl.olean
 lib/lean/Init/Data/List/Lemmas.ilean
 lib/lean/Init/Data/List/Lemmas.olean
+lib/lean/Init/Data/List/MinMax.ilean
+lib/lean/Init/Data/List/MinMax.olean
+lib/lean/Init/Data/List/Monadic.ilean
+lib/lean/Init/Data/List/Monadic.olean
+lib/lean/Init/Data/List/Nat.ilean
+lib/lean/Init/Data/List/Nat.olean
+lib/lean/Init/Data/List/Nat/Basic.ilean
+lib/lean/Init/Data/List/Nat/Basic.olean
+lib/lean/Init/Data/List/Nat/Pairwise.ilean
+lib/lean/Init/Data/List/Nat/Pairwise.olean
+lib/lean/Init/Data/List/Nat/Range.ilean
+lib/lean/Init/Data/List/Nat/Range.olean
+lib/lean/Init/Data/List/Nat/TakeDrop.ilean
+lib/lean/Init/Data/List/Nat/TakeDrop.olean
 lib/lean/Init/Data/List/Notation.ilean
 lib/lean/Init/Data/List/Notation.olean
+lib/lean/Init/Data/List/Pairwise.ilean
+lib/lean/Init/Data/List/Pairwise.olean
+lib/lean/Init/Data/List/Sublist.ilean
+lib/lean/Init/Data/List/Sublist.olean
 lib/lean/Init/Data/List/TakeDrop.ilean
 lib/lean/Init/Data/List/TakeDrop.olean
+lib/lean/Init/Data/List/Zip.ilean
+lib/lean/Init/Data/List/Zip.olean
 lib/lean/Init/Data/Nat.ilean
 lib/lean/Init/Data/Nat.olean
 lib/lean/Init/Data/Nat/Basic.ilean
@@ -240,6 +276,8 @@ lib/lean/Init/Data/String/Extra.ilean
 lib/lean/Init/Data/String/Extra.olean
 lib/lean/Init/Data/String/Lemmas.ilean
 lib/lean/Init/Data/String/Lemmas.olean
+lib/lean/Init/Data/Subtype.ilean
+lib/lean/Init/Data/Subtype.olean
 lib/lean/Init/Data/Sum.ilean
 lib/lean/Init/Data/Sum.olean
 lib/lean/Init/Data/ToString.ilean
@@ -252,6 +290,8 @@ lib/lean/Init/Data/UInt.ilean
 lib/lean/Init/Data/UInt.olean
 lib/lean/Init/Data/UInt/Basic.ilean
 lib/lean/Init/Data/UInt/Basic.olean
+lib/lean/Init/Data/UInt/Bitwise.ilean
+lib/lean/Init/Data/UInt/Bitwise.olean
 lib/lean/Init/Data/UInt/Lemmas.ilean
 lib/lean/Init/Data/UInt/Lemmas.olean
 lib/lean/Init/Data/UInt/Log2.ilean
@@ -1092,14 +1132,22 @@ lib/lean/Lean/Elab/PreDefinition/Structural/Eqns.ilean
 lib/lean/Lean/Elab/PreDefinition/Structural/Eqns.olean
 lib/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.ilean
 lib/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.olean
+lib/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.ilean
+lib/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.olean
 lib/lean/Lean/Elab/PreDefinition/Structural/IndPred.ilean
 lib/lean/Lean/Elab/PreDefinition/Structural/IndPred.olean
 lib/lean/Lean/Elab/PreDefinition/Structural/Main.ilean
 lib/lean/Lean/Elab/PreDefinition/Structural/Main.olean
 lib/lean/Lean/Elab/PreDefinition/Structural/Preprocess.ilean
 lib/lean/Lean/Elab/PreDefinition/Structural/Preprocess.olean
+lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.ilean
+lib/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.olean
 lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.ilean
 lib/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.olean
+lib/lean/Lean/Elab/PreDefinition/TerminationArgument.ilean
+lib/lean/Lean/Elab/PreDefinition/TerminationArgument.olean
+lib/lean/Lean/Elab/PreDefinition/TerminationHint.ilean
+lib/lean/Lean/Elab/PreDefinition/TerminationHint.olean
 lib/lean/Lean/Elab/PreDefinition/WF.ilean
 lib/lean/Lean/Elab/PreDefinition/WF.olean
 lib/lean/Lean/Elab/PreDefinition/WF/Eqns.ilean
@@ -1118,10 +1166,6 @@ lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.ilean
 lib/lean/Lean/Elab/PreDefinition/WF/Preprocess.olean
 lib/lean/Lean/Elab/PreDefinition/WF/Rel.ilean
 lib/lean/Lean/Elab/PreDefinition/WF/Rel.olean
-lib/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.ilean
-lib/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.olean
-lib/lean/Lean/Elab/PreDefinition/WF/TerminationHint.ilean
-lib/lean/Lean/Elab/PreDefinition/WF/TerminationHint.olean
 lib/lean/Lean/Elab/Print.ilean
 lib/lean/Lean/Elab/Print.olean
 lib/lean/Lean/Elab/Quotation.ilean
@@ -1178,6 +1222,8 @@ lib/lean/Lean/Elab/Tactic/Conv/Unfold.ilean
 lib/lean/Lean/Elab/Tactic/Conv/Unfold.olean
 lib/lean/Lean/Elab/Tactic/Delta.ilean
 lib/lean/Lean/Elab/Tactic/Delta.olean
+lib/lean/Lean/Elab/Tactic/DiscrTreeKey.ilean
+lib/lean/Lean/Elab/Tactic/DiscrTreeKey.olean
 lib/lean/Lean/Elab/Tactic/Doc.ilean
 lib/lean/Lean/Elab/Tactic/Doc.olean
 lib/lean/Lean/Elab/Tactic/ElabTerm.ilean
@@ -1270,6 +1316,8 @@ lib/lean/Lean/Language/Basic.ilean
 lib/lean/Lean/Language/Basic.olean
 lib/lean/Lean/Language/Lean.ilean
 lib/lean/Lean/Language/Lean.olean
+lib/lean/Lean/Language/Lean/Types.ilean
+lib/lean/Lean/Language/Lean/Types.olean
 lib/lean/Lean/LazyInitExtension.ilean
 lib/lean/Lean/LazyInitExtension.olean
 lib/lean/Lean/Level.ilean
@@ -1286,6 +1334,8 @@ lib/lean/Lean/Linter/Deprecated.ilean
 lib/lean/Lean/Linter/Deprecated.olean
 lib/lean/Lean/Linter/MissingDocs.ilean
 lib/lean/Lean/Linter/MissingDocs.olean
+lib/lean/Lean/Linter/Omit.ilean
+lib/lean/Lean/Linter/Omit.olean
 lib/lean/Lean/Linter/UnusedVariables.ilean
 lib/lean/Lean/Linter/UnusedVariables.olean
 lib/lean/Lean/Linter/Util.ilean
@@ -1338,6 +1388,10 @@ lib/lean/Lean/Meta/Constructions.ilean
 lib/lean/Lean/Meta/Constructions.olean
 lib/lean/Lean/Meta/Constructions/BRecOn.ilean
 lib/lean/Lean/Meta/Constructions/BRecOn.olean
+lib/lean/Lean/Meta/Constructions/CasesOn.ilean
+lib/lean/Lean/Meta/Constructions/CasesOn.olean
+lib/lean/Lean/Meta/Constructions/NoConfusion.ilean
+lib/lean/Lean/Meta/Constructions/NoConfusion.olean
 lib/lean/Lean/Meta/Constructions/RecOn.ilean
 lib/lean/Lean/Meta/Constructions/RecOn.olean
 lib/lean/Lean/Meta/CtorRecognizer.ilean
@@ -1430,6 +1484,8 @@ lib/lean/Lean/Meta/Offset.ilean
 lib/lean/Lean/Meta/Offset.olean
 lib/lean/Lean/Meta/PPGoal.ilean
 lib/lean/Lean/Meta/PPGoal.olean
+lib/lean/Lean/Meta/PProdN.ilean
+lib/lean/Lean/Meta/PProdN.olean
 lib/lean/Lean/Meta/RecursorInfo.ilean
 lib/lean/Lean/Meta/RecursorInfo.olean
 lib/lean/Lean/Meta/Reduce.ilean
@@ -1552,6 +1608,8 @@ lib/lean/Lean/Meta/Tactic/Simp/Attr.ilean
 lib/lean/Lean/Meta/Tactic/Simp/Attr.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.olean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.ilean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.ilean
@@ -1562,6 +1620,8 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.olean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.ilean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.ilean
@@ -1754,6 +1814,8 @@ lib/lean/Lean/ToExpr.ilean
 lib/lean/Lean/ToExpr.olean
 lib/lean/Lean/Util.ilean
 lib/lean/Lean/Util.olean
+lib/lean/Lean/Util/CollectAxioms.ilean
+lib/lean/Lean/Util/CollectAxioms.olean
 lib/lean/Lean/Util/CollectFVars.ilean
 lib/lean/Lean/Util/CollectFVars.olean
 lib/lean/Lean/Util/CollectLevelParams.ilean
@@ -1790,6 +1852,8 @@ lib/lean/Lean/Util/MonadBacktrack.ilean
 lib/lean/Lean/Util/MonadBacktrack.olean
 lib/lean/Lean/Util/MonadCache.ilean
 lib/lean/Lean/Util/MonadCache.olean
+lib/lean/Lean/Util/NumObjs.ilean
+lib/lean/Lean/Util/NumObjs.olean
 lib/lean/Lean/Util/OccursCheck.ilean
 lib/lean/Lean/Util/OccursCheck.olean
 lib/lean/Lean/Util/PPExt.ilean
@@ -1814,6 +1878,10 @@ lib/lean/Lean/Util/ReplaceLevel.ilean
 lib/lean/Lean/Util/ReplaceLevel.olean
 lib/lean/Lean/Util/SCC.ilean
 lib/lean/Lean/Util/SCC.olean
+lib/lean/Lean/Util/SafeExponentiation.ilean
+lib/lean/Lean/Util/SafeExponentiation.olean
+lib/lean/Lean/Util/SearchPath.ilean
+lib/lean/Lean/Util/SearchPath.olean
 lib/lean/Lean/Util/ShareCommon.ilean
 lib/lean/Lean/Util/ShareCommon.olean
 lib/lean/Lean/Util/Sorry.ilean
@@ -1842,6 +1910,72 @@ lib/lean/Lean/Widget/UserWidget.ilean
 lib/lean/Lean/Widget/UserWidget.olean
 lib/lean/Std.ilean
 lib/lean/Std.olean
+lib/lean/Std/Data.ilean
+lib/lean/Std/Data.olean
+lib/lean/Std/Data/DHashMap.ilean
+lib/lean/Std/Data/DHashMap.olean
+lib/lean/Std/Data/DHashMap/AdditionalOperations.ilean
+lib/lean/Std/Data/DHashMap/AdditionalOperations.olean
+lib/lean/Std/Data/DHashMap/Basic.ilean
+lib/lean/Std/Data/DHashMap/Basic.olean
+lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.ilean
+lib/lean/Std/Data/DHashMap/Internal/AssocList/Basic.olean
+lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.ilean
+lib/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.olean
+lib/lean/Std/Data/DHashMap/Internal/Defs.ilean
+lib/lean/Std/Data/DHashMap/Internal/Defs.olean
+lib/lean/Std/Data/DHashMap/Internal/Index.ilean
+lib/lean/Std/Data/DHashMap/Internal/Index.olean
+lib/lean/Std/Data/DHashMap/Internal/List/Associative.ilean
+lib/lean/Std/Data/DHashMap/Internal/List/Associative.olean
+lib/lean/Std/Data/DHashMap/Internal/List/Defs.ilean
+lib/lean/Std/Data/DHashMap/Internal/List/Defs.olean
+lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.ilean
+lib/lean/Std/Data/DHashMap/Internal/List/HashesTo.olean
+lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.ilean
+lib/lean/Std/Data/DHashMap/Internal/List/Pairwise.olean
+lib/lean/Std/Data/DHashMap/Internal/List/Perm.ilean
+lib/lean/Std/Data/DHashMap/Internal/List/Perm.olean
+lib/lean/Std/Data/DHashMap/Internal/List/Sublist.ilean
+lib/lean/Std/Data/DHashMap/Internal/List/Sublist.olean
+lib/lean/Std/Data/DHashMap/Internal/Model.ilean
+lib/lean/Std/Data/DHashMap/Internal/Model.olean
+lib/lean/Std/Data/DHashMap/Internal/Raw.ilean
+lib/lean/Std/Data/DHashMap/Internal/Raw.olean
+lib/lean/Std/Data/DHashMap/Internal/RawLemmas.ilean
+lib/lean/Std/Data/DHashMap/Internal/RawLemmas.olean
+lib/lean/Std/Data/DHashMap/Internal/WF.ilean
+lib/lean/Std/Data/DHashMap/Internal/WF.olean
+lib/lean/Std/Data/DHashMap/Lemmas.ilean
+lib/lean/Std/Data/DHashMap/Lemmas.olean
+lib/lean/Std/Data/DHashMap/Raw.ilean
+lib/lean/Std/Data/DHashMap/Raw.olean
+lib/lean/Std/Data/DHashMap/RawDef.ilean
+lib/lean/Std/Data/DHashMap/RawDef.olean
+lib/lean/Std/Data/DHashMap/RawLemmas.ilean
+lib/lean/Std/Data/DHashMap/RawLemmas.olean
+lib/lean/Std/Data/HashMap.ilean
+lib/lean/Std/Data/HashMap.olean
+lib/lean/Std/Data/HashMap/AdditionalOperations.ilean
+lib/lean/Std/Data/HashMap/AdditionalOperations.olean
+lib/lean/Std/Data/HashMap/Basic.ilean
+lib/lean/Std/Data/HashMap/Basic.olean
+lib/lean/Std/Data/HashMap/Lemmas.ilean
+lib/lean/Std/Data/HashMap/Lemmas.olean
+lib/lean/Std/Data/HashMap/Raw.ilean
+lib/lean/Std/Data/HashMap/Raw.olean
+lib/lean/Std/Data/HashMap/RawLemmas.ilean
+lib/lean/Std/Data/HashMap/RawLemmas.olean
+lib/lean/Std/Data/HashSet.ilean
+lib/lean/Std/Data/HashSet.olean
+lib/lean/Std/Data/HashSet/Basic.ilean
+lib/lean/Std/Data/HashSet/Basic.olean
+lib/lean/Std/Data/HashSet/Lemmas.ilean
+lib/lean/Std/Data/HashSet/Lemmas.olean
+lib/lean/Std/Data/HashSet/Raw.ilean
+lib/lean/Std/Data/HashSet/Raw.olean
+lib/lean/Std/Data/HashSet/RawLemmas.ilean
+lib/lean/Std/Data/HashSet/RawLemmas.olean
 lib/lean/libInit.a
 lib/lean/libInit_shared.so
 lib/lean/libLake.a
@@ -1875,6 +2009,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data.lean
 %%DATADIR%%/src/lean/Init/Data/AC.lean
 %%DATADIR%%/src/lean/Init/Data/Array.lean
+%%DATADIR%%/src/lean/Init/Data/Array/Attach.lean
 %%DATADIR%%/src/lean/Init/Data/Array/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/Array/BasicAux.lean
 %%DATADIR%%/src/lean/Init/Data/Array/BinSearch.lean
@@ -1885,6 +2020,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Array/QSort.lean
 %%DATADIR%%/src/lean/Init/Data/Array/Subarray.lean
 %%DATADIR%%/src/lean/Init/Data/Array/Subarray/Split.lean
+%%DATADIR%%/src/lean/Init/Data/Array/TakeDrop.lean
+%%DATADIR%%/src/lean/Init/Data/BEq.lean
 %%DATADIR%%/src/lean/Init/Data/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/BitVec.lean
 %%DATADIR%%/src/lean/Init/Data/BitVec/Basic.lean
@@ -1901,6 +2038,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Char/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Fin.lean
 %%DATADIR%%/src/lean/Init/Data/Fin/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/Fin/Bitwise.lean
 %%DATADIR%%/src/lean/Init/Data/Fin/Fold.lean
 %%DATADIR%%/src/lean/Init/Data/Fin/Iterate.lean
 %%DATADIR%%/src/lean/Init/Data/Fin/Lemmas.lean
@@ -1925,13 +2063,27 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Int/Order.lean
 %%DATADIR%%/src/lean/Init/Data/Int/Pow.lean
 %%DATADIR%%/src/lean/Init/Data/List.lean
+%%DATADIR%%/src/lean/Init/Data/List/Attach.lean
 %%DATADIR%%/src/lean/Init/Data/List/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/List/BasicAux.lean
 %%DATADIR%%/src/lean/Init/Data/List/Control.lean
+%%DATADIR%%/src/lean/Init/Data/List/Count.lean
+%%DATADIR%%/src/lean/Init/Data/List/Erase.lean
+%%DATADIR%%/src/lean/Init/Data/List/Find.lean
 %%DATADIR%%/src/lean/Init/Data/List/Impl.lean
 %%DATADIR%%/src/lean/Init/Data/List/Lemmas.lean
+%%DATADIR%%/src/lean/Init/Data/List/MinMax.lean
+%%DATADIR%%/src/lean/Init/Data/List/Monadic.lean
+%%DATADIR%%/src/lean/Init/Data/List/Nat.lean
+%%DATADIR%%/src/lean/Init/Data/List/Nat/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/List/Nat/Pairwise.lean
+%%DATADIR%%/src/lean/Init/Data/List/Nat/Range.lean
+%%DATADIR%%/src/lean/Init/Data/List/Nat/TakeDrop.lean
 %%DATADIR%%/src/lean/Init/Data/List/Notation.lean
+%%DATADIR%%/src/lean/Init/Data/List/Pairwise.lean
+%%DATADIR%%/src/lean/Init/Data/List/Sublist.lean
 %%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean
+%%DATADIR%%/src/lean/Init/Data/List/Zip.lean
 %%DATADIR%%/src/lean/Init/Data/Nat.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise.lean
@@ -1968,12 +2120,14 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/String/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/String/Extra.lean
 %%DATADIR%%/src/lean/Init/Data/String/Lemmas.lean
+%%DATADIR%%/src/lean/Init/Data/Subtype.lean
 %%DATADIR%%/src/lean/Init/Data/Sum.lean
 %%DATADIR%%/src/lean/Init/Data/ToString.lean
 %%DATADIR%%/src/lean/Init/Data/ToString/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/ToString/Macro.lean
 %%DATADIR%%/src/lean/Init/Data/UInt.lean
 %%DATADIR%%/src/lean/Init/Data/UInt/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/UInt/Bitwise.lean
 %%DATADIR%%/src/lean/Init/Data/UInt/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean
 %%DATADIR%%/src/lean/Init/Dynamic.lean
@@ -2266,10 +2420,14 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Basic.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Eqns.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/FindRecArg.lean
+%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/IndGroupInfo.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/IndPred.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Main.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/Preprocess.lean
+%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean
+%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationArgument.lean
+%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/TerminationHint.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Eqns.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Fix.lean
@@ -2279,8 +2437,6 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/PackMutual.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Preprocess.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Rel.lean
-%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/TerminationArgument.lean
-%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/TerminationHint.lean
 %%DATADIR%%/src/lean/Lean/Elab/Print.lean
 %%DATADIR%%/src/lean/Lean/Elab/Quotation.lean
 %%DATADIR%%/src/lean/Lean/Elab/Quotation/Precheck.lean
@@ -2309,6 +2465,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Simp.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Unfold.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Delta.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/DiscrTreeKey.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Doc.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/ElabTerm.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Ext.lean
@@ -2355,6 +2512,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/LabelAttribute.lean
 %%DATADIR%%/src/lean/Lean/Language/Basic.lean
 %%DATADIR%%/src/lean/Lean/Language/Lean.lean
+%%DATADIR%%/src/lean/Lean/Language/Lean/Types.lean
 %%DATADIR%%/src/lean/Lean/LazyInitExtension.lean
 %%DATADIR%%/src/lean/Lean/Level.lean
 %%DATADIR%%/src/lean/Lean/Linter.lean
@@ -2363,6 +2521,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Linter/ConstructorAsVariable.lean
 %%DATADIR%%/src/lean/Lean/Linter/Deprecated.lean
 %%DATADIR%%/src/lean/Lean/Linter/MissingDocs.lean
+%%DATADIR%%/src/lean/Lean/Linter/Omit.lean
 %%DATADIR%%/src/lean/Lean/Linter/UnusedVariables.lean
 %%DATADIR%%/src/lean/Lean/Linter/Util.lean
 %%DATADIR%%/src/lean/Lean/LoadDynlib.lean
@@ -2389,6 +2548,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/CongrTheorems.lean
 %%DATADIR%%/src/lean/Lean/Meta/Constructions.lean
 %%DATADIR%%/src/lean/Lean/Meta/Constructions/BRecOn.lean
+%%DATADIR%%/src/lean/Lean/Meta/Constructions/CasesOn.lean
+%%DATADIR%%/src/lean/Lean/Meta/Constructions/NoConfusion.lean
 %%DATADIR%%/src/lean/Lean/Meta/Constructions/RecOn.lean
 %%DATADIR%%/src/lean/Lean/Meta/CtorRecognizer.lean
 %%DATADIR%%/src/lean/Lean/Meta/DecLevel.lean
@@ -2435,6 +2596,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/NatInstTesters.lean
 %%DATADIR%%/src/lean/Lean/Meta/Offset.lean
 %%DATADIR%%/src/lean/Lean/Meta/PPGoal.lean
+%%DATADIR%%/src/lean/Lean/Meta/PProdN.lean
 %%DATADIR%%/src/lean/Lean/Meta/RecursorInfo.lean
 %%DATADIR%%/src/lean/Lean/Meta/Reduce.lean
 %%DATADIR%%/src/lean/Lean/Meta/ReduceEval.lean
@@ -2496,11 +2658,13 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Attr.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Array.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/List.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
@@ -2598,6 +2762,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Syntax.lean
 %%DATADIR%%/src/lean/Lean/ToExpr.lean
 %%DATADIR%%/src/lean/Lean/Util.lean
+%%DATADIR%%/src/lean/Lean/Util/CollectAxioms.lean
 %%DATADIR%%/src/lean/Lean/Util/CollectFVars.lean
 %%DATADIR%%/src/lean/Lean/Util/CollectLevelParams.lean
 %%DATADIR%%/src/lean/Lean/Util/CollectMVars.lean
@@ -2616,6 +2781,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Util/LeanOptions.lean
 %%DATADIR%%/src/lean/Lean/Util/MonadBacktrack.lean
 %%DATADIR%%/src/lean/Lean/Util/MonadCache.lean
+%%DATADIR%%/src/lean/Lean/Util/NumObjs.lean
 %%DATADIR%%/src/lean/Lean/Util/OccursCheck.lean
 %%DATADIR%%/src/lean/Lean/Util/PPExt.lean
 %%DATADIR%%/src/lean/Lean/Util/Path.lean
@@ -2628,6 +2794,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Util/ReplaceExpr.lean
 %%DATADIR%%/src/lean/Lean/Util/ReplaceLevel.lean
 %%DATADIR%%/src/lean/Lean/Util/SCC.lean
+%%DATADIR%%/src/lean/Lean/Util/SafeExponentiation.lean
+%%DATADIR%%/src/lean/Lean/Util/SearchPath.lean
 %%DATADIR%%/src/lean/Lean/Util/ShareCommon.lean
 %%DATADIR%%/src/lean/Lean/Util/Sorry.lean
 %%DATADIR%%/src/lean/Lean/Util/TestExtern.lean
@@ -2643,6 +2811,39 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Widget/UserWidget.lean
 %%DATADIR%%/src/lean/Leanc.lean
 %%DATADIR%%/src/lean/Std.lean
+%%DATADIR%%/src/lean/Std/Data.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/AdditionalOperations.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Basic.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Basic.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Defs.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Index.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Defs.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/HashesTo.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Pairwise.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Perm.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/List/Sublist.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Model.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/Raw.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Internal/WF.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/Raw.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/RawDef.lean
+%%DATADIR%%/src/lean/Std/Data/DHashMap/RawLemmas.lean
+%%DATADIR%%/src/lean/Std/Data/HashMap.lean
+%%DATADIR%%/src/lean/Std/Data/HashMap/AdditionalOperations.lean
+%%DATADIR%%/src/lean/Std/Data/HashMap/Basic.lean
+%%DATADIR%%/src/lean/Std/Data/HashMap/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Data/HashMap/Raw.lean
+%%DATADIR%%/src/lean/Std/Data/HashMap/RawLemmas.lean
+%%DATADIR%%/src/lean/Std/Data/HashSet.lean
+%%DATADIR%%/src/lean/Std/Data/HashSet/Basic.lean
+%%DATADIR%%/src/lean/Std/Data/HashSet/Lemmas.lean
+%%DATADIR%%/src/lean/Std/Data/HashSet/Raw.lean
+%%DATADIR%%/src/lean/Std/Data/HashSet/RawLemmas.lean
 %%DATADIR%%/src/lean/lake/Lake.lean
 %%DATADIR%%/src/lean/lake/Lake/Build.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean
@@ -2818,6 +3019,10 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/lock/Nop.lean
 %%DATADIR%%/src/lean/lake/tests/lock/Wait.lean
 %%DATADIR%%/src/lean/lake/tests/lock/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Error.lean
+%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Info.lean
+%%DATADIR%%/src/lean/lake/tests/logLevel/Log/Warning.lean
+%%DATADIR%%/src/lean/lake/tests/logLevel/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/manifest/bar/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/manifest/foo/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/manifest/lakefile.lean
@@ -2857,6 +3062,3 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/trace/Foo.lean
 %%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean
 %%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean
-%%DATADIR%%/src/lean/lake/tests/wfail/Warn.lean
-%%DATADIR%%/src/lean/lake/tests/wfail/lakefile.lean
-@dir lib/lean/Std