## Summary

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.

## Versions

v8.6.1 :: 0 :: gentoo

- Modified
- License
- LGPL-2.1
- Keywords
- ~amd64 ~ppc ~x86
- USE flags
- camlp5 debug doc gtk ocamlopt

v8.6 :: 0 :: gentoo

- Modified
- License
- LGPL-2.1
- Keywords
- amd64 ppc x86
- USE flags
- camlp5 debug doc gtk ocamlopt

## USE flags

### General

- camlp5
- Build using camlp5. This is required for some plugins like Ssreflect.
- 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
- gtk
- Add support for x11-libs/gtk+ (The GIMP Toolkit)
- ocamlopt
- Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)

## Dependencies

dev-lang / ocaml : Type-inferring functional programming language descended from the ML family

dev-ml / camlp4 : System for writing extensible parsers for programming languages

dev-ml / camlp5 : A preprocessor-pretty-printer of ocaml

dev-ml / findlib : OCaml tool to find/use non-standard packages

dev-ml / lablgtk : Objective CAML interface for Gtk+2

dev-tex / hevea : HeVeA is a quite complete and fast LaTeX to HTML translator

dev-tex / xcolor : xcolor -- easy driver-independent access to colors

dev-texlive / texlive-latexextra : TeXLive LaTeX additional packages

dev-texlive / texlive-mathscience : TeXLive Mathematics, natural sciences, computer science packages

dev-texlive / texlive-pictures : TeXLive Graphics, pictures, diagrams

media-libs / netpbm : A set of utilities for converting to/from the netpbm (and related) formats

virtual / latex-base : Virtual for basic LaTeX binaries

## Runtime Dependencies

dev-lang / ocaml : Type-inferring functional programming language descended from the ML family

dev-ml / camlp4 : System for writing extensible parsers for programming languages

## Depending packages

sci-mathematics / why3-for-spark : Platform for deductive program verification

## Bugs

- 554232
- sci-mathematics/coq-8.4_p6 fails test bugs/closed/shouldsucceed/2456.v
- 559564
- sys-apps/portage-2.2.20.1: a slot conflict between dev-lang/ocaml and sci-mathematics/coq cannot be auto resolved
- 625120
- sci-mathematics/coq-8.6 : Error: The files /usr/lib64/ocaml/pervasives.cmi
- 653864
- sci-mathematics/coq-8.9.0 version bump
- 672038
- Request sci-mathematics/coq-8.8 ebuild

## Change logs

- Andreas Sturmlechner · gentoo

sci-mathematics/coq: Drop obsolete dev-texlive/texlive-mathextra

Package-Manager: Portage-2.3.28, Repoman-2.3.9 - Alexis Ballier · gentoo

sci-mathematics/coq: bump to 8.6.1

Package-Manager: Portage-2.3.6, Repoman-2.3.2 - Alexis Ballier · gentoo

sci-mathematics/coq: Remove old

Package-Manager: Portage-2.3.6, Repoman-2.3.2 - Agostino Sarubbo · gentoo

sci-mathematics/coq: ppc stable wrt bug #619676

Package-Manager: Portage-2.3.6, Repoman-2.3.1 RepoMan-Options: --include-arches="ppc" Signed-off-by: Agostino Sarubbo <ago@gentoo.org> - Agostino Sarubbo · gentoo

sci-mathematics/coq: x86 stable wrt bug #619676

Package-Manager: Portage-2.3.6, Repoman-2.3.1 RepoMan-Options: --include-arches="x86" Signed-off-by: Agostino Sarubbo <ago@gentoo.org> - Agostino Sarubbo · gentoo

sci-mathematics/coq: amd64 stable wrt bug #619676

Package-Manager: Portage-2.3.6, Repoman-2.3.1 RepoMan-Options: --include-arches="amd64" Signed-off-by: Agostino Sarubbo <ago@gentoo.org> - Robin H. Johnson · gentoo

Drop $Id$ per council decision in bug #611234.

Signed-off-by: Robin H. Johnson <robbat2@gentoo.org> - T. Malfatti · gentoo

media-libs/portaudio: Version bump - Alexis Ballier · gentoo

sci-mathematics/coq: adjust deps for TeX Live 2016.

Package-Manager: Portage-2.3.3, Repoman-2.3.1 - Alexis Ballier · gentoo

sci-mathematics/coq: remove old

Package-Manager: Portage-2.3.3, Repoman-2.3.1 - Alexis Ballier · gentoo

sci-mathematics/coq: add missing findlib build dep, bug #603126

Package-Manager: Portage-2.3.3, Repoman-2.3.1 - Alexis Ballier · gentoo

