diff options
Diffstat (limited to 'math/lean4/Makefile')
| -rw-r--r-- | math/lean4/Makefile | 25 |
1 files changed, 20 insertions, 5 deletions
diff --git a/math/lean4/Makefile b/math/lean4/Makefile index acc607f13634..8b5c81aa12bc 100644 --- a/math/lean4/Makefile +++ b/math/lean4/Makefile @@ -1,7 +1,6 @@ PORTNAME= lean4 DISTVERSIONPREFIX= v -DISTVERSION= 4.20.1 -PORTREVISION= 1 +DISTVERSION= 4.25.2-20251201 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 @@ -12,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) @@ -25,6 +25,7 @@ USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # USE_GITHUB= yes GH_ACCOUNT= leanprover +GH_TAGNAME= 5e165e3 CFLAGS+= -fPIC CXXFLAGS+= -fPIC @@ -32,7 +33,6 @@ CXXFLAGS+= -fPIC CMAKE_OFF= USE_MIMALLOC #MAKE_ARGS+= V=1 VERBOSE=1 -#MAKE_JOBS_UNSAFE= yes MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean BINARY_ALIAS= make=${GMAKE} python=${PYTHON_CMD} @@ -48,6 +48,19 @@ pre-everything:: @${ECHO_MSG} " # mount /proc" @${ECHO_MSG} "" +post-patch: + # Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files + @${FIND} ${WRKSRC}/tests -name "lakefile.toml" | while read f; do \ + ${GREP} -q "weakLeancArgs" "$$f" || \ + ( ${PRINTF} 'weakLeancArgs = ["-fPIC"]\n\n' | cat - "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f" ); \ + done + # Add weakLeancArgs to lakefile.lean files that define packages + @${FIND} ${WRKSRC}/tests -name "lakefile.lean" | while read f; do \ + if ${GREP} -q "^package .* where" "$$f" && ! ${GREP} -q "weakLeancArgs" "$$f"; then \ + ${AWK} '/^package .* where$$/ {print; print " weakLeancArgs := #[\"-fPIC\"]"; next} 1' "$$f" > "$$f.tmp" && ${MV} "$$f.tmp" "$$f"; \ + fi; \ + done + post-install: # remove empty dirs @${FIND} ${STAGEDIR}${DATADIR} -type d -empty -delete @@ -61,8 +74,10 @@ 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 -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.25.2-20251201: 100% tests passed, 0 tests failed out of 3367 .include <bsd.port.mk> |