git: 4c7811ea785f - main - math/lean4: update 4.7.0 → 4.8.0

From: Yuri Victorovich <yuri_at_FreeBSD.org>
Date: Fri, 07 Jun 2024 17:01:27 UTC
The branch main has been updated by yuri:

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

commit 4c7811ea785fa4c53d83e3991a6f786e09251d0f
Author:     Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2024-06-07 17:01:16 +0000
Commit:     Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2024-06-07 17:01:24 +0000

    math/lean4: update 4.7.0 → 4.8.0
    
    Reported by:    portscout
---
 math/lean4/Makefile  |   6 +-
 math/lean4/distinfo  |   6 +-
 math/lean4/pkg-plist | 214 +++++++++++++++++++++++++++++++++++++++++++++++----
 3 files changed, 206 insertions(+), 20 deletions(-)

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index cbc4e5280841..c6a1086693fe 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.7.0
+DISTVERSION=	4.8.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
@@ -39,6 +39,8 @@ post-install:
 		lib/lean/libInit_shared.so \
 		lib/lean/libleanshared.so
 
-# 6 tests are known to fail due to bugs in the testcase code, see https://github.com/leanprover/lean4/issues/3179
+# 2 test failures:
+# https://github.com/leanprover/lean4/issues/4396: The test leanlaketest_old times out
+# https://github.com/leanprover/lean4/issues/4397: The test leanlaketest_serve fails: error: unexpected identifier; expected command
 
 .include <bsd.port.mk>
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index d20cb0cc673a..d12208f173cc 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1713025323
-SHA256 (leanprover-lean4-v4.7.0_GH0.tar.gz) = b1f00b5f2431b34aeacba993c4f4675211a3827e96c4b1a06054c58188ae72c8
-SIZE (leanprover-lean4-v4.7.0_GH0.tar.gz) = 19261610
+TIMESTAMP = 1717688258
+SHA256 (leanprover-lean4-v4.8.0_GH0.tar.gz) = 3bb46c24b4f5ad1fee38163bf466d8f60a334bb64a19c9801a42f76162580f9c
+SIZE (leanprover-lean4-v4.8.0_GH0.tar.gz) = 20345135
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 5b2bc5e8899c..75fc4ce6be58 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -30,6 +30,10 @@ lib/lean/Init/Control/Id.ilean
 lib/lean/Init/Control/Id.olean
 lib/lean/Init/Control/Lawful.ilean
 lib/lean/Init/Control/Lawful.olean
+lib/lean/Init/Control/Lawful/Basic.ilean
+lib/lean/Init/Control/Lawful/Basic.olean
+lib/lean/Init/Control/Lawful/Instances.ilean
+lib/lean/Init/Control/Lawful/Instances.olean
 lib/lean/Init/Control/Option.ilean
 lib/lean/Init/Control/Option.olean
 lib/lean/Init/Control/Reader.ilean
@@ -68,6 +72,8 @@ lib/lean/Init/Data/Array/QSort.ilean
 lib/lean/Init/Data/Array/QSort.olean
 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/Basic.ilean
 lib/lean/Init/Data/Basic.olean
 lib/lean/Init/Data/BitVec.ilean
@@ -140,6 +146,8 @@ lib/lean/Init/Data/Int/Lemmas.ilean
 lib/lean/Init/Data/Int/Lemmas.olean
 lib/lean/Init/Data/Int/Order.ilean
 lib/lean/Init/Data/Int/Order.olean
+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/Basic.ilean
@@ -148,6 +156,8 @@ 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/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/Nat.ilean
@@ -160,6 +170,8 @@ lib/lean/Init/Data/Nat/Bitwise/Basic.ilean
 lib/lean/Init/Data/Nat/Bitwise/Basic.olean
 lib/lean/Init/Data/Nat/Bitwise/Lemmas.ilean
 lib/lean/Init/Data/Nat/Bitwise/Lemmas.olean
+lib/lean/Init/Data/Nat/Compare.ilean
+lib/lean/Init/Data/Nat/Compare.olean
 lib/lean/Init/Data/Nat/Control.ilean
 lib/lean/Init/Data/Nat/Control.olean
 lib/lean/Init/Data/Nat/Div.ilean
@@ -168,6 +180,8 @@ lib/lean/Init/Data/Nat/Dvd.ilean
 lib/lean/Init/Data/Nat/Dvd.olean
 lib/lean/Init/Data/Nat/Gcd.ilean
 lib/lean/Init/Data/Nat/Gcd.olean
+lib/lean/Init/Data/Nat/Lcm.ilean
+lib/lean/Init/Data/Nat/Lcm.olean
 lib/lean/Init/Data/Nat/Lemmas.ilean
 lib/lean/Init/Data/Nat/Lemmas.olean
 lib/lean/Init/Data/Nat/Linear.ilean
