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-rc3
DISTNAME =		mathlib-4.35.0rc3

DIST_TUPLE +=		github leanprover-community plausible fb13df72ecefd8ddbf9291021d7f33a8673eb57b .lake/packages/plausible
DIST_TUPLE +=		github leanprover-community LeanSearchClient 29ff470276c725ae01505d55b17148c18fc7dfd3 .lake/packages/LeanSearchClient
DIST_TUPLE +=		github leanprover-community import-graph 7e81a29bda33a6b257bd37557a6aa6aebe175d96 .lake/packages/importGraph
DIST_TUPLE +=		github leanprover-community ProofWidgets4 c643bbb3c24f8a25f9c14e3a6b1ceb13d01f3de1 .lake/packages/proofwidgets
DIST_TUPLE +=		github leanprover-community aesop a90fbf7b02ff06a0deebf74088dff9e5fe02c9ea .lake/packages/aesop
DIST_TUPLE +=		github leanprover-community quote4 37b0ba0b26109cf9f9c541f0f9557e50cfa1a3b9 .lake/packages/Qq
DIST_TUPLE +=		github leanprover-community batteries 3b7c8101932390d60e92a3f3d917901d5b5a773b .lake/packages/batteries
DIST_TUPLE +=		github leanprover lean4-cli 843844fa601dd56767b1eb22b7ada5b64d5e567a .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>
