# Maintainer: Celeste <cielesti@protonmail.com>
maintainer="Celeste <cielesti@protonmail.com>"
pkgname=rocq-stdlib
pkgver=9.0.0
pkgrel=0
pkgdesc="Formal proof management system (split-off standard library)"
url="https://rocq-prover.org/"
arch="all !armhf !armv7 !x86 !s390x !riscv64 !loongarch64" # follow rocq
license="LGPL-2.1-only"
depends="rocq~$pkgver"
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"
source="$pkgname-$pkgver.tar.gz::https://github.com/coq/stdlib/releases/download/V$pkgver/stdlib-$pkgver.tar.gz"
builddir="$srcdir/stdlib-$pkgver"

install_if="rocq~$pkgver"
replaces="coq"

build() {
	dune build -p rocq-stdlib
}

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

sha512sums="
97faa80d63a398c2c6872e043d65b1b907bb01ec3ea42f35cf757b3457b8fa2b64475d1577000ce2dea2c3f93e59e36cc5af9864adacf47f92db96ecbe307a45  rocq-stdlib-9.0.0.tar.gz
"
