math/lean4: update 4.6.0 → 4.7.0

Reported by:	portscout

5 files changed, 306 insertions, 23 deletions

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index cfb76980d3a5..66c8a8cf5adc 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.6.0
+DISTVERSION=	4.7.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
@@ -35,6 +35,7 @@ post-install:
 		bin/lake \
 		bin/lean \
 		bin/leanc \
+		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
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index d6ff8ff5f2c9..d20cb0cc673a 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1709183089
-SHA256 (leanprover-lean4-v4.6.0_GH0.tar.gz) = 9e90f38c9b55e8accc27f75394db1fcdb58bc4dc22ba99d1232e4921c66ff2af
-SIZE (leanprover-lean4-v4.6.0_GH0.tar.gz) = 17532157
+TIMESTAMP = 1713025323
+SHA256 (leanprover-lean4-v4.7.0_GH0.tar.gz) = b1f00b5f2431b34aeacba993c4f4675211a3827e96c4b1a06054c58188ae72c8
+SIZE (leanprover-lean4-v4.7.0_GH0.tar.gz) = 19261610
diff --git a/math/lean4/files/patch-src_CMakeLists.txt b/math/lean4/files/patch-src_CMakeLists.txt
index 6109d2793eac..98298fd62d75 100644
--- a/math/lean4/files/patch-src_CMakeLists.txt
+++ b/math/lean4/files/patch-src_CMakeLists.txt
@@ -1,18 +1,22 @@
---- src/CMakeLists.txt.orig	2023-12-21 22:11:33 UTC
+--- src/CMakeLists.txt.orig	2024-03-06 02:11:32 UTC
 +++ src/CMakeLists.txt
-@@ -352,6 +352,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+@@ -362,6 +362,15 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
    string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
-   string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
-   string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+   string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
+   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
 +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
++  if(BSYMBOLIC)
++    string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
++    string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
++  endif()
 +  string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
 +  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
-+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
-+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
++  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
++  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
  elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
    string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
-   string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
-@@ -592,7 +597,7 @@ endif()
+   string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
+@@ -624,7 +633,7 @@ endif()
    file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
  endif()
  
diff --git a/math/lean4/files/patch-stage0_src_CMakeLists.txt b/math/lean4/files/patch-stage0_src_CMakeLists.txt
index e8af91b549aa..ec7e8f739ef0 100644
--- a/math/lean4/files/patch-stage0_src_CMakeLists.txt
+++ b/math/lean4/files/patch-stage0_src_CMakeLists.txt
@@ -1,18 +1,22 @@
---- stage0/src/CMakeLists.txt.orig	2023-12-21 22:11:33 UTC
+--- stage0/src/CMakeLists.txt.orig	2024-03-06 02:11:32 UTC
 +++ stage0/src/CMakeLists.txt
-@@ -352,6 +352,11 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
+@@ -362,6 +362,15 @@ if(${CMAKE_SYSTEM_NAME} MATCHES "Linux")
    string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
-   string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
-   string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
+   string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
+   string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
 +elseif(${CMAKE_SYSTEM_NAME} MATCHES "FreeBSD")
