1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
Coq version 8.0 is a major evolution of the Coq system. The final
version of is now coming out.
Coq version 8.0 features
------------------------
First, the logical system of Coq version 8.0 has been simplified by
removing the impredicativity of the sort Set. This allows to benefit
of the principle of description in formalisations of classical
mathematics without leading to logical inconsistencies. Impredicativity
remains available as an option for experimented users still wishing to
require this feature.
Secondly, Coq version 8.0 comes with a completely new syntax of
terms, and a slightly revised syntax for tactics and commands. Besides
a better uniformity and a simplification of the syntax, the purpose is
to allow the use of high-level comforts, such as implicit types in
quantification and notations for standard arithmetical notions
(e.g. +, *, <, <=) without conflicts with the rest of the syntax. A new
notion of "interpretation scopes" allows also to reuse the same
notations in different contexts of formalisation (e.g. +, * are valid
on nat, Z, R, types, etc).
Thirdly, the standard library has been revised and simplified. There
is now only one equality "=" and one existential quantification valid
on all types. The type "R" is now in Set and the library on "Z" has
been re-organised. The basic notions from the initial state now have
implicit arguments.
Coq version 8.0 comes with a smart and robust comment-preserving
automatic translator from old to new syntax. A translation package
with a documentation of the new syntax accompanies the distribution.
Coq version 8.0 brings also a new automation tactic for first-order
statements and various improvements of existing tactics.
Last but not the least, Coq version 8.0 comes with CoqIde, a new
integrated gtk-based user interface in the style of ProofGeneral.
New book on Coq
---------------
For the first time, a comprehensive textbook on the art of Coq,
accompanies the distribution of Coq. We are extremely thankful to the
authors, Yves Bertot and Pierre Casteran, for this essential
contribution to the development of Coq. This 470-pages book comes with
about 200 exercises and their solution in Coq. Details are on
http://www.labri.fr/~casteran/CoqArt.
Changes wrt Coq version 8.0 beta
--------------------------------
The main change wrt to Coq 8.0 beta is a different semantics for the
if-then-else construction, which may lead to the need of rerunning the
translator, or to modify a few lines by hand. The other modifications
mainly consist in extensions or upgrading (a few tactics and commands,
XML exportation of theories and proof scripts, coqdoc compatibility)
and bug fixes. See file Changes.html on Coq web site for details.
Downloading and documentation
-----------------------------
The sources of Coq V8.0, including its integrated development
environment, are available from http://coq.inria.fr/ and
ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0/. The translation package
coq-8.0-translator.tar.gz is available separately at the same
location.
Please refer to the accompanying document CHANGES or the location
ftp://ftp.inria.fr/INRIA/LogiCal/coq/V8.0/doc/Changes.html for a
full list of changes including sources of incompatibilities.
The documentation of Coq V8.0 is available in postscript, pdf and
html format.
Users are kindly invited to report bugs at http://coq.inria.fr/bin/coq-bugs
and to mail Coq-Club@pauillac.inria.fr for general questions or remarks.
Note that you can now choose your personal options at
http://pauillac.inria.fr/mailman/listinfo/coq-club and consult the
mails archive at http://pauillac.inria.fr/pipermail/coq-club.
The Coq development team
|
