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

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


Branch: CURRENT, Version: 8.10.2nb4, Package name: coq-8.10.2nb4, 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/gtk3] [graphics/adwaita-icon-theme] [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:

SHA1: ecdb79a8b4cd76912b39e037ef52545406e63799
RMD160: a3686508b97a98b668c91a513e73f88dff02af89
Filesize: 6077.09 KB

Version history: (Expand)


CVS history: (Expand)


   2020-06-02 10:25:05 by Adam Ciarcinski | Files touched by this commit (1689)
Log message:
Revbump for icu
   2020-05-24 01:45:45 by Makoto Fujiwara | Files touched by this commit (1)
Log message:
(lang/coq) Fix build: Remove no effective SUBST block
   2020-04-28 07:46:53 by Taylor R Campbell | Files touched by this commit (1)
Log message:
lang/coq: needs bash as tool

Otherwise build fails with:

   OCAMLOPT -o bin/coqide
   CHECK revision
   env: bash: No such file or directory
   gmake[1]: *** [Makefile.dev:34: revision] Error 127
   gmake[1]: Leaving directory '/tmp/pkgbuild/2020Q1/lang/coq/work/coq-8.10.2'
   gmake: *** [Makefile:179: submake] Error 2
   2020-03-10 23:11:24 by Thomas Klausner | Files touched by this commit (1681) | Package updated
Log message:
librsvg: update bl3.mk to remove libcroco in rust case

recursive bump for the dependency change
   2020-03-08 17:51:54 by Thomas Klausner | Files touched by this commit (2833)
Log message:
*: recursive bump for libffi
   2020-03-01 06:25:14 by David A. Holland | Files touched by this commit (2) | Package updated
Log message:
lang/coq now needs adwaita-icon-theme.

(without it the new coqide is missing things, and it seems to
specifically refer to adwaita-icon-theme by name)

Bump PKGREVISION to 1, since coqide is a default-on option.
   2020-01-24 16:54:49 by Jaap Boender | Files touched by this commit (6) | Package updated
Log message:
Updated lang/coq to version 8.10.2.

Changes include:
- native 63-bit machine integers;
- a new sort of definitionally proof-irrelevant propositons: SProp;
- private universes for opaque polymorphic constants;
- string notations and numeral notations;
- a new simplex-based proof engine for the tactics lia, nia, lra and nra;
- new introduction patterns for SSReflect;
- a tactic to rewrite under binders: under;
- easy input of non-ASCII symbols in CoqIDE, which now uses GTK3.

and many small improvements and bugfixes.
   2020-01-18 22:51:16 by Jonathan Perkin | Files touched by this commit (1836)
Log message:
*: Recursive revision bump for openssl 1.1.1.