@@ -182,6 +196,8 @@ lib/lean/Init/Data/Nat/Power2.ilean
 lib/lean/Init/Data/Nat/Power2.olean
 lib/lean/Init/Data/Nat/SOM.ilean
 lib/lean/Init/Data/Nat/SOM.olean
+lib/lean/Init/Data/Nat/Simproc.ilean
+lib/lean/Init/Data/Nat/Simproc.olean
 lib/lean/Init/Data/OfScientific.ilean
 lib/lean/Init/Data/OfScientific.olean
 lib/lean/Init/Data/Option.ilean
@@ -232,10 +248,14 @@ lib/lean/Init/Dynamic.ilean
 lib/lean/Init/Dynamic.olean
 lib/lean/Init/Ext.ilean
 lib/lean/Init/Ext.olean
+lib/lean/Init/GetElem.ilean
+lib/lean/Init/GetElem.olean
 lib/lean/Init/Guard.ilean
 lib/lean/Init/Guard.olean
 lib/lean/Init/Hints.ilean
 lib/lean/Init/Hints.olean
+lib/lean/Init/MacroTrace.ilean
+lib/lean/Init/MacroTrace.olean
 lib/lean/Init/Meta.ilean
 lib/lean/Init/Meta.olean
 lib/lean/Init/MetaTypes.ilean
@@ -308,16 +328,18 @@ lib/lean/Lake/Build.ilean
 lib/lean/Lake/Build.olean
 lib/lean/Lake/Build/Actions.ilean
 lib/lean/Lake/Build/Actions.olean
+lib/lean/Lake/Build/Basic.ilean
+lib/lean/Lake/Build/Basic.olean
 lib/lean/Lake/Build/Common.ilean
 lib/lean/Lake/Build/Common.olean
-lib/lean/Lake/Build/Context.ilean
-lib/lean/Lake/Build/Context.olean
 lib/lean/Lake/Build/Data.ilean
 lib/lean/Lake/Build/Data.olean
 lib/lean/Lake/Build/Executable.ilean
 lib/lean/Lake/Build/Executable.olean
 lib/lean/Lake/Build/Facets.ilean
 lib/lean/Lake/Build/Facets.olean
+lib/lean/Lake/Build/Fetch.ilean
+lib/lean/Lake/Build/Fetch.olean
 lib/lean/Lake/Build/Imports.ilean
 lib/lean/Lake/Build/Imports.olean
 lib/lean/Lake/Build/Index.ilean
@@ -332,10 +354,10 @@ lib/lean/Lake/Build/Library.ilean
 lib/lean/Lake/Build/Library.olean
 lib/lean/Lake/Build/Module.ilean
 lib/lean/Lake/Build/Module.olean
-lib/lean/Lake/Build/Monad.ilean
-lib/lean/Lake/Build/Monad.olean
 lib/lean/Lake/Build/Package.ilean
 lib/lean/Lake/Build/Package.olean
+lib/lean/Lake/Build/Run.ilean
+lib/lean/Lake/Build/Run.olean
 lib/lean/Lake/Build/Store.ilean
 lib/lean/Lake/Build/Store.olean
 lib/lean/Lake/Build/Targets.ilean
@@ -360,6 +382,12 @@ lib/lean/Lake/CLI/Main.ilean
 lib/lean/Lake/CLI/Main.olean
 lib/lean/Lake/CLI/Serve.ilean
 lib/lean/Lake/CLI/Serve.olean
+lib/lean/Lake/CLI/Translate.ilean
+lib/lean/Lake/CLI/Translate.olean
+lib/lean/Lake/CLI/Translate/Lean.ilean
+lib/lean/Lake/CLI/Translate/Lean.olean
+lib/lean/Lake/CLI/Translate/Toml.ilean
+lib/lean/Lake/CLI/Translate/Toml.olean
 lib/lean/Lake/Config.ilean
 lib/lean/Lake/Config.olean
 lib/lean/Lake/Config/Context.ilean
@@ -380,6 +408,8 @@ lib/lean/Lake/Config/Glob.ilean
 lib/lean/Lake/Config/Glob.olean
 lib/lean/Lake/Config/InstallPath.ilean
 lib/lean/Lake/Config/InstallPath.olean
+lib/lean/Lake/Config/Lang.ilean
+lib/lean/Lake/Config/Lang.olean
 lib/lean/Lake/Config/LeanConfig.ilean
 lib/lean/Lake/Config/LeanConfig.olean
 lib/lean/Lake/Config/LeanExe.ilean
@@ -440,10 +470,36 @@ lib/lean/Lake/Load/Materialize.ilean
 lib/lean/Lake/Load/Materialize.olean
 lib/lean/Lake/Load/Package.ilean
 lib/lean/Lake/Load/Package.olean
+lib/lean/Lake/Load/Toml.ilean
+lib/lean/Lake/Load/Toml.olean
 lib/lean/Lake/Main.ilean
 lib/lean/Lake/Main.olean
