This version comes with many improvements of existing
features, especially regarding the tactics, the module system,
extraction, the type classes, the program command, libraries,
coqdoc. It also includes a new tactic (nsatz, standing for
Hilbert's NullStellensatz, that extends ring to systems of polynomial
equations) and a few new libraries (a certification
of mergesort, a new library of finite sets with computational
and logical contents separated). For a full log of changes,
see the file
CHANGES.
Coq 8.3 is not entirely upward compatible with 8.2. The major incompatibilities can be easily treated by using the new -compat 8.2 option or by setting/unsetting
adequate options. See the file
COMPATIBILITY for
details and migration recommendations.
| Sources | ||
| coq-8.3pl4.tar.gz | 3.7 MB | |
| Binaries | ||
 Windows |
coq-8.3pl3-win-0.exe (bundled with CoqIDE) | 49 MB |
 MacOS |
coq-8.3pl4-macosx.dmg | 61 MB |
| coqide-8.3pl4-macosx.dmg (Coq bundled with CoqIDE interface) | 78 MB | |
| The packages require MacOS ≥ 10.5 | ||
| Documentation | ||
| Tutorial.pdf | 0.2 MB | |
| Reference-Manual.pdf | 1.5 MB | |
dmg packages, use the Coq bug tracker.
This is the previous stable release of the Coq system (see the detailed description and the full list of changes).
| Sources | ||
| coq-8.2pl3.tar.gz | 3.5 MB | |
| Binaries | ||
| Windows
|
coq-8.2pl2-win-1.exe | 138 MB |
| MacOS
|
coq-8.2pl3-macosx.dmg | 29 MB |
| coqide-8.2pl3-macosx.dmg (Coq bundled with CoqIDE interface) | 49 MB | |
| These binary packages should work for Mac OS 10.5, 10.6 and 10.7. If you wish to compile your own version of Coq, you may follow these instructions to build a MacOS package using MacPorts | ||
| Documentation | ||
| Tutorial.pdf | 0.2 MB | |
| Reference-Manual.pdf | 2 MB | |
The development version of Coq is browsable and downloadable from our Subversion repository using command: svn checkout svn://scm.gforge.inria.fr/svn/coq/trunk. The daily level of stability of this version (and of the bug-fix branches) can be observed at the coq-bench site or by subscribing to the coq-bench mailing list.
Most of the previous version of Coq are available here for the most recent ones and here for the older ones.
When compiled with Objective Caml 3.11 (which is the case of the Windows and MacOS packages we release), Coq supports dynamic loading of extensions. The following extensions are known to work as plugins:
- The small scale reflection package (ssreflect) contains the robust and compact tactic language and libraries that were started for supporting the full formalization of the 4 color theorem and that now serves, among other applications, as support for the ongoing formalization of the odd order theorem in group theory. (*)
- The rewriting modulo associativity and commutativity plugin (AAC_tactics). (*)
- The classical extraction module provides extraction of programs from classical proofs in Prop.
- The rippling plugin for automation of inductive arguments.
- The descente infinie plugin for delayed inference of the induction hypothesis needed in well-founded induction. (*)
Note: Objective Caml ≥ 3.11.1 is required for building plugins on MacOS 10.5. (*) above means that the plugin is submitted to the user contributions and planned to be kept compatible with the new releases of Coq to come.
Consider also the experimental Coq Modulo Theories (CoqMT) which modifies Coq with primitive support for user-defined first-order equational theories (starting with linear arithmetic).