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

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


Branch: CURRENT, Version: 8.7.1nb1, Package name: coq-8.7.1nb1, 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/compositeproto] [x11/glproto] [x11/renderproto] [x11/xproto] [x11/xf86vidmodeproto] [x11/recordproto] [x11/xf86driproto] [x11/damageproto] [x11/inputproto] [x11/xextproto] [x11/randrproto] [x11/dri2proto] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers]

Package options: coqide

Master sites:

SHA1: ea4c4bbed3dc1a5550bbb7e2923ed751f9ad2be6
RMD160: 405d24ba9f0eda5b72e8bd0ed0778390cc444bf0
Filesize: 5538.213 KB

Version history: (Expand)


CVS history: (Expand)


   2018-01-28 21:11:10 by Thomas Klausner | Files touched by this commit (462) | Package updated
Log message:
Bump PKGREVISION for gdbm shlib major bump
   2018-01-22 12:54:43 by Jaap Boender | Files touched by this commit (1)
Log message:
Corrected PLIST for lang/coq
   2018-01-10 17:26:53 by Jaap Boender | Files touched by this commit (6) | Package updated
Log message:
Updated package lang/coq to version 8.7.1.

This is a compatibility release with OCaml 4.06.0. It also contains many
bugfixes, documentation improvements and user message improvements.
   2018-01-01 23:30:04 by Roland Illig | Files touched by this commit (537)
Log message:
Sort PLIST files.

Unsorted entries in PLIST files have generated a pkglint warning for at
least 12 years. Somewhat more recently, pkglint has learned to sort
PLIST files automatically. Since pkglint 5.4.23, the sorting is only
done in obvious, simple cases. These have been applied by running:

  pkglint -Cnone,PLIST -Wnone,plist-sort -r -F
   2017-11-30 17:45:43 by Adam Ciarcinski | Files touched by this commit (654) | Package updated
Log message:
Revbump after textproc/icu update
   2017-11-23 18:20:22 by Thomas Klausner | Files touched by this commit (556)
Log message:
recursive bump for libxkbcommon removal from at-spi2-core
   2017-11-03 12:20:28 by Jaap Boender | Files touched by this commit (5) | Package updated
Log message:
Updated lang/coq to version 8.7.0.

Includes many improvements and bugfixes (none that seem to be breaking
backwards compatibility though), see the CHANGELOG.
For packaging:
- camlp4 support removed, package now uses camlp5 exclusively
- fix for PR pkg/52651
   2017-09-18 11:53:40 by Maya Rashish | Files touched by this commit (676)
Log message:
revbump for requiring ICU 59.x