-lib/lean/Lake/Util/Async.ilean
-lib/lean/Lake/Util/Async.olean
+lib/lean/Lake/Toml.ilean
+lib/lean/Lake/Toml.olean
+lib/lean/Lake/Toml/Data.ilean
+lib/lean/Lake/Toml/Data.olean
+lib/lean/Lake/Toml/Data/DateTime.ilean
+lib/lean/Lake/Toml/Data/DateTime.olean
+lib/lean/Lake/Toml/Data/Dict.ilean
+lib/lean/Lake/Toml/Data/Dict.olean
+lib/lean/Lake/Toml/Data/Value.ilean
+lib/lean/Lake/Toml/Data/Value.olean
+lib/lean/Lake/Toml/Decode.ilean
+lib/lean/Lake/Toml/Decode.olean
+lib/lean/Lake/Toml/Elab.ilean
+lib/lean/Lake/Toml/Elab.olean
+lib/lean/Lake/Toml/Elab/Expression.ilean
+lib/lean/Lake/Toml/Elab/Expression.olean
+lib/lean/Lake/Toml/Elab/Value.ilean
+lib/lean/Lake/Toml/Elab/Value.olean
+lib/lean/Lake/Toml/Encode.ilean
+lib/lean/Lake/Toml/Encode.olean
+lib/lean/Lake/Toml/Grammar.ilean
+lib/lean/Lake/Toml/Grammar.olean
+lib/lean/Lake/Toml/Load.ilean
+lib/lean/Lake/Toml/Load.olean
+lib/lean/Lake/Toml/ParserUtil.ilean
+lib/lean/Lake/Toml/ParserUtil.olean
 lib/lean/Lake/Util/Binder.ilean
 lib/lean/Lake/Util/Binder.olean
 lib/lean/Lake/Util/Casing.ilean
@@ -466,24 +522,32 @@ lib/lean/Lake/Util/Exit.ilean
 lib/lean/Lake/Util/Exit.olean
 lib/lean/Lake/Util/Family.ilean
 lib/lean/Lake/Util/Family.olean
+lib/lean/Lake/Util/FilePath.ilean
+lib/lean/Lake/Util/FilePath.olean
 lib/lean/Lake/Util/Git.ilean
 lib/lean/Lake/Util/Git.olean
+lib/lean/Lake/Util/IO.ilean
+lib/lean/Lake/Util/IO.olean
 lib/lean/Lake/Util/Lift.ilean
 lib/lean/Lake/Util/Lift.olean
 lib/lean/Lake/Util/List.ilean
 lib/lean/Lake/Util/List.olean
+lib/lean/Lake/Util/Lock.ilean
+lib/lean/Lake/Util/Lock.olean
 lib/lean/Lake/Util/Log.ilean
 lib/lean/Lake/Util/Log.olean
 lib/lean/Lake/Util/MainM.ilean
 lib/lean/Lake/Util/MainM.olean
+lib/lean/Lake/Util/Message.ilean
+lib/lean/Lake/Util/Message.olean
 lib/lean/Lake/Util/Name.ilean
 lib/lean/Lake/Util/Name.olean
 lib/lean/Lake/Util/NativeLib.ilean
 lib/lean/Lake/Util/NativeLib.olean
+lib/lean/Lake/Util/Newline.ilean
+lib/lean/Lake/Util/Newline.olean
 lib/lean/Lake/Util/Opaque.ilean
 lib/lean/Lake/Util/Opaque.olean
-lib/lean/Lake/Util/OptionIO.ilean
-lib/lean/Lake/Util/OptionIO.olean
 lib/lean/Lake/Util/OrdHashSet.ilean
 lib/lean/Lake/Util/OrdHashSet.olean
 lib/lean/Lake/Util/OrderedTagAttribute.ilean
@@ -508,6 +572,8 @@ lib/lean/Lean/Attributes.ilean
 lib/lean/Lean/Attributes.olean
 lib/lean/Lean/AuxRecursor.ilean
 lib/lean/Lean/AuxRecursor.olean
+lib/lean/Lean/BuiltinDocAttr.ilean
+lib/lean/Lean/BuiltinDocAttr.olean
 lib/lean/Lean/Class.ilean
 lib/lean/Lean/Class.olean
 lib/lean/Lean/Compiler.ilean
@@ -790,6 +856,8 @@ lib/lean/Lean/Data/Lsp/TextSync.ilean
 lib/lean/Lean/Data/Lsp/TextSync.olean
 lib/lean/Lean/Data/Lsp/Utf16.ilean
 lib/lean/Lean/Data/Lsp/Utf16.olean
+lib/lean/Lean/Data/Lsp/Window.ilean
+lib/lean/Lean/Data/Lsp/Window.olean
 lib/lean/Lean/Data/Lsp/Workspace.ilean
 lib/lean/Lean/Data/Lsp/Workspace.olean
 lib/lean/Lean/Data/Name.ilean
@@ -874,6 +942,8 @@ lib/lean/Lean/Elab/Config.ilean
 lib/lean/Lean/Elab/Config.olean
 lib/lean/Lean/Elab/DeclModifiers.ilean
 lib/lean/Lean/Elab/DeclModifiers.olean
