sci-mathematics / coq

Proof assistant written in O'Caml

Official package sites : http://coq.inria.fr/ ·

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.

v8.9.1-r1 :: 0 :: gentoo

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

v8.6.1-r1 :: 0 :: gentoo

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

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)

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-texlive / texlive-latexextra : TeXLive LaTeX additional packages

dev-texlive / texlive-latexrecommended : TeXLive LaTeX recommended 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

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 / lablgtk : Objective CAML interface for Gtk+2

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

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
697066
sci-mathematics/coq-8.10.2 version bump
Repository mirror & CI · gentoo
Merge updates from master
Michael Mair-Keimberger · gentoo
sci-mathematics/coq: fix eclass usage
Signed-off-by: Michael Mair-Keimberger <m.mairkeimberger@gmail.com> Closes: https://github.com/gentoo/gentoo/pull/13706 Signed-off-by: Aaron Bauman <bman@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Mikle Kolyada · gentoo
sci-mathematics/coq: forward keywords again (forgotten)
Package-Manager: Portage-2.3.76, Repoman-2.3.16 Signed-off-by: Mikle Kolyada <zlogene@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Mikle Kolyada · gentoo
sci-mathematics/coq: migrate from dev-tex/xcolor
Package-Manager: Portage-2.3.76, Repoman-2.3.16 Signed-off-by: Mikle Kolyada <zlogene@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Mark Wright · gentoo
sci-mathematics/coq: Bump to 8.9.1
Thanks to Han and Anton Kochkov for requesting the bump. Closes: https://bugs.gentoo.org/653864 Closes: https://bugs.gentoo.org/672038 Package-Manager: Portage-2.3.76, Repoman-2.3.17 Signed-off-by: Mark Wright <gienah@gentoo.org>
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