COMMENT =		mathematical library for Lean 4

DPB_PROPERTIES =	parallel

# keep it synced with math/lean
GH_ACCOUNT =		leanprover-community
GH_PROJECT =		mathlib4
GH_TAGNAME =		v4.35.0-rc4
DISTNAME =		mathlib-4.35.0rc4

DIST_TUPLE +=		github leanprover-community plausible aef59637faa9e85fa2486acaaf906ce3f572af7c .lake/packages/plausible
DIST_TUPLE +=		github leanprover-community LeanSearchClient 234d9e074fbd6e911b920baf32db5291c3125be0 .lake/packages/LeanSearchClient
DIST_TUPLE +=		github leanprover-community import-graph 579f558774c4ac6840e715ba60dabf3030619349 .lake/packages/importGraph
DIST_TUPLE +=		github leanprover-community ProofWidgets4 d5ad4a0b79fa7f9818fe1380d05a3f6143823c09 .lake/packages/proofwidgets
DIST_TUPLE +=		github leanprover-community aesop 04879b1e1de744d5c9777c8cf63fa55a8f652e5e .lake/packages/aesop
DIST_TUPLE +=		github leanprover-community quote4 e7c4cdd2f1bf9df361ef7f621b4d6867012ab65e .lake/packages/Qq
DIST_TUPLE +=		github leanprover-community batteries b71aaf60877e673fdb921f06f20987d12ee8a290 .lake/packages/batteries
DIST_TUPLE +=		github leanprover lean4-cli 82c11b9717083154aefc5fe8d4cba4bbf046298f .lake/packages/Cli

CATEGORIES =		math

HOMEPAGE =		https://leanprover-community.github.io/

MAINTAINER =		Kirill A. Korinsky <kirill@korins.ky>

# Apache 2.0
PERMIT_PACKAGE =	Yes

BUILD_DEPENDS =		math/lean \
			textproc/jq

RUN_DEPENDS =		math/lean

# Default stack is 1Gb per thread, limit it for compiling
MAKE_ENV +=		LEAN_STACK_SIZE_KB=65536 \
			LEAN_NUM_THREADS=${MAKE_JOBS} \
			LAKE_ARTIFACT_CACHE=false \
			MATHLIB_NO_CACHE_ON_UPDATE=1

NO_TEST =		Yes

pre-configure:
	cd ${WRKSRC} && ${LOCALBASE}/bin/jq \
	    '.packages |= map(.type = "path" | .dir = (".lake/packages/" + .name) | del(.url, .rev, .inputRev, .subDir))' \
	    lake-manifest.json > lake-manifest.json.tmp
	mv ${WRKSRC}/lake-manifest.json.tmp ${WRKSRC}/lake-manifest.json

do-build:
	cd ${WRKSRC} && ${SETENV} ${MAKE_ENV} \
	    ${LOCALBASE}/bin/lake --no-cache build Mathlib

do-install:
	${INSTALL_DATA_DIR} ${PREFIX}/lib/lean ${PREFIX}/src/lean
	for pkg in ${WRKSRC} ${WRKSRC}/.lake/packages/*; do \
		if [ -d "$$pkg/.lake/build/lib/lean" ]; then \
			tar -cf - -C "$$pkg/.lake/build/lib/lean" \
			    -s ',.*\.hash$$,,' -s ',.*\.trace$$,,' . | \
			    tar -xf - -C ${PREFIX}/lib/lean; \
			(cd "$$pkg/.lake/build/lib/lean" && \
			    find . -type f -name '*.olean') | \
			    sed 's,\.olean$$,.lean,' | \
			    tar -cf - -C "$$pkg" -I - | \
			    tar -xf - -C ${PREFIX}/src/lean; \
		fi; \
	done

.include <bsd.port.mk>