+lib/lean/Lean/Elab/DeclNameGen.ilean
+lib/lean/Lean/Elab/DeclNameGen.olean
 lib/lean/Lean/Elab/DeclUtil.ilean
 lib/lean/Lean/Elab/DeclUtil.olean
 lib/lean/Lean/Elab/Declaration.ilean
@@ -1004,14 +1074,14 @@ lib/lean/Lean/Elab/PreDefinition/WF/Ite.ilean
 lib/lean/Lean/Elab/PreDefinition/WF/Ite.olean
 lib/lean/Lean/Elab/PreDefinition/WF/Main.ilean
 lib/lean/Lean/Elab/PreDefinition/WF/Main.olean
-lib/lean/Lean/Elab/PreDefinition/WF/PackDomain.ilean
-lib/lean/Lean/Elab/PreDefinition/WF/PackDomain.olean
 lib/lean/Lean/Elab/PreDefinition/WF/PackMutual.ilean
 lib/lean/Lean/Elab/PreDefinition/WF/PackMutual.olean
 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
@@ -1110,6 +1180,10 @@ lib/lean/Lean/Elab/Tactic/Repeat.ilean
 lib/lean/Lean/Elab/Tactic/Repeat.olean
 lib/lean/Lean/Elab/Tactic/Rewrite.ilean
 lib/lean/Lean/Elab/Tactic/Rewrite.olean
+lib/lean/Lean/Elab/Tactic/Rewrites.ilean
+lib/lean/Lean/Elab/Tactic/Rewrites.olean
+lib/lean/Lean/Elab/Tactic/Rfl.ilean
+lib/lean/Lean/Elab/Tactic/Rfl.olean
 lib/lean/Lean/Elab/Tactic/ShowTerm.ilean
 lib/lean/Lean/Elab/Tactic/ShowTerm.olean
 lib/lean/Lean/Elab/Tactic/Simp.ilean
@@ -1152,6 +1226,10 @@ lib/lean/Lean/KeyedDeclsAttribute.ilean
 lib/lean/Lean/KeyedDeclsAttribute.olean
 lib/lean/Lean/LabelAttribute.ilean
 lib/lean/Lean/LabelAttribute.olean
+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/LazyInitExtension.ilean
 lib/lean/Lean/LazyInitExtension.olean
 lib/lean/Lean/Level.ilean
@@ -1188,10 +1266,18 @@ lib/lean/Lean/Meta/AbstractNestedProofs.ilean
 lib/lean/Lean/Meta/AbstractNestedProofs.olean
 lib/lean/Lean/Meta/AppBuilder.ilean
 lib/lean/Lean/Meta/AppBuilder.olean
+lib/lean/Lean/Meta/ArgsPacker.ilean
+lib/lean/Lean/Meta/ArgsPacker.olean
+lib/lean/Lean/Meta/ArgsPacker/Basic.ilean
+lib/lean/Lean/Meta/ArgsPacker/Basic.olean
 lib/lean/Lean/Meta/Basic.ilean
 lib/lean/Lean/Meta/Basic.olean
+lib/lean/Lean/Meta/Canonicalizer.ilean
+lib/lean/Lean/Meta/Canonicalizer.olean
 lib/lean/Lean/Meta/Check.ilean
 lib/lean/Lean/Meta/Check.olean
+lib/lean/Lean/Meta/CheckTactic.ilean
+lib/lean/Lean/Meta/CheckTactic.olean
 lib/lean/Lean/Meta/Closure.ilean
 lib/lean/Lean/Meta/Closure.olean
 lib/lean/Lean/Meta/Coe.ilean
@@ -1212,6 +1298,8 @@ lib/lean/Lean/Meta/CtorRecognizer.ilean
 lib/lean/Lean/Meta/CtorRecognizer.olean
 lib/lean/Lean/Meta/DecLevel.ilean
 lib/lean/Lean/Meta/DecLevel.olean
+lib/lean/Lean/Meta/Diagnostics.ilean
+lib/lean/Lean/Meta/Diagnostics.olean
 lib/lean/Lean/Meta/DiscrTree.ilean
 lib/lean/Lean/Meta/DiscrTree.olean
 lib/lean/Lean/Meta/DiscrTreeTypes.ilean
@@ -1290,6 +1378,8 @@ lib/lean/Lean/Meta/Match/Value.ilean
 lib/lean/Lean/Meta/Match/Value.olean
 lib/lean/Lean/Meta/MatchUtil.ilean
 lib/lean/Lean/Meta/MatchUtil.olean
+lib/lean/Lean/Meta/NatInstTesters.ilean
+lib/lean/Lean/Meta/NatInstTesters.olean
 lib/lean/Lean/Meta/Offset.ilean
 lib/lean/Lean/Meta/Offset.olean
 lib/lean/Lean/Meta/PPGoal.ilean