++  if(BSYMBOLIC)
++    string(APPEND LEANC_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
++    string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-Bsymbolic")
++  endif()
 +  string(APPEND CMAKE_CXX_FLAGS " -fPIC -ftls-model=initial-exec")
 +  string(APPEND LEANC_EXTRA_FLAGS " -fPIC")
-+  string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
-+  string(APPEND CMAKE_EXE_LINKER_FLAGS " -lleanshared -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
++  string(APPEND TOOLCHAIN_SHARED_LINKER_FLAGS " -Wl,-rpath=\\$$ORIGIN/..:\\$$ORIGIN")
++  string(APPEND CMAKE_EXE_LINKER_FLAGS " -Wl,-rpath=\\\$ORIGIN/../lib:\\\$ORIGIN/../lib/lean")
  elseif(${CMAKE_SYSTEM_NAME} MATCHES "Darwin")
    string(APPEND CMAKE_CXX_FLAGS " -ftls-model=initial-exec")
-   string(APPEND LEANSHARED_LINKER_FLAGS " -install_name @rpath/libleanshared.dylib")
-@@ -592,7 +597,7 @@ endif()
+   string(APPEND INIT_SHARED_LINKER_FLAGS " -install_name @rpath/libInit_shared.dylib")
+@@ -624,7 +633,7 @@ endif()
    file(CREATE_LINK ${CMAKE_SOURCE_DIR} ${CMAKE_BINARY_DIR}/src/lean RESULT _IGNORE_RES SYMBOLIC)
  endif()
  
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 3d78573ad15e..5b2bc5e8899c 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -8,6 +8,10 @@ include/lean/lean_gmp.h
 include/lean/version.h
 lib/lean/Init.ilean
 lib/lean/Init.olean
+lib/lean/Init/BinderPredicates.ilean
+lib/lean/Init/BinderPredicates.olean
+lib/lean/Init/ByCases.ilean
+lib/lean/Init/ByCases.olean
 lib/lean/Init/Classical.ilean
 lib/lean/Init/Classical.olean
 lib/lean/Init/Coe.ilean
@@ -56,6 +60,8 @@ lib/lean/Init/Data/Array/DecidableEq.ilean
 lib/lean/Init/Data/Array/DecidableEq.olean
 lib/lean/Init/Data/Array/InsertionSort.ilean
 lib/lean/Init/Data/Array/InsertionSort.olean
+lib/lean/Init/Data/Array/Lemmas.ilean
+lib/lean/Init/Data/Array/Lemmas.olean
 lib/lean/Init/Data/Array/Mem.ilean
 lib/lean/Init/Data/Array/Mem.olean
 lib/lean/Init/Data/Array/QSort.ilean
@@ -64,10 +70,24 @@ lib/lean/Init/Data/Array/Subarray.ilean
 lib/lean/Init/Data/Array/Subarray.olean
 lib/lean/Init/Data/Basic.ilean
 lib/lean/Init/Data/Basic.olean
+lib/lean/Init/Data/BitVec.ilean
+lib/lean/Init/Data/BitVec.olean
+lib/lean/Init/Data/BitVec/Basic.ilean
+lib/lean/Init/Data/BitVec/Basic.olean
+lib/lean/Init/Data/BitVec/Bitblast.ilean
+lib/lean/Init/Data/BitVec/Bitblast.olean
+lib/lean/Init/Data/BitVec/Folds.ilean
+lib/lean/Init/Data/BitVec/Folds.olean
+lib/lean/Init/Data/BitVec/Lemmas.ilean
+lib/lean/Init/Data/BitVec/Lemmas.olean
+lib/lean/Init/Data/Bool.ilean
+lib/lean/Init/Data/Bool.olean
 lib/lean/Init/Data/ByteArray.ilean
 lib/lean/Init/Data/ByteArray.olean
 lib/lean/Init/Data/ByteArray/Basic.ilean
 lib/lean/Init/Data/ByteArray/Basic.olean
+lib/lean/Init/Data/Cast.ilean
+lib/lean/Init/Data/Cast.olean
 lib/lean/Init/Data/Channel.ilean
 lib/lean/Init/Data/Channel.olean
 lib/lean/Init/Data/Char.ilean
@@ -78,6 +98,12 @@ 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/Fold.ilean
+lib/lean/Init/Data/Fin/Fold.olean
+lib/lean/Init/Data/Fin/Iterate.ilean
+lib/lean/Init/Data/Fin/Iterate.olean
+lib/lean/Init/Data/Fin/Lemmas.ilean
+lib/lean/Init/Data/Fin/Lemmas.olean
 lib/lean/Init/Data/Fin/Log2.ilean
 lib/lean/Init/Data/Fin/Log2.olean
 lib/lean/Init/Data/Float.ilean
@@ -102,6 +128,18 @@ lib/lean/Init/Data/Int.ilean
 lib/lean/Init/Data/Int.olean
 lib/lean/Init/Data/Int/Basic.ilean
 lib/lean/Init/Data/Int/Basic.olean
+lib/lean/Init/Data/Int/Bitwise.ilean
+lib/lean/Init/Data/Int/Bitwise.olean
+lib/lean/Init/Data/Int/DivMod.ilean
+lib/lean/Init/Data/Int/DivMod.olean
+lib/lean/Init/Data/Int/DivModLemmas.ilean
+lib/lean/Init/Data/Int/DivModLemmas.olean
+lib/lean/Init/Data/Int/Gcd.ilean
+lib/lean/Init/Data/Int/Gcd.olean
+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/List.ilean
 lib/lean/Init/Data/List.olean
 lib/lean/Init/Data/List/Basic.ilean
@@ -110,22 +148,36 @@ 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/Lemmas.ilean
+lib/lean/Init/Data/List/Lemmas.olean
 lib/lean/Init/Data/Nat.ilean
 lib/lean/Init/Data/Nat.olean
 lib/lean/Init/Data/Nat/Basic.ilean
 lib/lean/Init/Data/Nat/Basic.olean
 lib/lean/Init/Data/Nat/Bitwise.ilean
 lib/lean/Init/Data/Nat/Bitwise.olean
+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/Control.ilean
 lib/lean/Init/Data/Nat/Control.olean
 lib/lean/Init/Data/Nat/Div.ilean
 lib/lean/Init/Data/Nat/Div.olean
+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/Lemmas.ilean
+lib/lean/Init/Data/Nat/Lemmas.olean
 lib/lean/Init/Data/Nat/Linear.ilean
 lib/lean/Init/Data/Nat/Linear.olean
 lib/lean/Init/Data/Nat/Log2.ilean
 lib/lean/Init/Data/Nat/Log2.olean
+lib/lean/Init/Data/Nat/MinMax.ilean
+lib/lean/Init/Data/Nat/MinMax.olean
+lib/lean/Init/Data/Nat/Mod.ilean
+lib/lean/Init/Data/Nat/Mod.olean
 lib/lean/Init/Data/Nat/Power2.ilean
 lib/lean/Init/Data/Nat/Power2.olean
 lib/lean/Init/Data/Nat/SOM.ilean
@@ -140,6 +192,8 @@ lib/lean/Init/Data/Option/BasicAux.ilean
 lib/lean/Init/Data/Option/BasicAux.olean
 lib/lean/Init/Data/Option/Instances.ilean
 lib/lean/Init/Data/Option/Instances.olean
+lib/lean/Init/Data/Option/Lemmas.ilean
+lib/lean/Init/Data/Option/Lemmas.olean
 lib/lean/Init/Data/Ord.ilean
 lib/lean/Init/Data/Ord.olean
 lib/lean/Init/Data/Prod.ilean
@@ -160,6 +214,8 @@ lib/lean/Init/Data/String/Basic.ilean
 lib/lean/Init/Data/String/Basic.olean
 lib/lean/Init/Data/String/Extra.ilean
 lib/lean/Init/Data/String/Extra.olean
+lib/lean/Init/Data/Sum.ilean
+lib/lean/Init/Data/Sum.olean
 lib/lean/Init/Data/ToString.ilean
 lib/lean/Init/Data/ToString.olean
 lib/lean/Init/Data/ToString/Basic.ilean
@@ -174,6 +230,10 @@ lib/lean/Init/Data/UInt/Log2.ilean
 lib/lean/Init/Data/UInt/Log2.olean
 lib/lean/Init/Dynamic.ilean
 lib/lean/Init/Dynamic.olean
+lib/lean/Init/Ext.ilean
+lib/lean/Init/Ext.olean
+lib/lean/Init/Guard.ilean
+lib/lean/Init/Guard.olean
 lib/lean/Init/Hints.ilean
 lib/lean/Init/Hints.olean
 lib/lean/Init/Meta.ilean
@@ -184,8 +244,26 @@ lib/lean/Init/Notation.ilean
 lib/lean/Init/Notation.olean
 lib/lean/Init/NotationExtra.ilean
 lib/lean/Init/NotationExtra.olean
+lib/lean/Init/Omega.ilean
+lib/lean/Init/Omega.olean
+lib/lean/Init/Omega/Coeffs.ilean
+lib/lean/Init/Omega/Coeffs.olean
+lib/lean/Init/Omega/Constraint.ilean
+lib/lean/Init/Omega/Constraint.olean
+lib/lean/Init/Omega/Int.ilean
+lib/lean/Init/Omega/Int.olean
+lib/lean/Init/Omega/IntList.ilean
+lib/lean/Init/Omega/IntList.olean
+lib/lean/Init/Omega/LinearCombo.ilean
+lib/lean/Init/Omega/LinearCombo.olean
+lib/lean/Init/Omega/Logic.ilean
+lib/lean/Init/Omega/Logic.olean
 lib/lean/Init/Prelude.ilean
 lib/lean/Init/Prelude.olean
+lib/lean/Init/PropLemmas.ilean
+lib/lean/Init/PropLemmas.olean
+lib/lean/Init/RCases.ilean
+lib/lean/Init/RCases.olean
 lib/lean/Init/ShareCommon.ilean
 lib/lean/Init/ShareCommon.olean
 lib/lean/Init/SimpLemmas.ilean
@@ -216,6 +294,8 @@ lib/lean/Init/System/Uri.ilean
 lib/lean/Init/System/Uri.olean
 lib/lean/Init/Tactics.ilean
 lib/lean/Init/Tactics.olean
+lib/lean/Init/TacticsExtra.ilean
+lib/lean/Init/TacticsExtra.olean
 lib/lean/Init/Util.ilean
 lib/lean/Init/Util.olean
 lib/lean/Init/WF.ilean
@@ -284,6 +364,8 @@ lib/lean/Lake/Config.ilean
 lib/lean/Lake/Config.olean
 lib/lean/Lake/Config/Context.ilean
 lib/lean/Lake/Config/Context.olean
+lib/lean/Lake/Config/Defaults.ilean
+lib/lean/Lake/Config/Defaults.olean
 lib/lean/Lake/Config/Dependency.ilean
 lib/lean/Lake/Config/Dependency.olean
 lib/lean/Lake/Config/Env.ilean
@@ -662,6 +744,8 @@ lib/lean/Lean/Data/Json.ilean
 lib/lean/Lean/Data/Json.olean
 lib/lean/Lean/Data/Json/Basic.ilean
 lib/lean/Lean/Data/Json/Basic.olean
+lib/lean/Lean/Data/Json/Elab.ilean
+lib/lean/Lean/Data/Json/Elab.olean
 lib/lean/Lean/Data/Json/FromToJson.ilean
 lib/lean/Lean/Data/Json/FromToJson.olean
 lib/lean/Lean/Data/Json/Parser.ilean
@@ -766,6 +850,8 @@ lib/lean/Lean/Elab/AutoBound.ilean
 lib/lean/Lean/Elab/AutoBound.olean
 lib/lean/Lean/Elab/AuxDef.ilean
 lib/lean/Lean/Elab/AuxDef.olean
+lib/lean/Lean/Elab/BinderPredicates.ilean
+lib/lean/Lean/Elab/BinderPredicates.olean
 lib/lean/Lean/Elab/Binders.ilean
 lib/lean/Lean/Elab/Binders.olean
 lib/lean/Lean/Elab/BindersUtil.ilean
@@ -778,6 +864,8 @@ lib/lean/Lean/Elab/BuiltinTerm.ilean
 lib/lean/Lean/Elab/BuiltinTerm.olean
 lib/lean/Lean/Elab/Calc.ilean
 lib/lean/Lean/Elab/Calc.olean
+lib/lean/Lean/Elab/CheckTactic.ilean
+lib/lean/Lean/Elab/CheckTactic.olean
 lib/lean/Lean/Elab/Command.ilean
 lib/lean/Lean/Elab/Command.olean
 lib/lean/Lean/Elab/ComputedFields.ilean
@@ -834,6 +922,8 @@ lib/lean/Lean/Elab/Frontend.ilean
 lib/lean/Lean/Elab/Frontend.olean
 lib/lean/Lean/Elab/GenInjective.ilean
 lib/lean/Lean/Elab/GenInjective.olean
+lib/lean/Lean/Elab/GuardMsgs.ilean
+lib/lean/Lean/Elab/GuardMsgs.olean
 lib/lean/Lean/Elab/Import.ilean
 lib/lean/Lean/Elab/Import.olean
 lib/lean/Lean/Elab/Inductive.ilean
@@ -860,6 +950,8 @@ lib/lean/Lean/Elab/Match.ilean
 lib/lean/Lean/Elab/Match.olean
 lib/lean/Lean/Elab/MatchAltView.ilean
 lib/lean/Lean/Elab/MatchAltView.olean
+lib/lean/Lean/Elab/MatchExpr.ilean
+lib/lean/Lean/Elab/MatchExpr.olean
 lib/lean/Lean/Elab/Mixfix.ilean
 lib/lean/Lean/Elab/Mixfix.olean
 lib/lean/Lean/Elab/MutualDef.ilean
@@ -952,6 +1044,8 @@ lib/lean/Lean/Elab/Tactic/Cache.ilean
 lib/lean/Lean/Elab/Tactic/Cache.olean
 lib/lean/Lean/Elab/Tactic/Calc.ilean
 lib/lean/Lean/Elab/Tactic/Calc.olean
+lib/lean/Lean/Elab/Tactic/Change.ilean
+lib/lean/Lean/Elab/Tactic/Change.olean
 lib/lean/Lean/Elab/Tactic/Config.ilean
 lib/lean/Lean/Elab/Tactic/Config.olean
 lib/lean/Lean/Elab/Tactic/Congr.ilean
@@ -978,26 +1072,60 @@ lib/lean/Lean/Elab/Tactic/Delta.ilean
 lib/lean/Lean/Elab/Tactic/Delta.olean
 lib/lean/Lean/Elab/Tactic/ElabTerm.ilean
 lib/lean/Lean/Elab/Tactic/ElabTerm.olean
+lib/lean/Lean/Elab/Tactic/Ext.ilean
+lib/lean/Lean/Elab/Tactic/Ext.olean
+lib/lean/Lean/Elab/Tactic/FalseOrByContra.ilean
+lib/lean/Lean/Elab/Tactic/FalseOrByContra.olean
 lib/lean/Lean/Elab/Tactic/Generalize.ilean
 lib/lean/Lean/Elab/Tactic/Generalize.olean
+lib/lean/Lean/Elab/Tactic/Guard.ilean
+lib/lean/Lean/Elab/Tactic/Guard.olean
 lib/lean/Lean/Elab/Tactic/Induction.ilean
 lib/lean/Lean/Elab/Tactic/Induction.olean
 lib/lean/Lean/Elab/Tactic/Injection.ilean
 lib/lean/Lean/Elab/Tactic/Injection.olean
+lib/lean/Lean/Elab/Tactic/LibrarySearch.ilean
+lib/lean/Lean/Elab/Tactic/LibrarySearch.olean
 lib/lean/Lean/Elab/Tactic/Location.ilean
 lib/lean/Lean/Elab/Tactic/Location.olean
 lib/lean/Lean/Elab/Tactic/Match.ilean
 lib/lean/Lean/Elab/Tactic/Match.olean
 lib/lean/Lean/Elab/Tactic/Meta.ilean
 lib/lean/Lean/Elab/Tactic/Meta.olean
+lib/lean/Lean/Elab/Tactic/NormCast.ilean
+lib/lean/Lean/Elab/Tactic/NormCast.olean
+lib/lean/Lean/Elab/Tactic/Omega.ilean
+lib/lean/Lean/Elab/Tactic/Omega.olean
+lib/lean/Lean/Elab/Tactic/Omega/Core.ilean
+lib/lean/Lean/Elab/Tactic/Omega/Core.olean
+lib/lean/Lean/Elab/Tactic/Omega/Frontend.ilean
+lib/lean/Lean/Elab/Tactic/Omega/Frontend.olean
+lib/lean/Lean/Elab/Tactic/Omega/MinNatAbs.ilean
+lib/lean/Lean/Elab/Tactic/Omega/MinNatAbs.olean
+lib/lean/Lean/Elab/Tactic/Omega/OmegaM.ilean
+lib/lean/Lean/Elab/Tactic/Omega/OmegaM.olean
+lib/lean/Lean/Elab/Tactic/RCases.ilean
+lib/lean/Lean/Elab/Tactic/RCases.olean
+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/ShowTerm.ilean
+lib/lean/Lean/Elab/Tactic/ShowTerm.olean
 lib/lean/Lean/Elab/Tactic/Simp.ilean
 lib/lean/Lean/Elab/Tactic/Simp.olean
+lib/lean/Lean/Elab/Tactic/SimpTrace.ilean
+lib/lean/Lean/Elab/Tactic/SimpTrace.olean
+lib/lean/Lean/Elab/Tactic/Simpa.ilean
+lib/lean/Lean/Elab/Tactic/Simpa.olean
 lib/lean/Lean/Elab/Tactic/Simproc.ilean
 lib/lean/Lean/Elab/Tactic/Simproc.olean
+lib/lean/Lean/Elab/Tactic/SolveByElim.ilean
+lib/lean/Lean/Elab/Tactic/SolveByElim.olean
 lib/lean/Lean/Elab/Tactic/Split.ilean
 lib/lean/Lean/Elab/Tactic/Split.olean
+lib/lean/Lean/Elab/Tactic/Symm.ilean
+lib/lean/Lean/Elab/Tactic/Symm.olean
 lib/lean/Lean/Elab/Tactic/Unfold.ilean
 lib/lean/Lean/Elab/Tactic/Unfold.olean
 lib/lean/Lean/Elab/Term.ilean
@@ -1022,6 +1150,8 @@ lib/lean/Lean/InternalExceptionId.ilean
 lib/lean/Lean/InternalExceptionId.olean
 lib/lean/Lean/KeyedDeclsAttribute.ilean
 lib/lean/Lean/KeyedDeclsAttribute.olean
+lib/lean/Lean/LabelAttribute.ilean
+lib/lean/Lean/LabelAttribute.olean
 lib/lean/Lean/LazyInitExtension.ilean
 lib/lean/Lean/LazyInitExtension.olean
 lib/lean/Lean/Level.ilean
@@ -1060,22 +1190,26 @@ lib/lean/Lean/Meta/AppBuilder.ilean
 lib/lean/Lean/Meta/AppBuilder.olean
 lib/lean/Lean/Meta/Basic.ilean
 lib/lean/Lean/Meta/Basic.olean
-lib/lean/Lean/Meta/CasesOn.ilean
-lib/lean/Lean/Meta/CasesOn.olean
 lib/lean/Lean/Meta/Check.ilean
 lib/lean/Lean/Meta/Check.olean
 lib/lean/Lean/Meta/Closure.ilean
 lib/lean/Lean/Meta/Closure.olean
 lib/lean/Lean/Meta/Coe.ilean
 lib/lean/Lean/Meta/Coe.olean
+lib/lean/Lean/Meta/CoeAttr.ilean
+lib/lean/Lean/Meta/CoeAttr.olean
 lib/lean/Lean/Meta/CollectFVars.ilean
 lib/lean/Lean/Meta/CollectFVars.olean
 lib/lean/Lean/Meta/CollectMVars.ilean
 lib/lean/Lean/Meta/CollectMVars.olean
+lib/lean/Lean/Meta/CompletionName.ilean
+lib/lean/Lean/Meta/CompletionName.olean
 lib/lean/Lean/Meta/CongrTheorems.ilean
 lib/lean/Lean/Meta/CongrTheorems.olean
 lib/lean/Lean/Meta/Constructions.ilean
 lib/lean/Lean/Meta/Constructions.olean
+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/DiscrTree.ilean
@@ -1114,12 +1248,18 @@ lib/lean/Lean/Meta/Injective.ilean
 lib/lean/Lean/Meta/Injective.olean
 lib/lean/Lean/Meta/Instances.ilean
 lib/lean/Lean/Meta/Instances.olean
+lib/lean/Lean/Meta/Iterator.ilean
+lib/lean/Lean/Meta/Iterator.olean
 lib/lean/Lean/Meta/KAbstract.ilean
 lib/lean/Lean/Meta/KAbstract.olean
 lib/lean/Lean/Meta/KExprMap.ilean
 lib/lean/Lean/Meta/KExprMap.olean
+lib/lean/Lean/Meta/LazyDiscrTree.ilean
+lib/lean/Lean/Meta/LazyDiscrTree.olean
 lib/lean/Lean/Meta/LevelDefEq.ilean
 lib/lean/Lean/Meta/LevelDefEq.olean
+lib/lean/Lean/Meta/LitValues.ilean
+lib/lean/Lean/Meta/LitValues.olean
 lib/lean/Lean/Meta/Match.ilean
 lib/lean/Lean/Meta/Match.olean
 lib/lean/Lean/Meta/Match/Basic.ilean
@@ -1138,6 +1278,12 @@ lib/lean/Lean/Meta/Match/MatchEqsExt.ilean
 lib/lean/Lean/Meta/Match/MatchEqsExt.olean
 lib/lean/Lean/Meta/Match/MatchPatternAttr.ilean
 lib/lean/Lean/Meta/Match/MatchPatternAttr.olean
+lib/lean/Lean/Meta/Match/MatcherApp.ilean
+lib/lean/Lean/Meta/Match/MatcherApp.olean
+lib/lean/Lean/Meta/Match/MatcherApp/Basic.ilean
+lib/lean/Lean/Meta/Match/MatcherApp/Basic.olean
+lib/lean/Lean/Meta/Match/MatcherApp/Transform.ilean
+lib/lean/Lean/Meta/Match/MatcherApp/Transform.olean
 lib/lean/Lean/Meta/Match/MatcherInfo.ilean
 lib/lean/Lean/Meta/Match/MatcherInfo.olean
 lib/lean/Lean/Meta/Match/Value.ilean
@@ -1176,6 +1322,8 @@ lib/lean/Lean/Meta/Tactic/Assumption.ilean
 lib/lean/Lean/Meta/Tactic/Assumption.olean
 lib/lean/Lean/Meta/Tactic/AuxLemma.ilean
 lib/lean/Lean/Meta/Tactic/AuxLemma.olean
+lib/lean/Lean/Meta/Tactic/Backtrack.ilean
+lib/lean/Lean/Meta/Tactic/Backtrack.olean
 lib/lean/Lean/Meta/Tactic/Cases.ilean
 lib/lean/Lean/Meta/Tactic/Cases.olean
 lib/lean/Lean/Meta/Tactic/Cleanup.ilean
@@ -1196,12 +1344,16 @@ lib/lean/Lean/Meta/Tactic/FVarSubst.ilean
 lib/lean/Lean/Meta/Tactic/FVarSubst.olean
 lib/lean/Lean/Meta/Tactic/Generalize.ilean
 lib/lean/Lean/Meta/Tactic/Generalize.olean
+lib/lean/Lean/Meta/Tactic/IndependentOf.ilean
+lib/lean/Lean/Meta/Tactic/IndependentOf.olean
 lib/lean/Lean/Meta/Tactic/Induction.ilean
 lib/lean/Lean/Meta/Tactic/Induction.olean
 lib/lean/Lean/Meta/Tactic/Injection.ilean
 lib/lean/Lean/Meta/Tactic/Injection.olean
 lib/lean/Lean/Meta/Tactic/Intro.ilean
 lib/lean/Lean/Meta/Tactic/Intro.olean
+lib/lean/Lean/Meta/Tactic/LibrarySearch.ilean
+lib/lean/Lean/Meta/Tactic/LibrarySearch.olean
 lib/lean/Lean/Meta/Tactic/LinearArith.ilean
 lib/lean/Lean/Meta/Tactic/LinearArith.olean
 lib/lean/Lean/Meta/Tactic/LinearArith/Basic.ilean
@@ -1220,10 +1372,14 @@ lib/lean/Lean/Meta/Tactic/LinearArith/Simp.ilean
 lib/lean/Lean/Meta/Tactic/LinearArith/Simp.olean
 lib/lean/Lean/Meta/Tactic/LinearArith/Solver.ilean
 lib/lean/Lean/Meta/Tactic/LinearArith/Solver.olean
+lib/lean/Lean/Meta/Tactic/NormCast.ilean
+lib/lean/Lean/Meta/Tactic/NormCast.olean
 lib/lean/Lean/Meta/Tactic/Refl.ilean
 lib/lean/Lean/Meta/Tactic/Refl.olean
 lib/lean/Lean/Meta/Tactic/Rename.ilean
 lib/lean/Lean/Meta/Tactic/Rename.olean
+lib/lean/Lean/Meta/Tactic/Repeat.ilean
+lib/lean/Lean/Meta/Tactic/Repeat.olean
 lib/lean/Lean/Meta/Tactic/Replace.ilean
 lib/lean/Lean/Meta/Tactic/Replace.olean
 lib/lean/Lean/Meta/Tactic/Revert.ilean
@@ -1232,8 +1388,14 @@ lib/lean/Lean/Meta/Tactic/Rewrite.ilean
 lib/lean/Lean/Meta/Tactic/Rewrite.olean
 lib/lean/Lean/Meta/Tactic/Simp.ilean
 lib/lean/Lean/Meta/Tactic/Simp.olean
+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/BitVec.ilean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.olean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.ilean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Char.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Core.olean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.ilean
@@ -1242,8 +1404,12 @@ 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/Nat.ilean
 lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.olean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.ilean
+lib/lean/Lean/Meta/Tactic/Simp/BuiltinSimprocs/String.olean
 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/Main.ilean
 lib/lean/Lean/Meta/Tactic/Simp/Main.olean
 lib/lean/Lean/Meta/Tactic/Simp/RegisterCommand.ilean
@@ -1260,12 +1426,18 @@ lib/lean/Lean/Meta/Tactic/Simp/Simproc.ilean
 lib/lean/Lean/Meta/Tactic/Simp/Simproc.olean
 lib/lean/Lean/Meta/Tactic/Simp/Types.ilean
 lib/lean/Lean/Meta/Tactic/Simp/Types.olean
+lib/lean/Lean/Meta/Tactic/SolveByElim.ilean
+lib/lean/Lean/Meta/Tactic/SolveByElim.olean
 lib/lean/Lean/Meta/Tactic/Split.ilean
 lib/lean/Lean/Meta/Tactic/Split.olean
 lib/lean/Lean/Meta/Tactic/SplitIf.ilean
 lib/lean/Lean/Meta/Tactic/SplitIf.olean
 lib/lean/Lean/Meta/Tactic/Subst.ilean
 lib/lean/Lean/Meta/Tactic/Subst.olean
+lib/lean/Lean/Meta/Tactic/Symm.ilean
+lib/lean/Lean/Meta/Tactic/Symm.olean
+lib/lean/Lean/Meta/Tactic/TryThis.ilean
+lib/lean/Lean/Meta/Tactic/TryThis.olean
 lib/lean/Lean/Meta/Tactic/Unfold.ilean
 lib/lean/Lean/Meta/Tactic/Unfold.olean
 lib/lean/Lean/Meta/Tactic/UnifyEq.ilean
@@ -1356,8 +1528,16 @@ lib/lean/Lean/Server/AsyncList.ilean
 lib/lean/Lean/Server/AsyncList.olean
 lib/lean/Lean/Server/CodeActions.ilean
 lib/lean/Lean/Server/CodeActions.olean
+lib/lean/Lean/Server/CodeActions/Attr.ilean
+lib/lean/Lean/Server/CodeActions/Attr.olean
+lib/lean/Lean/Server/CodeActions/Basic.ilean
+lib/lean/Lean/Server/CodeActions/Basic.olean
+lib/lean/Lean/Server/CodeActions/Provider.ilean
+lib/lean/Lean/Server/CodeActions/Provider.olean
 lib/lean/Lean/Server/Completion.ilean
 lib/lean/Lean/Server/Completion.olean
+lib/lean/Lean/Server/CompletionItemData.ilean
+lib/lean/Lean/Server/CompletionItemData.olean
 lib/lean/Lean/Server/FileSource.ilean
 lib/lean/Lean/Server/FileSource.olean
 lib/lean/Lean/Server/FileWorker.ilean
@@ -1426,6 +1606,8 @@ lib/lean/Lean/Util/ForEachExprWhere.ilean
 lib/lean/Lean/Util/ForEachExprWhere.olean
 lib/lean/Lean/Util/HasConstCache.ilean
 lib/lean/Lean/Util/HasConstCache.olean
+lib/lean/Lean/Util/Heartbeats.ilean
+lib/lean/Lean/Util/Heartbeats.olean
 lib/lean/Lean/Util/InstantiateLevelParams.ilean
 lib/lean/Lean/Util/InstantiateLevelParams.olean
 lib/lean/Lean/Util/LakePath.ilean
@@ -1485,6 +1667,7 @@ lib/lean/Lean/Widget/Types.olean
 lib/lean/Lean/Widget/UserWidget.ilean
 lib/lean/Lean/Widget/UserWidget.olean
 lib/lean/libInit.a
+lib/lean/libInit_shared.so
 lib/lean/libLake.a
 lib/lean/libLean.a
 lib/lean/libleancpp.a
@@ -1492,6 +1675,8 @@ lib/lean/libleanrt.a
 lib/lean/libleanshared.so
 share/lean/lean.mk
 %%DATADIR%%/src/lean/Init.lean
+%%DATADIR%%/src/lean/Init/BinderPredicates.lean
+%%DATADIR%%/src/lean/Init/ByCases.lean
 %%DATADIR%%/src/lean/Init/Classical.lean
 %%DATADIR%%/src/lean/Init/Coe.lean
 %%DATADIR%%/src/lean/Init/Control.lean
@@ -1516,17 +1701,28 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Array/BinSearch.lean
 %%DATADIR%%/src/lean/Init/Data/Array/DecidableEq.lean
 %%DATADIR%%/src/lean/Init/Data/Array/InsertionSort.lean
+%%DATADIR%%/src/lean/Init/Data/Array/Lemmas.lean
 %%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/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/BitVec.lean
+%%DATADIR%%/src/lean/Init/Data/BitVec/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/BitVec/Bitblast.lean
+%%DATADIR%%/src/lean/Init/Data/BitVec/Folds.lean
+%%DATADIR%%/src/lean/Init/Data/BitVec/Lemmas.lean
+%%DATADIR%%/src/lean/Init/Data/Bool.lean
 %%DATADIR%%/src/lean/Init/Data/ByteArray.lean
 %%DATADIR%%/src/lean/Init/Data/ByteArray/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/Cast.lean
 %%DATADIR%%/src/lean/Init/Data/Channel.lean
 %%DATADIR%%/src/lean/Init/Data/Char.lean
 %%DATADIR%%/src/lean/Init/Data/Char/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/Fin.lean
 %%DATADIR%%/src/lean/Init/Data/Fin/Basic.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
 %%DATADIR%%/src/lean/Init/Data/Fin/Log2.lean
 %%DATADIR%%/src/lean/Init/Data/Float.lean
 %%DATADIR%%/src/lean/Init/Data/FloatArray.lean
@@ -1539,18 +1735,31 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Hashable.lean
 %%DATADIR%%/src/lean/Init/Data/Int.lean
 %%DATADIR%%/src/lean/Init/Data/Int/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/Int/Bitwise.lean
+%%DATADIR%%/src/lean/Init/Data/Int/DivMod.lean
+%%DATADIR%%/src/lean/Init/Data/Int/DivModLemmas.lean
+%%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/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/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/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/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Linear.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Log2.lean
+%%DATADIR%%/src/lean/Init/Data/Nat/MinMax.lean
+%%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/OfScientific.lean
@@ -1558,6 +1767,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/Option/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/Option/BasicAux.lean
 %%DATADIR%%/src/lean/Init/Data/Option/Instances.lean
+%%DATADIR%%/src/lean/Init/Data/Option/Lemmas.lean
 %%DATADIR%%/src/lean/Init/Data/Ord.lean
 %%DATADIR%%/src/lean/Init/Data/Prod.lean
 %%DATADIR%%/src/lean/Init/Data/Queue.lean
@@ -1568,6 +1778,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/String.lean
 %%DATADIR%%/src/lean/Init/Data/String/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/String/Extra.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
@@ -1575,12 +1786,23 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/Data/UInt/Basic.lean
 %%DATADIR%%/src/lean/Init/Data/UInt/Log2.lean
 %%DATADIR%%/src/lean/Init/Dynamic.lean
+%%DATADIR%%/src/lean/Init/Ext.lean
+%%DATADIR%%/src/lean/Init/Guard.lean
 %%DATADIR%%/src/lean/Init/Hints.lean
 %%DATADIR%%/src/lean/Init/Meta.lean
 %%DATADIR%%/src/lean/Init/MetaTypes.lean
 %%DATADIR%%/src/lean/Init/Notation.lean
 %%DATADIR%%/src/lean/Init/NotationExtra.lean
+%%DATADIR%%/src/lean/Init/Omega.lean
+%%DATADIR%%/src/lean/Init/Omega/Coeffs.lean
+%%DATADIR%%/src/lean/Init/Omega/Constraint.lean
+%%DATADIR%%/src/lean/Init/Omega/Int.lean
+%%DATADIR%%/src/lean/Init/Omega/IntList.lean
+%%DATADIR%%/src/lean/Init/Omega/LinearCombo.lean
+%%DATADIR%%/src/lean/Init/Omega/Logic.lean
 %%DATADIR%%/src/lean/Init/Prelude.lean
+%%DATADIR%%/src/lean/Init/PropLemmas.lean
+%%DATADIR%%/src/lean/Init/RCases.lean
 %%DATADIR%%/src/lean/Init/ShareCommon.lean
 %%DATADIR%%/src/lean/Init/SimpLemmas.lean
 %%DATADIR%%/src/lean/Init/Simproc.lean
@@ -1596,6 +1818,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Init/System/ST.lean
 %%DATADIR%%/src/lean/Init/System/Uri.lean
 %%DATADIR%%/src/lean/Init/Tactics.lean
+%%DATADIR%%/src/lean/Init/TacticsExtra.lean
 %%DATADIR%%/src/lean/Init/Util.lean
 %%DATADIR%%/src/lean/Init/WF.lean
 %%DATADIR%%/src/lean/Init/WFTactics.lean
@@ -1720,6 +1943,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Data/HashSet.lean
 %%DATADIR%%/src/lean/Lean/Data/Json.lean
 %%DATADIR%%/src/lean/Lean/Data/Json/Basic.lean
+%%DATADIR%%/src/lean/Lean/Data/Json/Elab.lean
 %%DATADIR%%/src/lean/Lean/Data/Json/FromToJson.lean
 %%DATADIR%%/src/lean/Lean/Data/Json/Parser.lean
 %%DATADIR%%/src/lean/Lean/Data/Json/Printer.lean
@@ -1772,12 +1996,14 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Attributes.lean
 %%DATADIR%%/src/lean/Lean/Elab/AutoBound.lean
 %%DATADIR%%/src/lean/Lean/Elab/AuxDef.lean
+%%DATADIR%%/src/lean/Lean/Elab/BinderPredicates.lean
 %%DATADIR%%/src/lean/Lean/Elab/Binders.lean
 %%DATADIR%%/src/lean/Lean/Elab/BindersUtil.lean
 %%DATADIR%%/src/lean/Lean/Elab/BuiltinCommand.lean
 %%DATADIR%%/src/lean/Lean/Elab/BuiltinNotation.lean
 %%DATADIR%%/src/lean/Lean/Elab/BuiltinTerm.lean
 %%DATADIR%%/src/lean/Lean/Elab/Calc.lean
+%%DATADIR%%/src/lean/Lean/Elab/CheckTactic.lean
 %%DATADIR%%/src/lean/Lean/Elab/Command.lean
 %%DATADIR%%/src/lean/Lean/Elab/ComputedFields.lean
 %%DATADIR%%/src/lean/Lean/Elab/Config.lean
@@ -1806,6 +2032,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Extra.lean
 %%DATADIR%%/src/lean/Lean/Elab/Frontend.lean
 %%DATADIR%%/src/lean/Lean/Elab/GenInjective.lean
+%%DATADIR%%/src/lean/Lean/Elab/GuardMsgs.lean
 %%DATADIR%%/src/lean/Lean/Elab/Import.lean
 %%DATADIR%%/src/lean/Lean/Elab/Inductive.lean
 %%DATADIR%%/src/lean/Lean/Elab/InfoTree.lean
@@ -1819,6 +2046,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/MacroRules.lean
 %%DATADIR%%/src/lean/Lean/Elab/Match.lean
 %%DATADIR%%/src/lean/Lean/Elab/MatchAltView.lean
+%%DATADIR%%/src/lean/Lean/Elab/MatchExpr.lean
 %%DATADIR%%/src/lean/Lean/Elab/Mixfix.lean
 %%DATADIR%%/src/lean/Lean/Elab/MutualDef.lean
 %%DATADIR%%/src/lean/Lean/Elab/Notation.lean
@@ -1865,6 +2093,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/BuiltinTactic.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Cache.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Calc.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Change.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Config.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Congr.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv.lean
@@ -1878,16 +2107,33 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Unfold.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Delta.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/ElabTerm.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Ext.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/FalseOrByContra.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Generalize.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Guard.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Induction.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Injection.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/LibrarySearch.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Location.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Match.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Meta.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/NormCast.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega/Core.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega/Frontend.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega/MinNatAbs.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Omega/OmegaM.lean
+%%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/ShowTerm.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Simp.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/SimpTrace.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Simpa.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Simproc.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/SolveByElim.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Split.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Symm.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Unfold.lean
 %%DATADIR%%/src/lean/Lean/Elab/Term.lean
 %%DATADIR%%/src/lean/Lean/Elab/Util.lean
@@ -1900,6 +2146,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/ImportingFlag.lean
 %%DATADIR%%/src/lean/Lean/InternalExceptionId.lean
 %%DATADIR%%/src/lean/Lean/KeyedDeclsAttribute.lean
+%%DATADIR%%/src/lean/Lean/LabelAttribute.lean
 %%DATADIR%%/src/lean/Lean/LazyInitExtension.lean
 %%DATADIR%%/src/lean/Lean/Level.lean
 %%DATADIR%%/src/lean/Lean/Linter.lean
@@ -1919,14 +2166,16 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/AbstractNestedProofs.lean
 %%DATADIR%%/src/lean/Lean/Meta/AppBuilder.lean
 %%DATADIR%%/src/lean/Lean/Meta/Basic.lean
-%%DATADIR%%/src/lean/Lean/Meta/CasesOn.lean
 %%DATADIR%%/src/lean/Lean/Meta/Check.lean
 %%DATADIR%%/src/lean/Lean/Meta/Closure.lean
 %%DATADIR%%/src/lean/Lean/Meta/Coe.lean
+%%DATADIR%%/src/lean/Lean/Meta/CoeAttr.lean
 %%DATADIR%%/src/lean/Lean/Meta/CollectFVars.lean
 %%DATADIR%%/src/lean/Lean/Meta/CollectMVars.lean
+%%DATADIR%%/src/lean/Lean/Meta/CompletionName.lean
 %%DATADIR%%/src/lean/Lean/Meta/CongrTheorems.lean
 %%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/DiscrTree.lean
 %%DATADIR%%/src/lean/Lean/Meta/DiscrTreeTypes.lean
@@ -1946,9 +2195,12 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/InferType.lean
 %%DATADIR%%/src/lean/Lean/Meta/Injective.lean
 %%DATADIR%%/src/lean/Lean/Meta/Instances.lean
+%%DATADIR%%/src/lean/Lean/Meta/Iterator.lean
 %%DATADIR%%/src/lean/Lean/Meta/KAbstract.lean
 %%DATADIR%%/src/lean/Lean/Meta/KExprMap.lean
+%%DATADIR%%/src/lean/Lean/Meta/LazyDiscrTree.lean
 %%DATADIR%%/src/lean/Lean/Meta/LevelDefEq.lean
+%%DATADIR%%/src/lean/Lean/Meta/LitValues.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match/Basic.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match/CaseArraySizes.lean
@@ -1958,6 +2210,9 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Match/MatchEqs.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match/MatchEqsExt.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match/MatchPatternAttr.lean
+%%DATADIR%%/src/lean/Lean/Meta/Match/MatcherApp.lean
+%%DATADIR%%/src/lean/Lean/Meta/Match/MatcherApp/Basic.lean
+%%DATADIR%%/src/lean/Lean/Meta/Match/MatcherApp/Transform.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match/MatcherInfo.lean
 %%DATADIR%%/src/lean/Lean/Meta/Match/Value.lean
 %%DATADIR%%/src/lean/Lean/Meta/MatchUtil.lean
@@ -1977,6 +2232,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Assert.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Assumption.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/AuxLemma.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Backtrack.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Cases.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Cleanup.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Clear.lean
@@ -1987,9 +2243,11 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/ElimInfo.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/FVarSubst.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
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Injection.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Intro.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/LibrarySearch.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Basic.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Main.lean
@@ -1999,18 +2257,25 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Nat/Solver.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Simp.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/LinearArith/Solver.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/NormCast.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Refl.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Rename.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Repeat.lean
 %%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/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/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/Nat.lean
+%%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/Main.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/RegisterCommand.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -2019,9 +2284,12 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/SimpTheorems.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Simproc.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Simp/Types.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/SolveByElim.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Split.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/SplitIf.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Subst.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Symm.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/TryThis.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Unfold.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/UnifyEq.lean
 %%DATADIR%%/src/lean/Lean/Meta/Tactic/Util.lean
@@ -2067,7 +2335,11 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Server.lean
 %%DATADIR%%/src/lean/Lean/Server/AsyncList.lean
 %%DATADIR%%/src/lean/Lean/Server/CodeActions.lean
+%%DATADIR%%/src/lean/Lean/Server/CodeActions/Attr.lean
+%%DATADIR%%/src/lean/Lean/Server/CodeActions/Basic.lean
+%%DATADIR%%/src/lean/Lean/Server/CodeActions/Provider.lean
 %%DATADIR%%/src/lean/Lean/Server/Completion.lean
+%%DATADIR%%/src/lean/Lean/Server/CompletionItemData.lean
 %%DATADIR%%/src/lean/Lean/Server/FileSource.lean
 %%DATADIR%%/src/lean/Lean/Server/FileWorker.lean
 %%DATADIR%%/src/lean/Lean/Server/FileWorker/RequestHandling.lean
@@ -2103,6 +2375,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Util/ForEachExpr.lean
 %%DATADIR%%/src/lean/Lean/Util/ForEachExprWhere.lean
 %%DATADIR%%/src/lean/Lean/Util/HasConstCache.lean
+%%DATADIR%%/src/lean/Lean/Util/Heartbeats.lean
 %%DATADIR%%/src/lean/Lean/Util/InstantiateLevelParams.lean
 %%DATADIR%%/src/lean/Lean/Util/LakePath.lean
 %%DATADIR%%/src/lean/Lean/Util/LeanOptions.lean
@@ -2164,6 +2437,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/CLI/Serve.lean
 %%DATADIR%%/src/lean/lake/Lake/Config.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/Context.lean
+%%DATADIR%%/src/lean/lake/Lake/Config/Defaults.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/Dependency.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/Env.lean
 %%DATADIR%%/src/lean/lake/Lake/Config/ExternLib.lean