git: 2c62b3dc7a70 - main - math/lean4: update 4.8.0 → 4.9.0
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Sat, 06 Jul 2024 21:06:16 UTC
The branch main has been updated by yuri:
URL: https://cgit.FreeBSD.org/ports/commit/?id=2c62b3dc7a702d763d2c12553777bd93002cccb0
commit 2c62b3dc7a702d763d2c12553777bd93002cccb0
Author: Wen Heping <wen@FreeBSD.org>
AuthorDate: 2024-07-06 20:48:28 +0000
Commit: Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2024-07-06 21:06:13 +0000
math/lean4: update 4.8.0 → 4.9.0
PR: 280156
---
math/lean4/Makefile | 2 +-
math/lean4/distinfo | 6 ++--
math/lean4/pkg-plist | 91 +++++++++++++++++++++++++++++++++++++++++++++++-----
3 files changed, 87 insertions(+), 12 deletions(-)
diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index c6a1086693fe..078d42595304 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
PORTNAME= lean4
DISTVERSIONPREFIX= v
-DISTVERSION= 4.8.0
+DISTVERSION= 4.9.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 d12208f173cc..2fcae32c6584 100644
--- a/math/lean4/distinfo
+++ b/math/lean4/distinfo
@@ -1,3 +1,3 @@
-TIMESTAMP = 1717688258
-SHA256 (leanprover-lean4-v4.8.0_GH0.tar.gz) = 3bb46c24b4f5ad1fee38163bf466d8f60a334bb64a19c9801a42f76162580f9c
-SIZE (leanprover-lean4-v4.8.0_GH0.tar.gz) = 20345135
+TIMESTAMP = 1720249428
+SHA256 (leanprover-lean4-v4.9.0_GH0.tar.gz) = f59b7a782bd7e918b35a133a954094f0e39e344ffef06689a1c53ae97ae8d769
+SIZE (leanprover-lean4-v4.9.0_GH0.tar.gz) = 22768229
diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist
index 75fc4ce6be58..fee7268e93e1 100644
--- a/math/lean4/pkg-plist
+++ b/math/lean4/pkg-plist
@@ -100,6 +100,8 @@ lib/lean/Init/Data/Char.ilean
lib/lean/Init/Data/Char.olean
lib/lean/Init/Data/Char/Basic.ilean
lib/lean/Init/Data/Char/Basic.olean
+lib/lean/Init/Data/Char/Lemmas.ilean
+lib/lean/Init/Data/Char/Lemmas.olean
lib/lean/Init/Data/Fin.ilean
lib/lean/Init/Data/Fin.olean
lib/lean/Init/Data/Fin/Basic.ilean
@@ -134,6 +136,8 @@ 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/DivMod.ilean
@@ -144,6 +148,8 @@ 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
@@ -230,6 +236,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/String/Lemmas.ilean
+lib/lean/Init/Data/String/Lemmas.olean
lib/lean/Init/Data/Sum.ilean
lib/lean/Init/Data/Sum.olean
lib/lean/Init/Data/ToString.ilean
@@ -244,12 +252,24 @@ 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/Dynamic.ilean
lib/lean/Init/Dynamic.olean
lib/lean/Init/Ext.ilean
lib/lean/Init/Ext.olean
lib/lean/Init/GetElem.ilean
lib/lean/Init/GetElem.olean
+lib/lean/Init/Grind.ilean
+lib/lean/Init/Grind.olean
+lib/lean/Init/Grind/Cases.ilean
+lib/lean/Init/Grind/Cases.olean
+lib/lean/Init/Grind/Lemmas.ilean
+lib/lean/Init/Grind/Lemmas.olean
+lib/lean/Init/Grind/Norm.ilean
+lib/lean/Init/Grind/Norm.olean
+lib/lean/Init/Grind/Tactics.ilean
+lib/lean/Init/Grind/Tactics.olean
lib/lean/Init/Guard.ilean
lib/lean/Init/Guard.olean
lib/lean/Init/Hints.ilean
@@ -440,6 +460,8 @@ lib/lean/Lake/DSL.ilean
lib/lean/Lake/DSL.olean
lib/lean/Lake/DSL/Attributes.ilean
lib/lean/Lake/DSL/Attributes.olean
+lib/lean/Lake/DSL/AttributesCore.ilean
+lib/lean/Lake/DSL/AttributesCore.olean
lib/lean/Lake/DSL/Config.ilean
lib/lean/Lake/DSL/Config.olean
lib/lean/Lake/DSL/DeclUtil.ilean
@@ -528,6 +550,8 @@ lib/lean/Lake/Util/Git.ilean
lib/lean/Lake/Util/Git.olean
lib/lean/Lake/Util/IO.ilean
lib/lean/Lake/Util/IO.olean
+lib/lean/Lake/Util/JsonObject.ilean
+lib/lean/Lake/Util/JsonObject.olean
lib/lean/Lake/Util/Lift.ilean
lib/lean/Lake/Util/Lift.olean
lib/lean/Lake/Util/List.ilean
@@ -544,8 +568,6 @@ lib/lean/Lake/Util/Name.ilean
lib/lean/Lake/Util/Name.olean
lib/lean/Lake/Util/NativeLib.ilean
lib/lean/Lake/Util/NativeLib.olean
-lib/lean/Lake/Util/Newline.ilean
-lib/lean/Lake/Util/Newline.olean
lib/lean/Lake/Util/Opaque.ilean
lib/lean/Lake/Util/Opaque.olean
lib/lean/Lake/Util/OrdHashSet.ilean
@@ -564,10 +586,14 @@ lib/lean/Lake/Util/Sugar.ilean
lib/lean/Lake/Util/Sugar.olean
lib/lean/Lake/Util/Task.ilean
lib/lean/Lake/Util/Task.olean
+lib/lean/Lake/Util/Version.ilean
+lib/lean/Lake/Util/Version.olean
lib/lean/Lake/Version.ilean
lib/lean/Lake/Version.olean
lib/lean/Lean.ilean
lib/lean/Lean.olean
+lib/lean/Lean/AddDecl.ilean
+lib/lean/Lean/AddDecl.olean
lib/lean/Lean/Attributes.ilean
lib/lean/Lean/Attributes.olean
lib/lean/Lean/AuxRecursor.ilean
@@ -1436,6 +1462,24 @@ lib/lean/Lean/Meta/Tactic/FunInd.ilean
lib/lean/Lean/Meta/Tactic/FunInd.olean
lib/lean/Lean/Meta/Tactic/Generalize.ilean
lib/lean/Lean/Meta/Tactic/Generalize.olean
+lib/lean/Lean/Meta/Tactic/Grind.ilean
+lib/lean/Lean/Meta/Tactic/Grind.olean
+lib/lean/Lean/Meta/Tactic/Grind/Attr.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Attr.olean
+lib/lean/Lean/Meta/Tactic/Grind/Cases.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Cases.olean
+lib/lean/Lean/Meta/Tactic/Grind/Core.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Core.olean
+lib/lean/Lean/Meta/Tactic/Grind/Injection.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Injection.olean
+lib/lean/Lean/Meta/Tactic/Grind/Preprocessor.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Preprocessor.olean
+lib/lean/Lean/Meta/Tactic/Grind/RevertAll.ilean
+lib/lean/Lean/Meta/Tactic/Grind/RevertAll.olean
+lib/lean/Lean/Meta/Tactic/Grind/Types.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Types.olean
+lib/lean/Lean/Meta/Tactic/Grind/Util.ilean
+lib/lean/Lean/Meta/Tactic/Grind/Util.olean
lib/lean/Lean/Meta/Tactic/IndependentOf.ilean
lib/lean/Lean/Meta/Tactic/IndependentOf.olean
lib/lean/Lean/Meta/Tactic/Induction.ilean
@@ -1829,6 +1873,7 @@ share/lean/lean.mk
%%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/Char/Lemmas.lean
%%DATADIR%%/src/lean/Init/Data/Fin.lean
%%DATADIR%%/src/lean/Init/Data/Fin/Basic.lean
%%DATADIR%%/src/lean/Init/Data/Fin/Fold.lean
@@ -1847,6 +1892,7 @@ share/lean/lean.mk
%%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/Bitwise/Lemmas.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
@@ -1859,6 +1905,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/TakeDrop.lean
%%DATADIR%%/src/lean/Init/Data/Nat.lean
%%DATADIR%%/src/lean/Init/Data/Nat/Basic.lean
%%DATADIR%%/src/lean/Init/Data/Nat/Bitwise.lean
@@ -1894,16 +1941,23 @@ 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/String/Lemmas.lean
%%DATADIR%%/src/lean/Init/Data/Sum.lean
%%DATADIR%%/src/lean/Init/Data/ToString.lean
%%DATADIR%%/src/lean/Init/Data/ToString/Basic.lean
%%DATADIR%%/src/lean/Init/Data/ToString/Macro.lean
%%DATADIR%%/src/lean/Init/Data/UInt.lean
%%DATADIR%%/src/lean/Init/Data/UInt/Basic.lean
+%%DATADIR%%/src/lean/Init/Data/UInt/Lemmas.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/GetElem.lean
+%%DATADIR%%/src/lean/Init/Grind.lean
+%%DATADIR%%/src/lean/Init/Grind/Cases.lean
+%%DATADIR%%/src/lean/Init/Grind/Lemmas.lean
+%%DATADIR%%/src/lean/Init/Grind/Norm.lean
+%%DATADIR%%/src/lean/Init/Grind/Tactics.lean
%%DATADIR%%/src/lean/Init/Guard.lean
%%DATADIR%%/src/lean/Init/Hints.lean
%%DATADIR%%/src/lean/Init/MacroTrace.lean
@@ -1941,6 +1995,7 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/Init/WF.lean
%%DATADIR%%/src/lean/Init/WFTactics.lean
%%DATADIR%%/src/lean/Lean.lean
+%%DATADIR%%/src/lean/Lean/AddDecl.lean
%%DATADIR%%/src/lean/Lean/Attributes.lean
%%DATADIR%%/src/lean/Lean/AuxRecursor.lean
%%DATADIR%%/src/lean/Lean/BuiltinDocAttr.lean
@@ -2375,6 +2430,15 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/Lean/Meta/Tactic/FVarSubst.lean
%%DATADIR%%/src/lean/Lean/Meta/Tactic/FunInd.lean
%%DATADIR%%/src/lean/Lean/Meta/Tactic/Generalize.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Attr.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Cases.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Core.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Injection.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Preprocessor.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/RevertAll.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Types.lean
+%%DATADIR%%/src/lean/Lean/Meta/Tactic/Grind/Util.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
@@ -2605,6 +2669,7 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/lake/Lake/Config/WorkspaceConfig.lean
%%DATADIR%%/src/lean/lake/Lake/DSL.lean
%%DATADIR%%/src/lean/lake/Lake/DSL/Attributes.lean
+%%DATADIR%%/src/lean/lake/Lake/DSL/AttributesCore.lean
%%DATADIR%%/src/lean/lake/Lake/DSL/Config.lean
%%DATADIR%%/src/lean/lake/Lake/DSL/DeclUtil.lean
%%DATADIR%%/src/lean/lake/Lake/DSL/Extensions.lean
@@ -2649,6 +2714,7 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/lake/Lake/Util/FilePath.lean
%%DATADIR%%/src/lean/lake/Lake/Util/Git.lean
%%DATADIR%%/src/lean/lake/Lake/Util/IO.lean
+%%DATADIR%%/src/lean/lake/Lake/Util/JsonObject.lean
%%DATADIR%%/src/lean/lake/Lake/Util/Lift.lean
%%DATADIR%%/src/lean/lake/Lake/Util/List.lean
%%DATADIR%%/src/lean/lake/Lake/Util/Lock.lean
@@ -2657,7 +2723,6 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/lake/Lake/Util/Message.lean
%%DATADIR%%/src/lean/lake/Lake/Util/Name.lean
%%DATADIR%%/src/lean/lake/Lake/Util/NativeLib.lean
-%%DATADIR%%/src/lean/lake/Lake/Util/Newline.lean
%%DATADIR%%/src/lean/lake/Lake/Util/Opaque.lean
%%DATADIR%%/src/lean/lake/Lake/Util/OrdHashSet.lean
%%DATADIR%%/src/lean/lake/Lake/Util/OrderedTagAttribute.lean
@@ -2667,6 +2732,7 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/lake/Lake/Util/StoreInsts.lean
%%DATADIR%%/src/lean/lake/Lake/Util/Sugar.lean
%%DATADIR%%/src/lean/lake/Lake/Util/Task.lean
+%%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
@@ -2681,6 +2747,19 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/lake/tests/buildArgs/lakefile.lean
%%DATADIR%%/src/lean/lake/tests/clone/test/Main.lean
%%DATADIR%%/src/lean/lake/tests/clone/test/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/driver/Test.lean
+%%DATADIR%%/src/lean/lake/tests/driver/dep-invalid.lean
+%%DATADIR%%/src/lean/lake/tests/driver/dep-unknown.lean
+%%DATADIR%%/src/lean/lake/tests/driver/dep.lean
+%%DATADIR%%/src/lean/lake/tests/driver/dep/lakefile.lean
+%%DATADIR%%/src/lean/lake/tests/driver/driver.lean
+%%DATADIR%%/src/lean/lake/tests/driver/exe.lean
+%%DATADIR%%/src/lean/lake/tests/driver/lib.lean
+%%DATADIR%%/src/lean/lake/tests/driver/none.lean
+%%DATADIR%%/src/lean/lake/tests/driver/runner.lean
+%%DATADIR%%/src/lean/lake/tests/driver/script.lean
+%%DATADIR%%/src/lean/lake/tests/driver/two.lean
+%%DATADIR%%/src/lean/lake/tests/driver/unknown.lean
%%DATADIR%%/src/lean/lake/tests/globs/TBA.lean
%%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian.lean
%%DATADIR%%/src/lean/lake/tests/globs/TBA/Eulerian/A.lean
@@ -2731,13 +2810,9 @@ share/lean/lean.mk
%%DATADIR%%/src/lean/lake/tests/reversion/Hello.lean
%%DATADIR%%/src/lean/lake/tests/reversion/Main.lean
%%DATADIR%%/src/lean/lake/tests/reversion/lakefile.lean
-%%DATADIR%%/src/lean/lake/tests/test/exe.lean
-%%DATADIR%%/src/lean/lake/tests/test/none.lean
-%%DATADIR%%/src/lean/lake/tests/test/script.lean
-%%DATADIR%%/src/lean/lake/tests/test/test.lean
-%%DATADIR%%/src/lean/lake/tests/test/two.lean
%%DATADIR%%/src/lean/lake/tests/toml/README.md
%%DATADIR%%/src/lean/lake/tests/toml/Test.lean
+%%DATADIR%%/src/lean/lake/tests/trace/Foo.lean
%%DATADIR%%/src/lean/lake/tests/translateConfig/out.expected.lean
%%DATADIR%%/src/lean/lake/tests/translateConfig/source.lean
%%DATADIR%%/src/lean/lake/tests/wfail/Warn.lean