# 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=coq
pkgver=8.20.0
pkgrel=0
pkgdesc="Formal proof management system"
url="https://coq.inria.fr/"
# 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"
source="$pkgname-$pkgver.tar.gz::https://github.com/coq/coq/archive/V$pkgver.tar.gz"

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

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

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="
1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b  coq-8.20.0.tar.gz
"
