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

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


Branch: CURRENT, Version: 8.7.0, Package name: coq-8.7.0, 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/python27] [x11/ocaml-lablgtk]

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: b539e0ff6f2a6dd31bbe8856db152705f9a22a01
RMD160: 7e752473b27a2d1a0f95ea3eb258ffba5a5a8d4f
Filesize: 5497.27 KB

Version history: (Expand)


CVS history: (Expand)


   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
   2017-09-08 19:19:01 by Jaap Boender | Files touched by this commit (3) | Package updated
Log message:
Updated package to latest version, 8.6.1. Changes include:

- Fix #5380: Default colors for CoqIDE are actually applied.
- Fix plugin warnings
- Document named evars (including Show ident)
- Fix Bug #5574, document function scope
- Adding a test case as requested in bug 5205.
- Fix Bug #5568, no dup notation warnings on repeated module imports
- Fix documentation of Typeclasses eauto :=
- Refactor documentation of records.
- Protecting from warnings while compiling 8.6
- Fixing an inconsistency between configure and configure.ml
- Add test-suite checks for coqchk with constraints
- Fix bug #5019 (looping zify on dependent types)
- Fix bug 5550: "typeclasses eauto with" does not work with section \ 
variables.
- Bug 5546, qualify datatype constructors when needed in Show Match
- Bug #5535, test for Show with -emacs
- Fix bug #5486, don't reverse ids in tuples
- Fixing #5522 (anomaly with free vars of pat)
- Fix bug #5526, don't check for nonlinearity in notation if printing only
- Fix bug #5255
- Fix bug #3659: -time should understand multibyte encodings.
- FIx bug #5300: Anomaly: Uncaught exception Not_found" in "Print \ 
Assumptions".
- Fix outdated description in RefMan.
- Repairing `Set Rewriting Schemes`
- Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
- Fix description of command-line arguments for Add (Rec) LoadPath
- Fix bug #5377: @? patterns broken.
- add XML protocol doc
- Fix anomaly when doing [all:Check _.] during a proof.
- Correction of bug #4306
- Fix #5435: [Eval native_compute in] raises anomaly.
- Instances should obey universe binders even when defined by tactics.
- Intern names bound in match patterns
- funind: Ignore missing info for current function
- Do not typecheck twice the type of opaque constants.
- show unused intro pattern warning
- [future] Be eager when "chaining" already resolved future values.
- Opaque side effects
- Fix #5132: coq_makefile generates incorrect install goal
- Run non-tactic comands without resilient_command
- Univs: fix bug #5365, generation of u+k <= v constraints
- make `emit' tail recursive
- Don't require printing-only notation to be productive
- Fix the way setoid_rewrite handles bindings.
- Fix for bug 5244 - set printing width ignored when given enough space
- Fix bug 4969, autoapply was not tagging shelved subgoals correctly
   2017-07-11 16:19:23 by Jaap Boender | Files touched by this commit (71)
Log message:
Revbump associated with ocaml-4.04.2
   2017-04-22 23:04:05 by Adam Ciarcinski | Files touched by this commit (670) | Package updated
Log message:
Revbump after icu update
   2017-02-12 07:26:18 by Ryo ONODERA | Files touched by this commit (1451)
Log message:
Recursive revbump from fonts/harfbuzz
   2017-02-06 14:56:14 by Thomas Klausner | Files touched by this commit (1452)
Log message:
Recursive bump for harfbuzz's new graphite2 dependency.
   2017-01-12 10:11:27 by Jaap Boender | Files touched by this commit (1)
Log message:
Added dependency on camlp4