# Contributor: alpine-mips-patches <info@mobile-stream.com>
# Contributor: omni <omni+alpine@hack.org>
# Contributor: Jason Gross <jasongross9@gmail.com>
# Maintainer: Celeste <cielesti@protonmail.com>
maintainer="Celeste <cielesti@protonmail.com>"
pkgname=rocq
pkgver=9.0.0	# upgrade together with rocq-stdlib
pkgrel=0
pkgdesc="Formal proof management system"
url="https://rocq-prover.org/"
# riscv64, loongarch64: ocaml
# s390x: not useful
# 32-bit: huge package and nobody would use it there
arch="all !armhf !armv7 !x86 !s390x !riscv64 !loongarch64"
license="LGPL-2.1-or-later"
makedepends="
	bash
	dune
	linux-headers
	ocaml
	ocaml-compiler-libs
	ocaml-findlib-dev
	ocaml-zarith
	"
options="!check" # many tests in 'make test-suite' fail
subpackages="
	$pkgname-doc
	coqide-server
	"
source="https://github.com/coq/coq/releases/download/V$pkgver/rocq-$pkgver.tar.gz"
builddir="$srcdir/coq-$pkgver"

provides="coq=$pkgver-r$pkgrel"
replaces="coq"

_components="rocq-runtime coq-core rocq-core coq coqide-server"

build() {
	./configure \
		-prefix /usr \
		-mandir /usr/share/man \
		-docdir /usr/share/doc \
		-libdir "$(ocamlc -where)/coq"
	make dunestrap
	dune build -p "${_components//\ /,}"
}

package() {
	dune install $_components \
		--prefix=/usr \
		--destdir="$pkgdir" \
		--mandir=/usr/share/man \
		--docdir=/usr/share/doc \
		--libdir="$(ocamlc -where)"

	# fix coqidetop.byte
	install -Dvm755 _build/default/ide/rocqide/dllplatform_specific_stubs.so \
		-t "$pkgdir"/usr/lib/ocaml/stublibs/
}

server() {
	pkgdesc="$pkgdesc (XML protocol server)"
	depends="$pkgname=$pkgver-r$pkgrel"

	amove \
		usr/bin/coqidetop \
		usr/lib/ocaml/coqide-server \
		usr/lib/ocaml/stublibs/dllplatform_specific_stubs.so
}

prepare_py_provides() {
	local datadir="${subpkgdir:-$pkgdir}"
	local pkgbasedir=${pkgbasedir:-"$startdir/pkg"}
	local controldir="$pkgbasedir"/.control.${subpkgname:-$pkgname}

	options_has "!tracedeps" && return 0

	ocaml4-abuild-find provides \
		"$datadir"/usr/lib/ocaml \
		"$controldir" \
		"$pkgver-r$pkgrel"
}

scan_python3_dependency() {
	local controldir="$2" datadir="$3"

	ocaml4-abuild-find requires \
		"$datadir"/usr/lib/ocaml \
		"$controldir"
}

sha512sums="
f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be  rocq-9.0.0.tar.gz
"