@@ -1342,6 +1432,8 @@ lib/lean/Lean/Meta/Tactic/ElimInfo.ilean
 lib/lean/Lean/Meta/Tactic/ElimInfo.olean
 lib/lean/Lean/Meta/Tactic/FVarSubst.ilean
 lib/lean/Lean/Meta/Tactic/FVarSubst.olean
+lib/lean/Lean/Meta/Tactic/FunInd.ilean
+lib/lean/Lean/Meta/Tactic/FunInd.olean
 lib/lean/Lean/Meta/Tactic/Generalize.ilean
 lib/lean/Lean/Meta/Tactic/Generalize.olean
 lib/lean/Lean/Meta/Tactic/IndependentOf.ilean
@@ -1386,6 +1478,10 @@ lib/lean/Lean/Meta/Tactic/Revert.ilean
 lib/lean/Lean/Meta/Tactic/Revert.olean
 lib/lean/Lean/Meta/Tactic/Rewrite.ilean
 lib/lean/Lean/Meta/Tactic/Rewrite.olean
+lib/lean/Lean/Meta/Tactic/Rewrites.ilean
+lib/lean/Lean/Meta/Tactic/Rewrites.olean
+lib/lean/Lean/Meta/Tactic/Rfl.ilean
+lib/lean/Lean/Meta/Tactic/Rfl.olean
 lib/lean/Lean/Meta/Tactic/Simp.ilean
 lib/lean/Lean/Meta/Tactic/Simp.olean
 lib/lean/Lean/Meta/Tactic/Simp/Attr.ilean
@@ -1410,6 +1506,8 @@ lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.olean
+lib/lean/Lean/Meta/Tactic/Simp/Diagnostics.ilean
+lib/lean/Lean/Meta/Tactic/Simp/Diagnostics.olean
 lib/lean/Lean/Meta/Tactic/Simp/Main.ilean
 lib/lean/Lean/Meta/Tactic/Simp/Main.olean
 lib/lean/Lean/Meta/Tactic/Simp/RegisterCommand.ilean
@@ -1496,10 +1594,14 @@ lib/lean/Lean/PrettyPrinter/Basic.ilean
 lib/lean/Lean/PrettyPrinter/Basic.olean
 lib/lean/Lean/PrettyPrinter/Delaborator.ilean
 lib/lean/Lean/PrettyPrinter/Delaborator.olean
+lib/lean/Lean/PrettyPrinter/Delaborator/Attributes.ilean
+lib/lean/Lean/PrettyPrinter/Delaborator/Attributes.olean
 lib/lean/Lean/PrettyPrinter/Delaborator/Basic.ilean
 lib/lean/Lean/PrettyPrinter/Delaborator/Basic.olean
 lib/lean/Lean/PrettyPrinter/Delaborator/Builtins.ilean
 lib/lean/Lean/PrettyPrinter/Delaborator/Builtins.olean
+lib/lean/Lean/PrettyPrinter/Delaborator/FieldNotation.ilean
+lib/lean/Lean/PrettyPrinter/Delaborator/FieldNotation.olean
 lib/lean/Lean/PrettyPrinter/Delaborator/Options.ilean
 lib/lean/Lean/PrettyPrinter/Delaborator/Options.olean
 lib/lean/Lean/PrettyPrinter/Delaborator/SubExpr.ilean
@@ -1516,6 +1618,8 @@ lib/lean/Lean/ReducibilityAttrs.ilean
 lib/lean/Lean/ReducibilityAttrs.olean
 lib/lean/Lean/Replay.ilean
 lib/lean/Lean/Replay.olean
+lib/lean/Lean/ReservedNameAction.ilean
+lib/lean/Lean/ReservedNameAction.olean
 lib/lean/Lean/ResolveName.ilean
 lib/lean/Lean/ResolveName.olean
 lib/lean/Lean/Runtime.ilean
@@ -1590,6 +1694,8 @@ lib/lean/Lean/Util/CollectLevelParams.ilean
 lib/lean/Lean/Util/CollectLevelParams.olean
 lib/lean/Lean/Util/CollectMVars.ilean
 lib/lean/Lean/Util/CollectMVars.olean
+lib/lean/Lean/Util/Diff.ilean
+lib/lean/Lean/Util/Diff.olean
 lib/lean/Lean/Util/FileSetupInfo.ilean
 lib/lean/Lean/Util/FileSetupInfo.olean
 lib/lean/Lean/Util/FindExpr.ilean
@@ -1628,6 +1734,8 @@ lib/lean/Lean/Util/Paths.ilean
 lib/lean/Lean/Util/Paths.olean
 lib/lean/Lean/Util/Profile.ilean
 lib/lean/Lean/Util/Profile.olean
+lib/lean/Lean/Util/Profiler.ilean
+lib/lean/Lean/Util/Profiler.olean
 lib/lean/Lean/Util/PtrSet.ilean
 lib/lean/Lean/Util/PtrSet.olean
 lib/lean/Lean/Util/RecDepth.ilean
