[Prev][Next][Index][Thread]
Coq V5.10 Release
Coq V5.10 Release
This is the announcement for the release of the Coq Proof Assistant,
Version 5.10.
It may be taken as usual from machine ftp.inria.fr, directory
INRIA/coq/V5.10, archive V5.10.tar.z and README file.
For users who are already using one of the beta-test versions of V5.10,
this final release has improved documentation, streamlining of tactics
(Some adaptation of your scripts may be necessary because the names
of inversion tactics have changed), and compressed theory files (.vo)
which keep the size of the installation much smaller and are uniform
across architectures. This substantial improvement necessitates
however the installation of the latest release of Caml Light; see
WARNING below.
For users who are still using our old release V5.8, it is high time to
switch to this new system, which has been completely rebuilt,
authorizes mutually recursive inductive families, compiled theory
modules, extensible parsers and pretty-printers, user-programmable
tactics, synthesis of implicit type arguments, and many other goodies.
The distribution also includes numerous new user-contributed
libraries.
The current release works under most modern UNIX platforms.
A specialised interface with the Centaur environment, called CTCoq, is
under completion in Sophia-Antipolis and should be available soon
in beta-test.
A Macintosh version will be available next Fall.
* WARNING: In order to install Coq V5.10 you NEED to install the latest
* release of Caml Light 0.7, available by anonymous ftp on
* ftp.inria.fr, in INRIA/lang/caml-light. You also need to
* install the Caml Light contribution `libunix'.
As always, anomaly reports to coq@pauillac.inria.fr
and general questions to coq-club@pauillac.inria.fr
We apologize for possible multiple copies of this message.
The Coq team