sci-mathematics/coq: bump to 8.6

Package-Manager: Portage-2.3.3, Repoman-2.3.1 - Alexis Ballier · gentoo

sci-mathematics/coq: bump to 8.5pl3

Package-Manager: portage-2.3.2 - Alexis Ballier · gentoo

sci-mathematics/coq: drop ocaml 4.03 patch; it is not needed anymore.

Package-Manager: portage-2.3.0 - Alexis Ballier · gentoo

sci-mathematics/coq: bump to 8.5pl2

Package-Manager: portage-2.3.0 - Patrice Clement · gentoo

sci-mathematics/coq: Clean up old.

Package-Manager: portage-2.2.28 - Patrice Clement · gentoo

sci-mathematics/coq: Stable for amd64. Retroactively mark stable for the remaining arches using the ALLARCHES policy.

Package-Manager: portage-2.2.28 Gentoo-Bug: https://bugs.gentoo.org/586932 - Alexis Ballier · gentoo

Revert "sci-mathematics/coq: Remove := from || dep, #586304"

This reverts commit 84224f26f9c893299a487431e2ee005b1795f01c. This commit is wrong in several aspects: - Such changes should come with a revbump - Removing := deps causes packages not to be rebuilt on upgrades, causing barely understandable build failures when upgrading, later on. Thanks to this commit, people that have installed those packages will likely experience those failures with the upcoming ocaml 4.03 unmask. - This is a non maintainer commit where no discussion at all happened with the maintainers during the 3 days between bug report and mass commit. Such discussion could have prevented the above mentioned breakage. Proper fix is to drop the backward compatibility part of the || () dep. This fix was slowly moving forward whenever possible and noticed. Main blocker for this is bug #463018 which requires taking extra care for not breaking the stable tree nor needlessly preventing future stabilization of packages. - Michał Górny · gentoo

sci-mathematics/coq: Remove := from || dep, #586304 - Alexis Ballier · gentoo

sci-mathematics/coq: fix build with ocaml 4.03

Package-Manager: portage-2.2.28 Signed-off-by: Alexis Ballier <aballier@gentoo.org> - Alexis Ballier · gentoo

sci-mathematics/coq: bump to 8.5pl1

Package-Manager: portage-2.2.28 Signed-off-by: Alexis Ballier <aballier@gentoo.org> - Patrice Clement · gentoo

Merge remote-tracking branch 'github/pr/711'. - Alexis Ballier · gentoo

sci-mathematics/coq: bump to 8.5

Package-Manager: portage-2.2.27 Signed-off-by: Alexis Ballier <aballier@gentoo.org> - Alexis Ballier · gentoo

sci-mathematics/coq: remove old

Package-Manager: portage-2.2.24 Signed-off-by: Alexis Ballier <aballier@gentoo.org> - Agostino Sarubbo · gentoo

sci-mathematics/coq: ppc stable wrt bug #553322

Package-Manager: portage-2.2.20.1 RepoMan-Options: --include-arches="ppc" - Agostino Sarubbo · gentoo

sci-mathematics/coq: x86 stable wrt bug #553322

Package-Manager: portage-2.2.20.1 RepoMan-Options: --include-arches="x86" - Robin H. Johnson · gentoo

proj/gentoo: Initial commit

This commit represents a new era for Gentoo: Storing the gentoo-x86 tree in Git, as converted from CVS. This commit is the start of the NEW history. Any historical data is intended to be grafted onto this point. Creation process: 1. Take final CVS checkout snapshot 2. Remove ALL ChangeLog* files 3. Transform all Manifests to thin 4. Remove empty Manifests 5. Convert all stale $Header$/$Id$ CVS keywords to non-expanded Git $Id$ 5.1. Do not touch files with -kb/-ko keyword flags. Signed-off-by: Robin H. Johnson <robbat2@gentoo.org> X-Thanks: Alec Warner <antarus@gentoo.org> - did the GSoC 2006 migration tests X-Thanks: Robin H. Johnson <robbat2@gentoo.org> - infra guy, herding this project X-Thanks: Nguyen Thai Ngoc Duy <pclouds@gentoo.org> - Former Gentoo developer, wrote Git features for the migration X-Thanks: Brian Harring <ferringb@gentoo.org> - wrote much python to improve cvs2svn X-Thanks: Rich Freeman <rich0@gentoo.org> - validation scripts X-Thanks: Patrick Lauer <patrick@gentoo.org> - Gentoo dev, running new 2014 work in migration X-Thanks: Michał Górny <mgorny@gentoo.org> - scripts, QA, nagging X-Thanks: All of other Gentoo developers - many ideas and lots of paint on the bikeshed