126 lines
5.0 KiB
Makefile
126 lines
5.0 KiB
Makefile
PORTNAME= lean4
|
|
DISTVERSIONPREFIX= v
|
|
DISTVERSION= 4.34.1
|
|
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
|
|
COMMENT= Theorem prover and functional language for math (new gen)
|
|
WWW= https://lean-lang.org/ \
|
|
https://github.com/leanprover/lean4
|
|
|
|
LICENSE= APACHE20
|
|
LICENSE_FILE= ${WRKSRC}/LICENSE
|
|
|
|
BROKEN_FreeBSD_14= compilation fails: .rsp files are not supprted by ar on 14: ar there is from Elftoolchain project which was later replaced by LLVM ar, which supports .rsp files
|
|
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)
|
|
|
|
BUILD_DEPENDS= bash:shells/bash \
|
|
cadical:math/cadical \
|
|
leantar:math/leangz
|
|
LIB_DEPENDS= libgmp.so:math/gmp \
|
|
libuv.so:devel/libuv
|
|
RUN_DEPENDS= cadical:math/cadical \
|
|
leantar:math/leangz
|
|
TEST_DEPENDS= bash:shells/bash \
|
|
git:devel/git \
|
|
gtail:sysutils/coreutils
|
|
|
|
USES= cmake:noninja,testing compiler:c++14-lang gmake pkgconfig python:build # ninja fails + gmake scripts are included in the project
|
|
|
|
USE_GITHUB= yes
|
|
GH_ACCOUNT= leanprover
|
|
GH_TUPLE= microsoft:mimalloc:v3.4.4:mimalloc/cmake/mimalloc/src/mimalloc
|
|
|
|
CFLAGS+= -fPIC
|
|
CXXFLAGS+= -fPIC
|
|
|
|
CMAKE_OFF= INSTALL_LEANTAR
|
|
|
|
#MAKE_ARGS+= V=1 VERBOSE=1
|
|
MAKE_ENV= LD_LIBRARY_PATH=${BUILD_WRKSRC}/stage0/lib/lean
|
|
|
|
BINARY_ALIAS= make=${GMAKE} \
|
|
python=${PYTHON_CMD} \
|
|
python3=${PYTHON_CMD}
|
|
|
|
CMAKE_ARGS+= -DLEANTAR=${LOCALBASE}/bin/leantar
|
|
|
|
# tests run in a very high memory on a 32-core system: 55GB
|
|
CMAKE_TESTING_JOBS= 8 # not respected, see https://github.com/leanprover/lean4/issues/15334 (workaround: run tests with 'cpuset -l 0-7' to limit parallelism)
|
|
|
|
CONFLICTS_BUILD= gsed # this should be CONFLICTS_TEST but it isn't defined; pesence of gsed for some reason makes several tests fail
|
|
|
|
OPTIONS_DEFINE= MIMALLOC
|
|
OPTIONS_DEFAULT= #MIMALLOC
|
|
OPTIONS_SUB= yes
|
|
|
|
MIMALLOC_DESC= Use mimalloc memory allocator (enables some optimizations in the code)
|
|
MIMALLOC_CMAKE_BOOL= USE_MIMALLOC
|
|
MIMALLOC_BROKEN= many tests print messages like: pid 34707 comm StackOverflow.lean. tid 1036070 stack overflow
|
|
|
|
pre-configure:
|
|
@${MKDIR} ${BUILD_WRKSRC}/mimalloc/src
|
|
@${LN} -sf ${WRKSRC}/cmake/mimalloc/src/mimalloc ${BUILD_WRKSRC}/mimalloc/src/mimalloc
|
|
|
|
post-configure:
|
|
# Copy leantar to build bin directories for tests (INSTALL_LEANTAR=OFF disables the built-in copy)
|
|
@${MKDIR} ${BUILD_WRKSRC}/stage0/bin ${BUILD_WRKSRC}/stage1/bin
|
|
@${CP} ${LOCALBASE}/bin/leantar ${BUILD_WRKSRC}/stage0/bin/
|
|
@${CP} ${LOCALBASE}/bin/leantar ${BUILD_WRKSRC}/stage1/bin/
|
|
# Create a test-only bin dir with gmake as "make" for tests needing GNU make (e.g. reverse-ffi) (need to see why BINARY ALIAS doesn't work for this)
|
|
@${MKDIR} ${BUILD_WRKSRC}/test-bin
|
|
@${LN} -sf ${LOCALBASE}/bin/gmake ${BUILD_WRKSRC}/test-bin/make
|
|
|
|
pre-everything::
|
|
@${ECHO_MSG} ""
|
|
@${ECHO_MSG} "Please note that build Lean requires /proc to be mounted."
|
|
@${ECHO_MSG} ""
|
|
@${ECHO_MSG} " The usual way to do this is to add this line to /etc/fstab:"
|
|
@${ECHO_MSG} " proc /proc procfs rw 0 0"
|
|
@${ECHO_MSG} ""
|
|
@${ECHO_MSG} " and then run this command as root:"
|
|
@${ECHO_MSG} " # mount /proc"
|
|
@${ECHO_MSG} ""
|
|
|
|
post-patch:
|
|
# Add weakLeancArgs = ["-fPIC"] to all test lakefile.toml files
|
|
# Skip inputFile test: its translate-config test expects exact TOML-to-Lean output
|
|
@${FIND} ${WRKSRC}/tests -name "lakefile.toml" -not -path "*/inputFile/*" | 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
|
|
# remove stray files
|
|
@${RM} ${STAGEDIR}${PREFIX}/LICENSE*
|
|
# remove bin/cadical, workaround for https://github.com/leanprover/lean4/issues/5603
|
|
@${RM} ${STAGEDIR}${PREFIX}/bin/cadical
|
|
# remove bin/leantar (we use the one from math/leangz)
|
|
@${RM} ${STAGEDIR}${PREFIX}/bin/leantar
|
|
# strip binaries
|
|
@cd ${STAGEDIR}${PREFIX} && ${STRIP_CMD} \
|
|
bin/lake \
|
|
bin/lean \
|
|
bin/leanc \
|
|
bin/leanir \
|
|
lib/lean/libInit_shared.so \
|
|
lib/lean/libleanshared.so \
|
|
lib/lean/libleanshared_1.so \
|
|
lib/lean/libleanshared_2.so \
|
|
lib/lean/libLake_shared.so
|
|
|
|
# tests as of 4.33.1: 100% tests passed, 0 tests failed out of 3988
|
|
# tests as of 4.34.0: 100% tests pass (individual testsuite runs have intermittent failures with different tests, but all individual tests pass when run separately)
|
|
# tests as of 4.34.1: 99% tests passed, 1 tests failed out of 4068: the 2 months old test cacheTransfer/test.sh fails, see https://github.com/leanprover/lean4/issues/15335
|
|
|
|
.include <bsd.port.mk>
|