@@ -1686,6 +1794,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Control/ExceptCps.lean
 %%DATADIR%%/src/lean/Init/Control/Id.lean
 %%DATADIR%%/src/lean/Init/Control/Lawful.lean
+%%DATADIR%%/src/lean/Init/Control/Lawful/Basic.lean
+%%DATADIR%%/src/lean/Init/Control/Lawful/Instances.lean
 %%DATADIR%%/src/lean/Init/Control/Option.lean
 %%DATADIR%%/src/lean/Init/Control/Reader.lean
 %%DATADIR%%/src/lean/Init/Control/State.lean
@@ -1705,6 +1815,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Array/Mem.lean
 %%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/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/BitVec.lean
 %%DATADIR%%/src/lean/Init/Data/BitVec/Basic.lean
@@ -1741,20 +1852,24 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Int/Gcd.lean
 %%DATADIR%%/src/lean/Init/Data/Int/Lemmas.lean
 %%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/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/List/BasicAux.lean
 %%DATADIR%%/src/lean/Init/Data/List/Control.lean
+%%DATADIR%%/src/lean/Init/Data/List/Impl.lean
 %%DATADIR%%/src/lean/Init/Data/List/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Nat.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
+%%DATADIR%%/src/lean/Init/Data/Nat/Compare.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Control.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Div.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Dvd.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Gcd.lean
+%%DATADIR%%/src/lean/Init/Data/Nat/Lcm.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Linear.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Log2.lean
@@ -1762,6 +1877,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Nat/Mod.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Power2.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/SOM.lean
+%%DATADIR%%/src/lean/Init/Data/Nat/Simproc.lean
 %%DATADIR%%/src/lean/Init/Data/OfScientific.lean
 %%DATADIR%%/src/lean/Init/Data/Option.lean
 %%DATADIR%%/src/lean/Init/Data/Option/Basic.lean
@@ -1787,8 +1903,10 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean
 %%DATADIR%%/src/lean/Init/Dynamic.lean
 %%DATADIR%%/src/lean/Init/Ext.lean
+%%DATADIR%%/src/lean/Init/GetElem.lean
 %%DATADIR%%/src/lean/Init/Guard.lean
 %%DATADIR%%/src/lean/Init/Hints.lean
+%%DATADIR%%/src/lean/Init/MacroTrace.lean
 %%DATADIR%%/src/lean/Init/Meta.lean
 %%DATADIR%%/src/lean/Init/MetaTypes.lean
 %%DATADIR%%/src/lean/Init/Notation.lean
@@ -1825,6 +1943,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean.lean
 %%DATADIR%%/src/lean/Lean/Attributes.lean
 %%DATADIR%%/src/lean/Lean/AuxRecursor.lean
+%%DATADIR%%/src/lean/Lean/BuiltinDocAttr.lean
 %%DATADIR%%/src/lean/Lean/Class.lean
 %%DATADIR%%/src/lean/Lean/Compiler.lean
 %%DATADIR%%/src/lean/Lean/Compiler/AtMostOnce.lean
@@ -1966,6 +2085,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Data/Lsp/LanguageFeatures.lean
 %%DATADIR%%/src/lean/Lean/Data/Lsp/TextSync.lean
 %%DATADIR%%/src/lean/Lean/Data/Lsp/Utf16.lean
+%%DATADIR%%/src/lean/Lean/Data/Lsp/Window.lean
 %%DATADIR%%/src/lean/Lean/Data/Lsp/Workspace.lean
 %%DATADIR%%/src/lean/Lean/Data/Name.lean
 %%DATADIR%%/src/lean/Lean/Data/NameMap.lean
@@ -2008,6 +2128,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/ComputedFields.lean
 %%DATADIR%%/src/lean/Lean/Elab/Config.lean
 %%DATADIR%%/src/lean/Lean/Elab/DeclModifiers.lean
+%%DATADIR%%/src/lean/Lean/Elab/DeclNameGen.lean
 %%DATADIR%%/src/lean/Lean/Elab/DeclUtil.lean
 %%DATADIR%%/src/lean/Lean/Elab/Declaration.lean
 %%DATADIR%%/src/lean/Lean/Elab/DeclarationRange.lean
@@ -2073,10 +2194,10 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/GuessLex.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Ite.lean
 %%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/Main.lean
-%%DATADIR%%/src/lean/Lean/Elab/PreDefinition/WF/PackDomain.lean
 %%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
@@ -2126,6 +2247,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/RCases.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Repeat.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Rewrite.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Rewrites.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Rfl.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/ShowTerm.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Simp.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/SimpTrace.lean
@@ -2147,6 +2270,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/InternalExceptionId.lean
 %%DATADIR%%/src/lean/Lean/KeyedDeclsAttribute.lean
 %%DATADIR%%/src/lean/Lean/LabelAttribute.lean
