math/lean4: update 4.9.1 → 4.10.0

3 files changed, 62 insertions, 19 deletions

diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 6eb36f82225d..562dad632944 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
 PORTNAME=	lean4
 DISTVERSIONPREFIX=	v
-DISTVERSION=	4.9.1
+DISTVERSION=	4.10.0
 CATEGORIES=	math lang devel # lean4 is primarily a math theorem prover, but it is also a language and a development environment
 
 MAINTAINER=	yuri@FreeBSD.org
diff --git a/math/lean4/distinfo b/math/lean4/distinfo
index 395168f7c42c..1ca0f069d7a4 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1720597727
-SHA256 (leanprover-lean4-v4.9.1_GH0.tar.gz) = 713e41ec71a9e9030e6f46cc5dbb5aef30ac1887dfe5faa5a054c0a2f0613b1e
-SIZE (leanprover-lean4-v4.9.1_GH0.tar.gz) = 22771989
+TIMESTAMP = 1722411891
+SHA256 (leanprover-lean4-v4.10.0_GH0.tar.gz) = dee5d1dbcea924fa3f4500c1f4854ea5953f471e3600dac71421c742c844b094
+SIZE (leanprover-lean4-v4.10.0_GH0.tar.gz) = 25013155
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index fee7268e93e1..65859221ae90 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -136,10 +136,10 @@ 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/Lemmas.ilean
-lib/lean/Init/Data/Int/Bitwise/Lemmas.olean
 lib/lean/Init/Data/Int/Bitwise.ilean
 lib/lean/Init/Data/Int/Bitwise.olean
+lib/lean/Init/Data/Int/Bitwise/Lemmas.ilean
+lib/lean/Init/Data/Int/Bitwise/Lemmas.olean
 lib/lean/Init/Data/Int/DivMod.ilean
 lib/lean/Init/Data/Int/DivMod.olean
 lib/lean/Init/Data/Int/DivModLemmas.ilean
@@ -148,8 +148,6 @@ 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/List/TakeDrop.ilean
-lib/lean/Init/Data/List/TakeDrop.olean
 lib/lean/Init/Data/Int/Order.ilean
 lib/lean/Init/Data/Int/Order.olean
 lib/lean/Init/Data/Int/Pow.ilean
@@ -166,6 +164,10 @@ lib/lean/Init/Data/List/Impl.ilean
 lib/lean/Init/Data/List/Impl.olean
 lib/lean/Init/Data/List/Lemmas.ilean
 lib/lean/Init/Data/List/Lemmas.olean
+lib/lean/Init/Data/List/Notation.ilean
+lib/lean/Init/Data/List/Notation.olean
+lib/lean/Init/Data/List/TakeDrop.ilean
+lib/lean/Init/Data/List/TakeDrop.olean
 lib/lean/Init/Data/Nat.ilean
 lib/lean/Init/Data/Nat.olean
 lib/lean/Init/Data/Nat/Basic.ilean
@@ -250,10 +252,10 @@ lib/lean/Init/Data/UInt.ilean
 lib/lean/Init/Data/UInt.olean
 lib/lean/Init/Data/UInt/Basic.ilean
 lib/lean/Init/Data/UInt/Basic.olean
-lib/lean/Init/Data/UInt/Log2.ilean
-lib/lean/Init/Data/UInt/Log2.olean
 lib/lean/Init/Data/UInt/Lemmas.ilean
 lib/lean/Init/Data/UInt/Lemmas.olean
+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
@@ -482,20 +484,28 @@ lib/lean/Lake/Load.ilean
 lib/lean/Lake/Load.olean
 lib/lean/Lake/Load/Config.ilean
 lib/lean/Lake/Load/Config.olean
-lib/lean/Lake/Load/Elab.ilean
-lib/lean/Lake/Load/Elab.olean
-lib/lean/Lake/Load/Main.ilean
-lib/lean/Lake/Load/Main.olean
+lib/lean/Lake/Load/Lean.ilean
+lib/lean/Lake/Load/Lean.olean
+lib/lean/Lake/Load/Lean/Elab.ilean
+lib/lean/Lake/Load/Lean/Elab.olean
+lib/lean/Lake/Load/Lean/Eval.ilean
+lib/lean/Lake/Load/Lean/Eval.olean
 lib/lean/Lake/Load/Manifest.ilean
 lib/lean/Lake/Load/Manifest.olean
 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/Resolve.ilean
+lib/lean/Lake/Load/Resolve.olean
 lib/lean/Lake/Load/Toml.ilean
 lib/lean/Lake/Load/Toml.olean
+lib/lean/Lake/Load/Workspace.ilean
+lib/lean/Lake/Load/Workspace.olean
 lib/lean/Lake/Main.ilean
 lib/lean/Lake/Main.olean
