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

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

Branch: pkgsrc-2017Q4, Version: 8.7.0nb2, Package name: coq-8.7.0nb2, 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:
[x11/gtk2] [x11/ocaml-lablgtk] [lang/ocaml] [lang/python27] [lang/camlp5]

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

Package options: coqide

Master sites:

SHA1: b539e0ff6f2a6dd31bbe8856db152705f9a22a01
RMD160: 7e752473b27a2d1a0f95ea3eb258ffba5a5a8d4f
Filesize: 5497.27 KB

Version history: (Expand)