# Contributor: alpine-mips-patches <info@mobile-stream.com>
# Contributor: omni <omni+alpine@hack.org>
# Maintainer: alpine-mips-patches <info@mobile-stream.com>
pkgname=coq
pkgver=8.16.1
pkgrel=0
pkgdesc="A formal proof management system"
url="https://coq.inria.fr"
arch="all !riscv64" # limited by ocaml aport
license="LGPL-2.1-or-later"
depends="ocaml-runtime"
makedepends="
	bash
	dune
	ocaml
	ocaml-compiler-libs
	ocaml-findlib-dev
	ocaml-num-dev
	ocaml-zarith
"
options="!check" # many tests in 'make test-suite' fail
subpackages="$pkgname-doc"
source="$pkgname-$pkgver.tar.gz::https://github.com/coq/coq/archive/V$pkgver.tar.gz"

# 32bit archs
case "$CARCH" in
armv7|armhf|mips|x86) options="$options textrels" ;;
esac

build() {
	./configure \
		-prefix /usr \
		-bytecode-compiler no \
		-coqide no

	case "$CARCH" in
		s390x) OCAMLPATH=/usr/lib/ocaml CAML_LD_LIBRARY_PATH=/usr/lib/ocaml/zarith/ make -j1;;
		*) OCAMLPATH=/usr/lib/ocaml CAML_LD_LIBRARY_PATH=/usr/lib/ocaml/zarith/ make;;
	esac
}

package() {
	make -j1 DESTDIR="$pkgdir" install
}

sha512sums="
e9c82f1a180c2e3946628e8e039999a1841397a5b4cd77f158de69876fa43b5c0f61ce76c510cc2b2f646a489110aea59da452b88ddd7850d1eab4105f1382f5  coq-8.16.1.tar.gz
"