# Template file for 'rocq'
pkgname=rocq
version=9.0.0
revision=1
hostmakedepends="dune ocaml ocaml-findlib ocaml-num ocaml-zarith"
depends="ocaml-findlib"
checkdepends="python3 rsync time"
short_desc="Proof assistant written in OCaml"
maintainer="Orphaned <orphan@voidlinux.org>"
license="LGPL-2.1-only"
homepage="https://rocq-prover.org/"
distfiles="https://github.com/rocq-prover/rocq/releases/download/V${version}/rocq-${version}.tar.gz"
checksum=82f86646fd3d047f760837648195c73374beee667b1c9592d31c5426e3b43a51
nopie=yes
nocross=yes
make_check=ci-skip  # takes long and has some faults
replaces="coq>=0"

if [ "$XBPS_WORDSIZE" = 32 ]; then
	broken="Not enough heap memory to reserve minor heaps"
fi

do_patch() {
	if ! command -v ocamlc.opt >/dev/null; then
		# see coq/coq#18609
		vsed -i -e 's/dep ^ ".cmxs"/dep ^ ".cma"/' tools/dune_rule_gen/coq_rules.ml
	fi
}

do_build() {
	make dunestrap
	dune build --display=short -p rocq-core,rocq-runtime,coqide-server,coq-core
}

do_install() {
	dune install rocq-core rocq-runtime coqide-server coq-core --prefix=/usr --destdir="$DESTDIR" \
		--mandir=/usr/share/man --docdir=/usr/share/doc
}

do_check() {
	make -C test-suite UNIT_TESTS= || make -C test-suite report PRINT_LOGS=1
}
