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. --------------------------------------------------------------