freebsd/ports
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

math/lean4: update 4.20.0-rc5 → 4.20.0

Browse Source
This commit is contained in:
Yuri Victorovich 2025-06-03 23:30:19 -07:00
parent 5baf43483c
commit 3aa99a618c
3 changed files with 6 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
math/lean4/Makefile
View File

@ -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 <bsd.port.mk>

6
math/lean4/distinfo
View File

@ -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

1
math/lean4/pkg-plist
View File

@ -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