summaryrefslogtreecommitdiff
path: root/math/lean4/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'math/lean4/Makefile')
-rw-r--r--math/lean4/Makefile12
1 files changed, 7 insertions, 5 deletions
diff --git a/math/lean4/Makefile b/math/lean4/Makefile
index 56155b9be891..c6d417be8716 100644
--- a/math/lean4/Makefile
+++ b/math/lean4/Makefile
@@ -1,6 +1,6 @@
PORTNAME= lean4
DISTVERSIONPREFIX= v
-DISTVERSION= 4.20.0-rc5
+DISTVERSION= 4.23.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
@@ -11,6 +11,7 @@ WWW= https://lean-lang.org/ \
LICENSE= APACHE20
LICENSE_FILE= ${WRKSRC}/LICENSE
+BROKEN_FreeBSD_13= compilation fails: error: use of undeclared identifier 'clearenv'
BROKEN_armv7= compilation fails: ../../.build/stage1/lib/temp/Init/Coe.depend: No such file or directory
BROKEN_i386= linking fails: INTERNAL PANIC: out of memory (during: Linking runLinter)
@@ -60,10 +61,11 @@ post-install:
bin/lean \
bin/leanc \
lib/lean/libInit_shared.so \
- lib/lean/libleanshared.so
+ lib/lean/libleanshared.so \
+ lib/lean/libleanshared_1.so \
+ lib/lean/libLake_shared.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
+# tests as of 4.23.0: 99% tests passed, 10 tests failed out of 2870
.include <bsd.port.mk>