Gentoo Packages

sci-mathematics/coq (gentoo)

Search

Package Information

Description:
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". Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.
Homepage:
https://rocq-prover.org https://github.com/rocq-prover/rocq/

Versions

Version EAPI Keywords Slot
9.1.1 8 ~amd64 ~arm64 0/9.1.1
9.1.0-r1 8 amd64 ~arm64 0/9.1.0-r1
9.0.0 8 ~amd64 ~arm64 0/9.0.0
8.20.0-r1 8 amd64 ~arm64 ~x86 0/8.20.0-r1
8.19.2-r1 8 amd64 ~arm64 ~x86 0/8.19.2-r1
8.17.1-r1 8 amd64 ~arm64 ~x86 0/8.17.1-r1

Metadata

Description

Maintainers

Upstream

Raw Metadata XML 
<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.

    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>
	<use>
		<flag name="native-compiler">
      Enable "native_compute" and compile the Coq Standard Library
    </flag>
	</use>
	<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>
</pkgmetadata>

Lint Warnings

USE Flags

Flag Description 9.1.1 9.1.0-r1 9.0.0 8.20.0-r1 8.19.2-r1 8.17.1-r1
debug Enable extra debug codepaths, like asserts and extra output. If you want to get meaningful backtraces see https://wiki.gentoo.org/wiki/Project:Quality_Assurance/Backtraces ✓ ✓ ✓ ✓ ✓ ✓
doc Add extra documentation (API, Javadoc, etc). It is recommended to enable per package instead of globally ✗ ✗ ✗ ✓ ✓ ✓
gui Enable support for a graphical user interface ✓ ✓ ✓ ✓ ✓ ✓
native-compiler Enable "native_compute" and compile the Coq Standard Library ✓ ✓ ✓ ✗ ✗ ✗
ocamlopt Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale) ⊕ ⊕ ⊕ ⊕ ⊕ ⊕
test Enable dependencies and/or preparations necessary to run tests (usually controlled by FEATURES=test but can be toggled independently) ✓ ✓ ✓ ✓ ✓ ✓

Manifest

Type File Size Versions
DIST coq-9.0.0.tar.gz 6305764 bytes 9.0.0
DIST coq-9.1.1.tar.gz 6395021 bytes 9.1.1
Unmatched Entries
Type File Size
DIST coq-8.17.1.tar.gz 7506035 bytes
DIST coq-8.19.2.tar.gz 7678311 bytes
DIST coq-8.20.0.tar.gz 7839432 bytes
DIST coq-9.1.0.tar.gz 6394996 bytes