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

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

Branch: pkgsrc-2015Q2, Version: 8.4pl6, Package name: coq-8.4pl6, 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] [lang/camlp5] [x11/ocaml-lablgtk] [x11/gtk2]

Required to build:
[x11/xextproto] [x11/inputproto] [x11/renderproto] [x11/compositeproto] [x11/xf86vidmodeproto] [x11/fixesproto4] [x11/glproto] [x11/randrproto] [x11/xf86driproto] [x11/xproto] [x11/xcb-proto] [x11/damageproto] [x11/dri2proto] [pkgtools/x11-links]

Package options: coqide

Master sites:

SHA1: c89525295659a805661ef91da24ecfb94e226953
RMD160: f57f6e5732d3977f3346dda2749f4b9628604018
Filesize: 4003.726 KB

Version history: (Expand)