+%%DATADIR%%/src/lean/Lean/Language/Basic.lean
+%%DATADIR%%/src/lean/Lean/Language/Lean.lean
 %%DATADIR%%/src/lean/Lean/LazyInitExtension.lean
 %%DATADIR%%/src/lean/Lean/Level.lean
 %%DATADIR%%/src/lean/Lean/Linter.lean
@@ -2165,8 +2290,12 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/AbstractMVars.lean
 %%DATADIR%%/src/lean/Lean/Meta/AbstractNestedProofs.lean
 %%DATADIR%%/src/lean/Lean/Meta/AppBuilder.lean
+%%DATADIR%%/src/lean/Lean/Meta/ArgsPacker.lean
+%%DATADIR%%/src/lean/Lean/Meta/ArgsPacker/Basic.lean
 %%DATADIR%%/src/lean/Lean/Meta/Basic.lean
+%%DATADIR%%/src/lean/Lean/Meta/Canonicalizer.lean
 %%DATADIR%%/src/lean/Lean/Meta/Check.lean
+%%DATADIR%%/src/lean/Lean/Meta/CheckTactic.lean
 %%DATADIR%%/src/lean/Lean/Meta/Closure.lean
 %%DATADIR%%/src/lean/Lean/Meta/Coe.lean
 %%DATADIR%%/src/lean/Lean/Meta/CoeAttr.lean
@@ -2177,6 +2306,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Constructions.lean
 %%DATADIR%%/src/lean/Lean/Meta/CtorRecognizer.lean
 %%DATADIR%%/src/lean/Lean/Meta/DecLevel.lean
+%%DATADIR%%/src/lean/Lean/Meta/Diagnostics.lean
 %%DATADIR%%/src/lean/Lean/Meta/DiscrTree.lean
 %%DATADIR%%/src/lean/Lean/Meta/DiscrTreeTypes.lean
 %%DATADIR%%/src/lean/Lean/Meta/Eqns.lean
@@ -2216,6 +2346,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Match/MatcherInfo.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match/Value.lean
 %%DATADIR%%/src/lean/Lean/Meta/MatchUtil.lean
+%%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/RecursorInfo.lean
@@ -2242,6 +2373,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Delta.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/ElimInfo.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/FVarSubst.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/FunInd.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Generalize.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/IndependentOf.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Induction.lean
@@ -2264,6 +2396,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Replace.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Revert.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Rewrite.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Rewrites.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Rfl.lean
 %%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
@@ -2276,6 +2410,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Diagnostics.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Main.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/RegisterCommand.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -2319,8 +2454,10 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/PrettyPrinter.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Basic.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator.lean
+%%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Attributes.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Basic.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Builtins.lean
+%%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/Options.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/SubExpr.lean
 %%DATADIR%%/src/lean/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -2329,6 +2466,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/ProjFns.lean
 %%DATADIR%%/src/lean/Lean/ReducibilityAttrs.lean
 %%DATADIR%%/src/lean/Lean/Replay.lean
+%%DATADIR%%/src/lean/Lean/ReservedNameAction.lean
 %%DATADIR%%/src/lean/Lean/ResolveName.lean
 %%DATADIR%%/src/lean/Lean/Runtime.lean
 %%DATADIR%%/src/lean/Lean/ScopedEnvExtension.lean
@@ -2367,6 +2505,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Util/CollectFVars.lean
 %%DATADIR%%/src/lean/Lean/Util/CollectLevelParams.lean
 %%DATADIR%%/src/lean/Lean/Util/CollectMVars.lean
+%%DATADIR%%/src/lean/Lean/Util/Diff.lean
 %%DATADIR%%/src/lean/Lean/Util/FileSetupInfo.lean
 %%DATADIR%%/src/lean/Lean/Util/FindExpr.lean
 %%DATADIR%%/src/lean/Lean/Util/FindLevelMVar.lean
@@ -2386,6 +2525,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Util/Path.lean
 %%DATADIR%%/src/lean/Lean/Util/Paths.lean
 %%DATADIR%%/src/lean/Lean/Util/Profile.lean
+%%DATADIR%%/src/lean/Lean/Util/Profiler.lean
 %%DATADIR%%/src/lean/Lean/Util/PtrSet.lean
 %%DATADIR%%/src/lean/Lean/Util/RecDepth.lean
 %%DATADIR%%/src/lean/Lean/Util/Recognizers.lean
@@ -2409,11 +2549,12 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake.lean
 %%DATADIR%%/src/lean/lake/Lake/Build.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean
+%%DATADIR%%/src/lean/lake/Lake/Build/Basic.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Common.lean
-%%DATADIR%%/src/lean/lake/Lake/Build/Context.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Data.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Executable.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Facets.lean
+%%DATADIR%%/src/lean/lake/Lake/Build/Fetch.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Imports.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Index.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Info.lean
@@ -2421,8 +2562,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/Build/Key.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Library.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Module.lean
-%%DATADIR%%/src/lean/lake/Lake/Build/Monad.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Package.lean
+%%DATADIR%%/src/lean/lake/Lake/Build/Run.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Store.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Targets.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Topological.lean
@@ -2435,6 +2576,9 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/CLI/Init.lean
 %%DATADIR%%/src/lean/lake/Lake/CLI/Main.lean
 %%DATADIR%%/src/lean/lake/Lake/CLI/Serve.lean
