[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/flocq/

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/flocq/

[Maciej Barć]

commit:     889a3cff4fa58c3b06643479ec34656758c52315
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Dec 24 21:28:46 2022 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Dec 24 22:26:48 2022 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=889a3cff

sci-mathematics/flocq: new package; add 4.1.0

Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/flocq/Manifest           |  1 +
 sci-mathematics/flocq/flocq-4.1.0.ebuild | 31 +++++++++++++++++++++++++++++++
 sci-mathematics/flocq/metadata.xml       | 18 ++++++++++++++++++
 3 files changed, 50 insertions(+)

diff --git a/sci-mathematics/flocq/Manifest b/sci-mathematics/flocq/Manifest
new file mode 100644
index 000000000000..f04ae7c7ad49
--- /dev/null
+++ b/sci-mathematics/flocq/Manifest
@@ -0,0 +1 @@
+DIST flocq-4.1.0.tar.gz 447412 BLAKE2B 1b993a0e86bd440602b16b94ed5aff4b95a3c732eca87c683d239702b285dee8eaaf7dad77f730ae4929bb24504e5fd12b9a181d48efac4c3db7f0606637c018 SHA512 677e0de1406b3c7e5504d114a5b18ec07c719bbad79a2cfb750ac309fd5ab09be5493afdb1786b5a188cece59fddcd4167e28bf3be4facbdea8fe3b11cdf1ab1

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>

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/flocq/

[Maciej Barć]

commit:     f0fa8cbb62c755c347fca77a212d6f0ceb1d89ba
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Thu Feb 16 11:51:11 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Thu Feb 16 11:55:45 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=f0fa8cbb

sci-mathematics/flocq: fix deps

Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 .../flocq/{flocq-4.1.0.ebuild => flocq-4.1.0-r1.ebuild}          | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/sci-mathematics/flocq/flocq-4.1.0.ebuild b/sci-mathematics/flocq/flocq-4.1.0-r1.ebuild
similarity index 83%
rename from sci-mathematics/flocq/flocq-4.1.0.ebuild
rename to sci-mathematics/flocq/flocq-4.1.0-r1.ebuild
index f48862539920..f70775d38f46 100644
--- a/sci-mathematics/flocq/flocq-4.1.0.ebuild
+++ b/sci-mathematics/flocq/flocq-4.1.0-r1.ebuild
@@ -1,4 +1,4 @@
-# Copyright 1999-2022 Gentoo Authors
+# Copyright 1999-2023 Gentoo Authors
 # Distributed under the terms of the GNU General Public License v2
 
 EAPI=8
@@ -14,8 +14,11 @@ LICENSE="LGPL-3"
 SLOT="0"
 KEYWORDS="~amd64 ~x86"
 
-RDEPEND=">=sci-mathematics/coq-8.12"
-BDEPEND="${RDEPEND}"
+RDEPEND="
+	dev-lang/ocaml:=
+	>=sci-mathematics/coq-8.12:=
+"
+DEPEND="${RDEPEND}"
 
 src_compile() {
 	./remake --jobs=$(makeopts_jobs) || die

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/flocq/

[Maciej Barć]

commit:     63e7f70de010945b04f0666c2f18704d552c2b6e
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sat Apr  1 21:48:45 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sat Apr  1 22:35:48 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=63e7f70d

sci-mathematics/flocq: bump to 4.1.1

Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/flocq/Manifest           |  1 +
 sci-mathematics/flocq/flocq-4.1.1.ebuild | 34 ++++++++++++++++++++++++++++++++
 2 files changed, 35 insertions(+)

diff --git a/sci-mathematics/flocq/Manifest b/sci-mathematics/flocq/Manifest
index f04ae7c7ad49..094cfd9c64ee 100644
--- a/sci-mathematics/flocq/Manifest
+++ b/sci-mathematics/flocq/Manifest
@@ -1 +1,2 @@
 DIST flocq-4.1.0.tar.gz 447412 BLAKE2B 1b993a0e86bd440602b16b94ed5aff4b95a3c732eca87c683d239702b285dee8eaaf7dad77f730ae4929bb24504e5fd12b9a181d48efac4c3db7f0606637c018 SHA512 677e0de1406b3c7e5504d114a5b18ec07c719bbad79a2cfb750ac309fd5ab09be5493afdb1786b5a188cece59fddcd4167e28bf3be4facbdea8fe3b11cdf1ab1
+DIST flocq-4.1.1.tar.gz 450132 BLAKE2B 00821a3e135156640320d1afd548bc1912953bba64cc675b7b6c94b4e3c792c444bfbb4ef1a3352adefa466548083e32c2b1e4b38747dcbc6ac6de6d72250a74 SHA512 7076b8d5e33b8225e0124b9f66f4e3e1ed3e30804c5bca28e30d5e176c1b8c5c3d777a28c243fada17ab4ed32f580c6d606b11f045d48f7acb15e03db59870c4

diff --git a/sci-mathematics/flocq/flocq-4.1.1.ebuild b/sci-mathematics/flocq/flocq-4.1.1.ebuild
new file mode 100644
index 000000000000..f70775d38f46
--- /dev/null
+++ b/sci-mathematics/flocq/flocq-4.1.1.ebuild
@@ -0,0 +1,34 @@
+# Copyright 1999-2023 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.12:=
+"
+DEPEND="${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
+}

[gentoo-commits] repo/gentoo:master commit in: sci-mathematics/flocq/

[Maciej Barć]

commit:     66e46e9f808925425d9ba22f89d0794ce3fafa87
Author:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Tue Apr 11 12:02:16 2023 +0000
Commit:     Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Tue Apr 11 14:17:01 2023 +0000
URL:        https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=66e46e9f

sci-mathematics/flocq: ignore CFLAGS for ML/Coq code

Closes: https://bugs.gentoo.org/904156
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>

 sci-mathematics/flocq/flocq-4.1.0-r1.ebuild | 3 +++
 sci-mathematics/flocq/flocq-4.1.1.ebuild    | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/sci-mathematics/flocq/flocq-4.1.0-r1.ebuild b/sci-mathematics/flocq/flocq-4.1.0-r1.ebuild
index f70775d38f46..a547b9e58320 100644
--- a/sci-mathematics/flocq/flocq-4.1.0-r1.ebuild
+++ b/sci-mathematics/flocq/flocq-4.1.0-r1.ebuild
@@ -20,6 +20,9 @@ RDEPEND="
 "
 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
 }

diff --git a/sci-mathematics/flocq/flocq-4.1.1.ebuild b/sci-mathematics/flocq/flocq-4.1.1.ebuild
index f70775d38f46..a547b9e58320 100644
--- a/sci-mathematics/flocq/flocq-4.1.1.ebuild
+++ b/sci-mathematics/flocq/flocq-4.1.1.ebuild
@@ -20,6 +20,9 @@ RDEPEND="
 "
 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
 }