| Version | EAPI | Keywords | Slot |
|---|---|---|---|
| 4.2.1 | 8 | ~amd64 ~x86 | 0 |
# Copyright 1999-2025 Gentoo Authors
# Distributed under the terms of the GNU General Public License v2
EAPI=8
inherit multiprocessing
DESCRIPTION="Formalization of floating-point arithmetic for the Coq proof assistant"
HOMEPAGE="http://flocq.gforge.inria.fr/
https://gitlab.inria.fr/flocq/flocq/"
SRC_URI="https://flocq.gitlabpages.inria.fr/releases/${P}.tar.gz"
LICENSE="LGPL-3"
SLOT="0"
KEYWORDS="~amd64 ~x86"
RDEPEND="
dev-lang/ocaml:=
>=sci-mathematics/coq-8.15:=
"
DEPEND="
${RDEPEND}
"
# Do not complain about CFLAGS etc since ML projects do not use them.
QA_FLAGS_IGNORED='.*'
src_compile() {
./remake --jobs=$(makeopts_jobs) || die
}
src_install() {
DESTDIR="${D}" ./remake install || die
dodoc AUTHORS INSTALL.md NEWS.md README.md
insinto "/usr/share/${PN}"
doins -r examples
}
dev-lang/ocaml:= >=sci-mathematics/coq-8.15:=
dev-lang/ocaml:= >=sci-mathematics/coq-8.15:=
| Type | File | Size | Source URLs |
|---|---|---|---|
| DIST | flocq-4.2.1.tar.gz | 447822 bytes | https://flocq.gitlabpages.inria.fr/releases/flocq-4.2.1.tar.gz |