+lib/lean/Lake/Reservoir.ilean
+lib/lean/Lake/Reservoir.olean
 lib/lean/Lake/Toml.ilean
 lib/lean/Lake/Toml.olean
 lib/lean/Lake/Toml/Data.ilean
@@ -932,6 +942,8 @@ lib/lean/Lean/DeclarationRange.ilean
 lib/lean/Lean/DeclarationRange.olean
 lib/lean/Lean/DocString.ilean
 lib/lean/Lean/DocString.olean
+lib/lean/Lean/DocString/Extension.ilean
+lib/lean/Lean/DocString/Extension.olean
 lib/lean/Lean/Elab.ilean
 lib/lean/Lean/Elab.olean
 lib/lean/Lean/Elab/App.ilean
@@ -1166,6 +1178,8 @@ lib/lean/Lean/Elab/Tactic/Conv/Unfold.ilean
 lib/lean/Lean/Elab/Tactic/Conv/Unfold.olean
 lib/lean/Lean/Elab/Tactic/Delta.ilean
 lib/lean/Lean/Elab/Tactic/Delta.olean
+lib/lean/Lean/Elab/Tactic/Doc.ilean
+lib/lean/Lean/Elab/Tactic/Doc.olean
 lib/lean/Lean/Elab/Tactic/ElabTerm.ilean
 lib/lean/Lean/Elab/Tactic/ElabTerm.olean
 lib/lean/Lean/Elab/Tactic/Ext.ilean
@@ -1266,6 +1280,8 @@ lib/lean/Lean/Linter/Basic.ilean
 lib/lean/Lean/Linter/Basic.olean
 lib/lean/Lean/Linter/Builtin.ilean
 lib/lean/Lean/Linter/Builtin.olean
+lib/lean/Lean/Linter/ConstructorAsVariable.ilean
+lib/lean/Lean/Linter/ConstructorAsVariable.olean
 lib/lean/Lean/Linter/Deprecated.ilean
 lib/lean/Lean/Linter/Deprecated.olean
 lib/lean/Lean/Linter/MissingDocs.ilean
@@ -1320,6 +1336,10 @@ 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/Constructions/BRecOn.ilean
+lib/lean/Lean/Meta/Constructions/BRecOn.olean
+lib/lean/Lean/Meta/Constructions/RecOn.ilean
+lib/lean/Lean/Meta/Constructions/RecOn.olean
 lib/lean/Lean/Meta/CtorRecognizer.ilean
 lib/lean/Lean/Meta/CtorRecognizer.olean
 lib/lean/Lean/Meta/DecLevel.ilean
@@ -1624,6 +1644,8 @@ lib/lean/Lean/Parser/Syntax.ilean
 lib/lean/Lean/Parser/Syntax.olean
 lib/lean/Lean/Parser/Tactic.ilean
 lib/lean/Lean/Parser/Tactic.olean
+lib/lean/Lean/Parser/Tactic/Doc.ilean
+lib/lean/Lean/Parser/Tactic/Doc.olean
 lib/lean/Lean/Parser/Term.ilean
 lib/lean/Lean/Parser/Term.olean
 lib/lean/Lean/Parser/Types.ilean
@@ -1818,10 +1840,13 @@ lib/lean/Lean/Widget/Types.ilean
 lib/lean/Lean/Widget/Types.olean
 lib/lean/Lean/Widget/UserWidget.ilean
 lib/lean/Lean/Widget/UserWidget.olean
+lib/lean/Std.ilean
+lib/lean/Std.olean
 lib/lean/libInit.a
 lib/lean/libInit_shared.so
 lib/lean/libLake.a
 lib/lean/libLean.a
+lib/lean/libStd.a
 lib/lean/libleancpp.a
 lib/lean/libleanrt.a
 lib/lean/libleanshared.so
@@ -1905,6 +1930,7 @@ share/lean/lean.mk
 %%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/List/Notation.lean
 %%DATADIR%%/src/lean/Init/Data/List/TakeDrop.lean
 %%DATADIR%%/src/lean/Init/Data/Nat.lean
 %%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean
@@ -2165,6 +2191,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Declaration.lean
 %%DATADIR%%/src/lean/Lean/DeclarationRange.lean
 %%DATADIR%%/src/lean/Lean/DocString.lean
+%%DATADIR%%/src/lean/Lean/DocString/Extension.lean
 %%DATADIR%%/src/lean/Lean/Elab.lean
 %%DATADIR%%/src/lean/Lean/Elab/App.lean
 %%DATADIR%%/src/lean/Lean/Elab/Arg.lean
@@ -2282,6 +2309,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Simp.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Conv/Unfold.lean
 %%DATADIR%%/src/lean/Lean/Elab/Tactic/Delta.lean
+%%DATADIR%%/src/lean/Lean/Elab/Tactic/Doc.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
@@ -2332,6 +2360,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Linter.lean
 %%DATADIR%%/src/lean/Lean/Linter/Basic.lean
 %%DATADIR%%/src/lean/Lean/Linter/Builtin.lean
