Date: Sat, 13 Apr 2024 22:31:16 GMT From: Yuri Victorovich <yuri@FreeBSD.org> To: ports-committers@FreeBSD.org, dev-commits-ports-all@FreeBSD.org, dev-commits-ports-main@FreeBSD.org Subject: git: d1bd2996d45a - main - math/lean4: update 4.6.0 =?utf-8?Q?=E2=86=92?= 4.7.0 Message-ID: <202404132231.43DMVG4Y054870@gitrepo.freebsd.org>
next in thread | raw e-mail | index | archive | help
The branch main has been updated by yuri: URL: https://cgit.FreeBSD.org/ports/commit/?id=d1bd2996d45a7bea0740770ab0d8c3f0c4690246 commit d1bd2996d45a7bea0740770ab0d8c3f0c4690246 Author: Yuri Victorovich <yuri@FreeBSD.org> AuthorDate: 2024-04-13 22:31:00 +0000 Commit: Yuri Victorovich <yuri@FreeBSD.org> CommitDate: 2024-04-13 22:31:12 +0000 math/lean4: update 4.6.0 → 4.7.0 Reported by: portscout --- math/lean4/Makefile | 3 +- math/lean4/distinfo | 6 +- math/lean4/files/patch-src_CMakeLists.txt | 20 +- math/lean4/files/patch-stage0_src_CMakeLists.txt | 20 +- math/lean4/pkg-plist | 280 ++++++++++++++++++++++- 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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?202404132231.43DMVG4Y054870>