gentoo-mirror/gentoo
1
0
Fork 0
mirror of https://github.com/gentoo-mirror/gentoo.git synced 2026-08-05 12:38:09 -07:00
Code Issues Projects Releases Wiki Activity

sci-mathematics/coq: update homepage and XML metadata

Browse Source 
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
This commit is contained in:
Maciej Barć
2025-09-28 17:06:01 +02:00
parent fb02487ba9
commit faa73bdb7a
6 changed files with 40 additions and 37 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
sci-mathematics/coq/coq-8.17.1-r1.ebuild
View File

@@ -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}"

5
sci-mathematics/coq/coq-8.19.2-r1.ebuild
View File

@@ -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}"

4
sci-mathematics/coq/coq-8.20.0-r1.ebuild
View File

@@ -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

4
sci-mathematics/coq/coq-9.0.0.ebuild
View File

@@ -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

4
sci-mathematics/coq/coq-9.1.0-r1.ebuild
View File

@@ -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

55
sci-mathematics/coq/metadata.xml
View File

@@ -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>sci-mathematics@gentoo.org</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>sci-mathematics@gentoo.org</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>