./lang/coq, Theorem prover which extracts programs from proofs

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]


Branch: CURRENT, Version: 8.8.1, Package name: coq-8.8.1, Maintainer: jaapb

From http://coq.inria.fr/doc/tutorial.html:

Coq is a Proof Assistant for a Logical Framework known as the
Calculus of Inductive Constructions. It allows the interactive
construction of formal proofs, and also the manipulation of
functional programs consistently with their specifications.


Required to run:
[lang/ocaml] [x11/gtk2] [lang/camlp5] [lang/python27] [x11/ocaml-lablgtk] [math/ocaml-num]

Required to build:
[pkgtools/x11-links] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers] [x11/xorgproto]

Package options: coqide

Master sites:

SHA1: 7dd5e31f9dd3f80d6dabfb019d1f495244f61999
RMD160: 72b75b1d3a78c1a34b8bac86a0180b8bb677db14
Filesize: 5795.316 KB

Version history: (Expand)


CVS history: (Expand)


   2018-08-02 14:57:03 by Jaap Boender | Files touched by this commit (4) | Package updated
Log message:
Updated package lang/coq to version 8.8.1.

The list of improvements, additions, bugfixes and so on is quite large;
those interested can refer to the CHANGES file in the distribution.

The reference manual has been fully ported to Sphinx.
   2018-07-20 05:34:33 by Ryo ONODERA | Files touched by this commit (705)
Log message:
Recursive revbump from textproc/icu-62.1
   2018-06-16 12:25:51 by Mark Davies | Files touched by this commit (1)
Log message:
coq: always installs coqdoc.sty in tex tree.
   2018-04-18 00:29:53 by Thomas Klausner | Files touched by this commit (286)
Log message:
Add p11-kit to gnutls/bl3.mk and bump dependencies.
   2018-04-16 16:35:28 by Thomas Klausner | Files touched by this commit (1284)
Log message:
Recursive bump for new fribidi dependency in pango.
   2018-04-14 09:34:46 by Adam Ciarcinski | Files touched by this commit (681) | Package updated
Log message:
revbump after icu update
   2018-04-09 13:29:23 by Jaap Boender | Files touched by this commit (3) | Package updated
Log message:
Updated lang/coq to version 8.7.2.

This fixes a critical bug in the VM handling of universes, and adds
various other minor fixes and improvements.
   2018-03-12 12:18:01 by Thomas Klausner | Files touched by this commit (2155)
Log message:
Recursive bumps for fontconfig and libzip dependency changes.