Path to this page:
NOTICE: This package has been removed from pkgsrc./
wip/coq,
Theorem prover which extracts programs from proofs
Branch: CURRENT,
Version: 8.11.0,
Package name: coq-8.11.0,
Maintainer: jaapbFrom 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/gtk3] [
math/ocaml-num] [
lang/python37] [
x11/ocaml-lablgtk3]
Required to build:[
pkgtools/x11-links] [
x11/xcb-proto] [
x11/fixesproto4] [
pkgtools/cwrappers] [
x11/xorgproto]
Package options: coqide
Master sites:
RMD160: e3ac2f67e9db3351bdf68f38609142999bcd3bab
Filesize: 6401.748 KB
Version history: (Expand)
- (2022-06-04) Package deleted from pkgsrc
- (2020-09-29) Package has been reborn
- (2020-09-29) Package deleted from pkgsrc
- (2020-01-29) Updated to version: coq-8.11.0
- (2020-01-24) Updated to version: coq-8.11+beta1
- (2020-01-02) Package has been reborn
CVS history: (Expand)
2012-12-02 21:35:28 by othyro | Files touched by this commit (5) | |
Log message:
Archive version of lang/coq. The version in HEAD now includes the doc
option, the only real difference between the two packages. Removing. Please
use lang/coq from now on.
|
2012-09-24 20:26:51 by Aleksej Saushev | Files touched by this commit (116) |
Log message:
Drop superfluous PKG_DESTDIR_SUPPORT, "user-destdir" is default these days.
Mark packages that don't or might probably not have staged installation.
|
2010-06-14 00:46:55 by Thomas Klausner | Files touched by this commit (271) |
Log message:
Bump PKGREVISION for libpng shlib name change.
Also add some patches to remove use of deprecated symbols and fix other
problems when looking for or compiling against libpng-1.4.x.
|
2010-03-11 15:37:20 by othyro | Files touched by this commit (5) | |
Log message:
Import coq-8.2pl1 as wip/coq.
Coq is a formal proof management system. It provides a formal language to write
mathematical definitions, executable algorithms and theorems together with an
environment for semi-interactive development of machine-checked proofs.
|