+%%DATADIR%%/src/lean/lake/Lake/CLI/Translate.lean
+%%DATADIR%%/src/lean/lake/Lake/CLI/Translate/Lean.lean
+%%DATADIR%%/src/lean/lake/Lake/CLI/Translate/Toml.lean
 %%DATADIR%%/src/lean/lake/Lake/Config.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/Context.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/Defaults.lean
@@ -2445,6 +2589,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/Config/FacetConfig.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/Glob.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/InstallPath.lean
+%%DATADIR%%/src/lean/lake/Lake/Config/Lang.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/LeanConfig.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/LeanExe.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/LeanExeConfig.lean
@@ -2475,8 +2620,21 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/Load/Manifest.lean
 %%DATADIR%%/src/lean/lake/Lake/Load/Materialize.lean
 %%DATADIR%%/src/lean/lake/Lake/Load/Package.lean
+%%DATADIR%%/src/lean/lake/Lake/Load/Toml.lean
 %%DATADIR%%/src/lean/lake/Lake/Main.lean
-%%DATADIR%%/src/lean/lake/Lake/Util/Async.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Data.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Data/DateTime.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Data/Dict.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Data/Value.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Decode.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Elab.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Elab/Expression.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Elab/Value.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Encode.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Grammar.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/Load.lean
+%%DATADIR%%/src/lean/lake/Lake/Toml/ParserUtil.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Binder.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Casing.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Cli.lean
@@ -2488,15 +2646,19 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/Util/Error.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Exit.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Family.lean
+%%DATADIR%%/src/lean/lake/Lake/Util/FilePath.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Git.lean
+%%DATADIR%%/src/lean/lake/Lake/Util/IO.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Lift.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/List.lean
+%%DATADIR%%/src/lean/lake/Lake/Util/Lock.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Log.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/MainM.lean
+%%DATADIR%%/src/lean/lake/Lake/Util/Message.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Name.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/NativeLib.lean
+%%DATADIR%%/src/lean/lake/Lake/Util/Newline.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Opaque.lean
-%%DATADIR%%/src/lean/lake/Lake/Util/OptionIO.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/OrdHashSet.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/OrderedTagAttribute.lean
 %%DATADIR%%/src/lean/lake/Lake/Util/Proc.lean
@@ -2510,6 +2672,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/badImport/Lib/A.lean
 %%DATADIR%%/src/lean/lake/tests/badImport/Lib/B.lean
+%%DATADIR%%/src/lean/lake/tests/badImport/Lib/C.lean
 %%DATADIR%%/src/lean/lake/tests/badImport/X.lean
 %%DATADIR%%/src/lean/lake/tests/badImport/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/buildArgs/Hello.lean
@@ -2524,6 +2687,10 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/globs/Test/1.lean
 %%DATADIR%%/src/lean/lake/tests/globs/Test/Subtest/1.lean
 %%DATADIR%%/src/lean/lake/tests/globs/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/lean/Lib.lean
+%%DATADIR%%/src/lean/lake/tests/lean/Lib/Basic.lean
+%%DATADIR%%/src/lean/lake/tests/lean/Test.lean
+%%DATADIR%%/src/lean/lake/tests/lean/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen.lean
 %%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/LlvmBitcodeGen/Basic.lean
 %%DATADIR%%/src/lean/lake/tests/llvm-bitcode-gen/Main.lean
@@ -2539,6 +2706,9 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/meta/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/noBuild/Test.lean
 %%DATADIR%%/src/lean/lake/tests/noBuild/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/noRelease/Test.lean
+%%DATADIR%%/src/lean/lake/tests/noRelease/dep/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/noRelease/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/order/A.lean
 %%DATADIR%%/src/lean/lake/tests/order/A/B.lean
 %%DATADIR%%/src/lean/lake/tests/order/A/B/C.lean
@@ -2558,3 +2728,17 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/precompileArgs/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/rebuild/Main.lean
 %%DATADIR%%/src/lean/lake/tests/rebuild/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean
+%%DATADIR%%/src/lean/lake/tests/reversion/Main.lean
+%%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/test/exe.lean
+%%DATADIR%%/src/lean/lake/tests/test/none.lean
+%%DATADIR%%/src/lean/lake/tests/test/script.lean
+%%DATADIR%%/src/lean/lake/tests/test/test.lean
+%%DATADIR%%/src/lean/lake/tests/test/two.lean
+%%DATADIR%%/src/lean/lake/tests/toml/README.md
+%%DATADIR%%/src/lean/lake/tests/toml/Test.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