commit: faa73bdb7a5c2aaa45860a143587fde7925202e1
Author: Maciej Barć <xgqt <AT> gentoo <DOT> org>
AuthorDate: Sun Sep 28 15:06:01 2025 +0000
Commit: Maciej Barć <xgqt <AT> gentoo <DOT> org>
CommitDate: Sun Sep 28 15:06:01 2025 +0000
URL: https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=faa73bdb
sci-mathematics/coq: update homepage and XML metadata
Signed-off-by: Maciej Barć <xgqt <AT> gentoo.org>
sci-mathematics/coq/coq-8.17.1-r1.ebuild | 5 +--
sci-mathematics/coq/coq-8.19.2-r1.ebuild | 5 +--
sci-mathematics/coq/coq-8.20.0-r1.ebuild | 4 +--
sci-mathematics/coq/coq-9.0.0.ebuild | 4 +--
sci-mathematics/coq/coq-9.1.0-r1.ebuild | 4 +--
sci-mathematics/coq/metadata.xml | 55 ++++++++++++++++----------------
6 files changed, 40 insertions(+), 37 deletions(-)
diff --git a/sci-mathematics/coq/coq-8.17.1-r1.ebuild
b/sci-mathematics/coq/coq-8.17.1-r1.ebuild
index 0376c24fc404..3c164c844d9b 100644
--- a/sci-mathematics/coq/coq-8.17.1-r1.ebuild
+++ b/sci-mathematics/coq/coq-8.17.1-r1.ebuild
@@ -9,8 +9,9 @@ MY_P="${PN}-${MY_PV}"
inherit check-reqs desktop dune edo
DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/
- https://github.com/coq/coq/";
+HOMEPAGE="https://rocq-prover.org
+ https://github.com/rocq-prover/rocq/";
+
SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz
-> ${P}.tar.gz"
S="${WORKDIR}/${MY_P}"
diff --git a/sci-mathematics/coq/coq-8.19.2-r1.ebuild
b/sci-mathematics/coq/coq-8.19.2-r1.ebuild
index 9613fc3a4f84..6b46ef0f3a4a 100644
--- a/sci-mathematics/coq/coq-8.19.2-r1.ebuild
+++ b/sci-mathematics/coq/coq-8.19.2-r1.ebuild
@@ -9,8 +9,9 @@ MY_P="${PN}-${MY_PV}"
inherit check-reqs desktop dune edo
DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="http://coq.inria.fr/
- https://github.com/coq/coq/";
+HOMEPAGE="https://rocq-prover.org
+ https://github.com/rocq-prover/rocq/";
+
SRC_URI="https://github.com/coq/coq/archive/V${MY_PV}.tar.gz
-> ${P}.tar.gz"
S="${WORKDIR}/${MY_P}"
diff --git a/sci-mathematics/coq/coq-8.20.0-r1.ebuild
b/sci-mathematics/coq/coq-8.20.0-r1.ebuild
index 1c69a8de9461..c1bd2a1ba337 100644
--- a/sci-mathematics/coq/coq-8.20.0-r1.ebuild
+++ b/sci-mathematics/coq/coq-8.20.0-r1.ebuild
@@ -6,8 +6,8 @@ EAPI=8
inherit check-reqs desktop dune edo
DESCRIPTION="Proof assistant written in O'Caml"
-HOMEPAGE="https://coq.inria.fr/
- https://github.com/coq/coq/";
+HOMEPAGE="https://rocq-prover.org
+ https://github.com/rocq-prover/rocq/";
if [[ "${PV}" == *9999* ]] ; then
inherit git-r3
diff --git a/sci-mathematics/coq/coq-9.0.0.ebuild
b/sci-mathematics/coq/coq-9.0.0.ebuild
index ac81887a2d4a..09bf3909c962 100644
--- a/sci-mathematics/coq/coq-9.0.0.ebuild
+++ b/sci-mathematics/coq/coq-9.0.0.ebuild
@@ -6,8 +6,8 @@ EAPI=8
inherit check-reqs desktop dune edo
DESCRIPTION="Coq/Rocq is a proof assistant written in O'Caml"
-HOMEPAGE="https://coq.inria.fr/
- https://github.com/coq/coq/";
+HOMEPAGE="https://rocq-prover.org
+ https://github.com/rocq-prover/rocq/";
if [[ "${PV}" == *9999* ]] ; then
inherit git-r3
diff --git a/sci-mathematics/coq/coq-9.1.0-r1.ebuild
b/sci-mathematics/coq/coq-9.1.0-r1.ebuild
index 21b7bffc808e..ac9ad6e10d8f 100644
--- a/sci-mathematics/coq/coq-9.1.0-r1.ebuild
+++ b/sci-mathematics/coq/coq-9.1.0-r1.ebuild
@@ -6,8 +6,8 @@ EAPI=8
inherit check-reqs desktop dune edo
DESCRIPTION="Coq/Rocq is a proof assistant written in O'Caml"
-HOMEPAGE="https://coq.inria.fr/
- https://github.com/coq/coq/";
+HOMEPAGE="https://rocq-prover.org
+ https://github.com/rocq-prover/rocq/";
if [[ "${PV}" == *9999* ]] ; then
inherit git-r3
diff --git a/sci-mathematics/coq/metadata.xml b/sci-mathematics/coq/metadata.xml
index 3e812d4a672d..6c71a7b57166 100644
--- a/sci-mathematics/coq/metadata.xml
+++ b/sci-mathematics/coq/metadata.xml
@@ -1,33 +1,34 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE pkgmetadata SYSTEM "https://www.gentoo.org/dtd/metadata.dtd";>
+
<pkgmetadata>
- <maintainer type="project">
- <email>[email protected]</email>
- <name>Gentoo Mathematics Project</name>
- </maintainer>
- <longdescription>
- Developed in the LogiCal project, the Coq tool is a formal proof
- management system: a proof done with Coq is mechanically checked
- by the machine.
+ <maintainer type="project">
+ <email>[email protected]</email>
+ <name>Gentoo Mathematics Project</name>
+ </maintainer>
+ <longdescription>
+ Developed in the LogiCal project, the Coq tool is a formal proof
+ management system: a proof done with Coq is mechanically checked
+ by the machine.
- In particular, Coq allows:
- * the definition of functions or predicates,
- * to state mathematical theorems and software specifications,
- * to develop interactively formal proofs of these theorems,
- * to check these proofs by a small certification "kernel".
+ In particular, Coq allows:
+ * the definition of functions or predicates,
+ * to state mathematical theorems and software specifications,
+ * to develop interactively formal proofs of these theorems,
+ * to check these proofs by a small certification "kernel".
- Coq is based on a logical framework called "Calculus of Inductive
- Constructions" extended by a modular development system for
- theories.
- </longdescription>
- <upstream>
- <changelog>https://github.com/coq/coq/releases/</changelog>
- <bugs-to>https://github.com/coq/coq/issues/</bugs-to>
- <remote-id type="github">coq/coq</remote-id>
- </upstream>
- <use>
- <flag name="native-compiler">
- Enable "native_compute" and compile the Coq Standard
Library
- </flag>
- </use>
+ Coq is based on a logical framework called "Calculus of Inductive
+ Constructions" extended by a modular development system for
+ theories.
+ </longdescription>
+ <upstream>
+ <changelog>https://github.com/rocq-prover/rocq/releases/</changelog>
+ <bugs-to>https://github.com/rocq-prover/rocq/issues/</bugs-to>
+ <remote-id type="github">rocq-prover/rocq</remote-id>
+ </upstream>
+ <use>
+ <flag name="native-compiler">
+ Enable "native_compute" and compile the Coq Standard Library
+ </flag>
+ </use>
</pkgmetadata>
