3 files changed, 52 insertions, 0 deletions
diff --git a/sci-mathematics/flocq/Manifest b/sci-mathematics/flocq/Manifest
new file mode 100644
index 000000000000..4f770414784e
--- /dev/null
+++ b/sci-mathematics/flocq/Manifest
@@ -0,0 +1,3 @@
+DIST flocq-4.1.0.tar.gz 447412 BLAKE2B 1b993a0e86bd440602b16b94ed5aff4b95a3c732eca87c683d239702b285dee8eaaf7dad77f730ae4929bb24504e5fd12b9a181d48efac4c3db7f0606637c018 SHA512 677e0de1406b3c7e5504d114a5b18ec07c719bbad79a2cfb750ac309fd5ab09be5493afdb1786b5a188cece59fddcd4167e28bf3be4facbdea8fe3b11cdf1ab1
+EBUILD flocq-4.1.0.ebuild 687 BLAKE2B 861d60eaba06ab5c3e6942ef00da0964112bc2860e2513cd052b1206ab911aa855b6102954d1944e0e4b1448b12bc125fef4407b4703dd7dc582dfe312695161 SHA512 8806148f7d5c5d1c9d0bdd8d145190238f8bde6df57c473d336f3b711e041766b095106601c9f8e4234892fd5878de68e9081fd1f8c244a4cc12f23678915c45
+MISC metadata.xml 685 BLAKE2B aa5fae67335fe3a4919e89654c550462d454586b6892aabd3d05940f2250d9368cc0195f1a761a8faf92245e8415711c99e28b6547a2c22c893a47f02aad4e89 SHA512 f2d195f05014e269699198abfa7c214a9ded40a635e32ff94b2d2d5c915d23a0664851118942c9e38b945721295aae2c80299f7370b8a2c2bbb4325b32bb8259
diff --git a/sci-mathematics/flocq/flocq-4.1.0.ebuild b/sci-mathematics/flocq/flocq-4.1.0.ebuild
new file mode 100644
index 000000000000..f48862539920
--- /dev/null
+++ b/sci-mathematics/flocq/flocq-4.1.0.ebuild
@@ -0,0 +1,31 @@
+# Copyright 1999-2022 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=">=sci-mathematics/coq-8.12"
+BDEPEND="${RDEPEND}"
+
+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
+}
diff --git a/sci-mathematics/flocq/metadata.xml b/sci-mathematics/flocq/metadata.xml
new file mode 100644
index 000000000000..4514b79800af
--- /dev/null
+++ b/sci-mathematics/flocq/metadata.xml
@@ -0,0 +1,18 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd">
+
+<pkgmetadata>
+  <maintainer type="project">
+    <email>sci-mathematics@gentoo.org</email>
+    <name>Gentoo Mathematics Project</name>
+  </maintainer>
+  <longdescription>
+    Flocq (Floats for Coq) is a formalization of floating-point arithmetic for
+    the Coq proof assistant. It provides a comprehensive library of theorems on
+    a multi-radix multi-precision arithmetic. It also supports efficient
+    numerical computations inside Coq.
+  </longdescription>
+  <upstream>
+    <bugs-to>https://gitlab.inria.fr/flocq/flocq/-/issues/</bugs-to>
+  </upstream>
+</pkgmetadata>