+%%DATADIR%%/src/lean/Lean/Linter/ConstructorAsVariable.lean
 %%DATADIR%%/src/lean/Lean/Linter/Deprecated.lean
 %%DATADIR%%/src/lean/Lean/Linter/MissingDocs.lean
 %%DATADIR%%/src/lean/Lean/Linter/UnusedVariables.lean
@@ -2359,6 +2388,8 @@ share/lean/lean.mk
 %%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/Constructions/BRecOn.lean
+%%DATADIR%%/src/lean/Lean/Meta/Constructions/RecOn.lean
 %%DATADIR%%/src/lean/Lean/Meta/CtorRecognizer.lean
 %%DATADIR%%/src/lean/Lean/Meta/DecLevel.lean
 %%DATADIR%%/src/lean/Lean/Meta/Diagnostics.lean
@@ -2511,6 +2542,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Parser/StrInterpolation.lean
 %%DATADIR%%/src/lean/Lean/Parser/Syntax.lean
 %%DATADIR%%/src/lean/Lean/Parser/Tactic.lean
+%%DATADIR%%/src/lean/Lean/Parser/Tactic/Doc.lean
 %%DATADIR%%/src/lean/Lean/Parser/Term.lean
 %%DATADIR%%/src/lean/Lean/Parser/Types.lean
 %%DATADIR%%/src/lean/Lean/ParserCompiler.lean
@@ -2610,6 +2642,7 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/Lean/Widget/Types.lean
 %%DATADIR%%/src/lean/Lean/Widget/UserWidget.lean
 %%DATADIR%%/src/lean/Leanc.lean
+%%DATADIR%%/src/lean/Std.lean
 %%DATADIR%%/src/lean/lake/Lake.lean
 %%DATADIR%%/src/lean/lake/Lake/Build.lean
 %%DATADIR%%/src/lean/lake/Lake/Build/Actions.lean
@@ -2680,13 +2713,17 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/DSL/Targets.lean
 %%DATADIR%%/src/lean/lake/Lake/Load.lean
 %%DATADIR%%/src/lean/lake/Lake/Load/Config.lean
-%%DATADIR%%/src/lean/lake/Lake/Load/Elab.lean
-%%DATADIR%%/src/lean/lake/Lake/Load/Main.lean
+%%DATADIR%%/src/lean/lake/Lake/Load/Lean.lean
+%%DATADIR%%/src/lean/lake/Lake/Load/Lean/Elab.lean
+%%DATADIR%%/src/lean/lake/Lake/Load/Lean/Eval.lean
 %%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/Resolve.lean
 %%DATADIR%%/src/lean/lake/Lake/Load/Toml.lean
+%%DATADIR%%/src/lean/lake/Lake/Load/Workspace.lean
 %%DATADIR%%/src/lean/lake/Lake/Main.lean
+%%DATADIR%%/src/lean/lake/Lake/Reservoir.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
@@ -2735,11 +2772,13 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/Lake/Util/Version.lean
 %%DATADIR%%/src/lean/lake/Lake/Version.lean
 %%DATADIR%%/src/lean/lake/README.md
-%%DATADIR%%/src/lean/lake/lakefile.lean
-%%DATADIR%%/src/lean/lake/tests/badImport/Lib/A.lean
+%%DATADIR%%/src/lean/lake/tests/badImport/Etc.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/Lib/B1.lean
+%%DATADIR%%/src/lean/lake/tests/badImport/Lib/S.lean
+%%DATADIR%%/src/lean/lake/tests/badImport/Lib/U.lean
 %%DATADIR%%/src/lean/lake/tests/badImport/X.lean
+%%DATADIR%%/src/lean/lake/tests/badImport/X1.lean
 %%DATADIR%%/src/lean/lake/tests/badImport/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/buildArgs/Hello.lean
 %%DATADIR%%/src/lean/lake/tests/buildArgs/Main.lean
@@ -2788,6 +2827,7 @@ share/lean/lean.mk
 %%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/online/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
@@ -2799,6 +2839,8 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/order/foo/Y.lean
 %%DATADIR%%/src/lean/lake/tests/order/foo/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/order/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/order/leaf/Z.lean
+%%DATADIR%%/src/lean/lake/tests/order/leaf/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/postUpdate/dep/hello.lean
 %%DATADIR%%/src/lean/lake/tests/postUpdate/dep/lakefile.lean
 %%DATADIR%%/src/lean/lake/tests/postUpdate/lakefile.lean
@@ -2817,3 +2859,4 @@ share/lean/lean.mk
 %%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean
 %%DATADIR%%/src/lean/lake/tests/wfail/Warn.lean
 %%DATADIR%%/src/lean/lake/tests/wfail/lakefile.lean
+@dir lib/lean/Std