From 3aa99a618ce34866f09d45fbb42e0a2558cb264c Mon Sep 17 00:00:00 2001 From: Yuri Victorovich Date: Tue, 3 Jun 2025 23:30:19 -0700 Subject: [PATCH] =?UTF-8?q?math/lean4:=20update=204.20.0-rc5=20=E2=86=92?= =?UTF-8?q?=204.20.0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- math/lean4/Makefile | 6 ++---- math/lean4/distinfo | 6 +++--- math/lean4/pkg-plist | 1 + 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/math/lean4/Makefile b/math/lean4/Makefile index 56155b9be891..6c17ccfee08c 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,6 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.20.0-rc5 +DISTVERSION= 4.20.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 @@ -62,8 +62,6 @@ post-install: lib/lean/libInit_shared.so \ lib/lean/libleanshared.so -# 2 test failures: -# https://github.com/leanprover/lean4/issues/4396: The test leanlaketest_old times out -# https://github.com/leanprover/lean4/issues/4397: The test leanlaketest_serve fails: error: unexpected identifier; expected command +tests as of 4.20.0: 99% tests passed, 16 tests failed out of 2594, see https://github.com/leanprover/lean4/issues/8628 .include diff --git a/math/lean4/distinfo b/math/lean4/distinfo index 5aef4f3763ae..bcaf7eef4b66 100644 --- a/math/lean4/distinfo +++ b/math/lean4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1746632807 -SHA256 (leanprover-lean4-v4.20.0-rc5_GH0.tar.gz) = aaddadf237e16bdb2fd06987315f4af0791dfa965a924511087865d441b80ec6 -SIZE (leanprover-lean4-v4.20.0-rc5_GH0.tar.gz) = 40328367 +TIMESTAMP = 1748922676 +SHA256 (leanprover-lean4-v4.20.0_GH0.tar.gz) = a6b0c2e9865b0339d77060a59bc821cfd43af47debd93e214042386710d18054 +SIZE (leanprover-lean4-v4.20.0_GH0.tar.gz) = 40324553 diff --git a/math/lean4/pkg-plist b/math/lean4/pkg-plist index 5615db78b1ee..17ff0331ad17 100644 --- a/math/lean4/pkg-plist +++ b/math/lean4/pkg-plist @@ -5281,6 +5281,7 @@ share/lean/lean.mk %%DATADIR%%/src/lean/lake/tests/precompileLink/FooDep.lean %%DATADIR%%/src/lean/lake/tests/precompileLink/FooDepDep.lean %%DATADIR%%/src/lean/lake/tests/precompileLink/Indirect.lean +%%DATADIR%%/src/lean/lake/tests/precompileLink/LakeTest.lean %%DATADIR%%/src/lean/lake/tests/precompileLink/lakefile.lean %%DATADIR%%/src/lean/lake/tests/precompileLink/orderTest.lean %%DATADIR%%/src/lean/lake/tests/query/exe.lean