PORTNAME=	lean4
DISTVERSIONPREFIX=	v
DISTVERSION=	4.35.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
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.5:mimalloc/cmake/mimalloc/src/mimalloc \
		Kha:lean4lean:lean4-bundle-4.35:lean4lean/ext/lean4lean

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:
	# Disable git downloads of optional checkers (not built by default)
	@${REINPLACE_CMD} -E \
		-e 's|GIT_REPOSITORY https://github.com/(ammkrn/nanoda_lib\|leanprover/con-leche\|leanprover/con-ron)|DOWNLOAD_COMMAND ""|' \
		-e '/GIT_TAG [0-9a-f]{40}/d' \
		-e '/GIT_SUBMODULES ""/d' \
		${WRKSRC}/src/CMakeLists.txt ${WRKSRC}/stage0/src/CMakeLists.txt
	# 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
# tests as of 4.35.0: 99% tests passed, 2 tests failed out of 4218: same cacheTransfer/test.sh failure, pkg/float failure

.include <bsd.port.mk>