[Prev][Next][Index][Thread]
Coq distribution
[------ The Types Forum ------- http://www.dcs.gla.ac.uk/~types ------]
Hello,
We are glad to announce the release of version 5.10.15 of the Coq
Proof Assistant for the Calculus of Inductive Constructions. This release
includes various changes in the code and libraries, which are
described more precisely below. The documentation has also been
updated.
Coq V5.10.15 comes in two flavors: the regular Coq, and a new, fully
up-to-date and compatible distribution of Ct-Coq (i.e. Coq with a
sophisticated graphical user-interface).
The Coq distribution is available at Rocquencourt and in Lyon:
ftp://ftp.ens-lyon.fr/pub/LIP/COQ/V5.10/
ftp://ftp.inria.fr/INRIA/coq/V5.10/
or through:
http://pauillac.inria.fr/coq/systeme_coq-eng.html
As usual, get the README files first, for instructions.
Because the organization of some files and directories has changed, we
will not provide any patches for update.
Ct-coq is available in Sophia-Antipolis:
http://www.inria.fr/croap/ctcoq-eng.html
Below, you will find a summary of the main changes with respect to the
previous version. It is followed by a description of the new Ct-Coq by
Janet Bertot.
This concerns the UNIX version of V5.10.15.
For the Microsoft-Windows as well as the Macintosh version
see below.
As usual, you might send problems, bug reports, remarks about the
installation to
coq@pauillac.inria.fr
and more general questions about the coq system to the mailing list
coq-club@pauillac.inria.fr
questions specific to the Ct-Coq interface should be addressed to
ctcoq-request@sophia.inria.fr
Enjoy!
for the Coq team,
Gerard Huet
(********************************************************************)
(* Main changes between V5.10.14 (july 95) and V5.10.15 (feb 96) *)
(********************************************************************)
* Changes in code:
- (x:A)(y:A)B is now printed as (x,y:A), same for abstraction.
- Many internal bugs have been fixed.
- New commands Set/Unset Undo to control the number of possible undo
Set/Unset Hyps_limit to control the number of printed hypotheses
* Changes in tactics:
- New tactics Rewrite .. in
- More inversion tactics (see the reference manual)
1) The tactics (Derive) Inversion and (Derive) Inversion_clear have been
extended to (co)inductive types of sort Set and Type.
2) New tactics are available for deriving inversion lemmas on different
sorts and performing simple dependent inversion.
- The tactic Rewrite uses now the lemmas eq_ind_r and no more the symmetry.
* The reference manual has been updated.
* Changes in librairies :
- Some Hint/Immediate have been added in the basic theories.
- More results on classical logic (previously in INIT/Classical)
are now in the directory theories/LOGIC
- theories/RELATIONS contains basic definitions and properties on relations
while theories/RELATIONS/WELLFOUNDED establishes results on well-foundness.
- Changes in the development theories/ALGEBRA
- A new directory theories/SORTING has been added.
* New contributions :
Bordeaux/Additions
Lannion/polycont
Marseille/CCS
Paris/ZF
Sophia-Antipolis/HARDWARE/ADDER
Sophia-Antipolis/HARDWARE/BLOCK
Sophia-Antipolis/HARDWARE/GENE
Sophia-Antipolis/HARDWARE/MULTIPLIER
Sophia-Antipolis/MATHS/DOMAINS
Sophia-Antipolis/MATHS/GEOMETRY
Sophia-Antipolis/MATHS/GROUPS
Sophia-Antipolis/MATHS/Z
(*************************************************************************)
Subject: CtCoq (running with Coq v5.10.15 -- archive of 15 February 1996)
CtCoq provides a working environment for the Coq theorem prover,
via a graphical user interface. The X interface and Coq run as
separate processes and the interface has multiple fonts and colors
for displaying commands, it provides support for constructing commands
and formulae, has an experimental textual presentation of proofs, and,
using a technique called "Proof by Pointing", allows the user to direct
the proof by clicking with the mouse on various parts of the subgoals.
To find out more, visit our www page listed below.
The CtCoq user interface version "beta2", which runs with Coq version
5.10.15, is now available for both sun4OS4 and DecAlpha workstations.
---------------
New features in this version of CtCoq include:
o Comments are handled partially, i.e., when associated to a toplevel
command. (NB: This works only if you have "perl" on your system.)
o The "Discard" interface has been extended so that the Discard button
may be used for undoing commands *other* than proof steps. Thus, one
can discard theorems, axioms, or definitions. Still certain commands
(such as Require or Hint) cannot be undone.
o Parsing of subexpressions in the Command window is no longer limited
to commands, tactics, or formulae, allowing for finer text editing.
o Proof by Pointing behavior has been improved. The generated script is
more natural for Coq users.
o Menus used in guided editing are now complete (updated for V5.10.15
syntax). Transformations between different variants of a command
or tactic are provided. The presentation of the hierarchical menus
has changed, hopefully making guided editing more agreeable.
o The auto-saving capability has been improved, making it less disruptive.
---------------
The www page is:
http://www.inria.fr/croap/ctcoq/ctcoq-eng.html
The direct ftp route is:
The machine: babar.inria.fr (138.96.24.21)
The directory: pub/centaur/ctcoq-beta2
Follow the README instructions to obtain all that you need.
NB: if you obtain the system directly by ftp you should send
mail to ctcoq-request@sophia.inria.fr indicating for which
architecture(s) you wish to run the CtCoq system.
For all and any questions/problems please send mail to:
ctcoq-request@sophia.inria.fr
---------------
HOT ! Last minute ! HOT
---------------
The latest version 5.10.15 of Coq is now also available for PC's running
Microsoft Windows 95 or Windows NT, as well as for the Apple Macintosh
(with 68k or PPC architecture).
These releases are as close as possible to the UNIX versions. There
can be found in the usual ftp directory in Rocquencourt:
ftp://ftp.inria.fr/pub/INRIA/coq/V5.10/CoqWin/
and
ftp://ftp.inria.fr/pub/INRIA/coq/V5.10/CoqMac/
Both distributions do not contain the user's contributions. You might
however use and add the corresponding files from the unix distrib.
As usual, please send any comments, bug reports, questions, to
coq@pauillac.inria.fr
The Windows version is due to Henri Laulhere; the Macintosh one to
Cesar Munoz.
--------------------------------------------------------------
Coming soon: arithmetic decision tactics.
--------------------------------------------------------------