Before downloading Proof General, please
register.
It only takes a moment.
The information collected will be used to help a case for
support for Proof General, and nothing else.
It is likely that development of Proof General will
finish very soon unless we can find new
resources.
If you have already registered you do not need to do so again.
You may like to consider joining the Proof General mailing list.
Developers and beta-testers may like to download a development release of Proof General. If you use an old version of a proof assistant, you may need to download one of the previous releases.
To run Proof General, you should have:
All these components are distributed under the GPL license.
Proof General is available in two formats:
Both the tarball and the RPM package include the generic elisp
code,
code for LEGO, Coq, and Isabelle, installation instructions
and documentation (in Info and HTML formats).
Documentation is available in other formats here . If you want to format the documentation yourself, you may like to download the .
This version of Proof General has been tested with XEmacs 21.1 and FSF Emacs 20.4. It supports Coq version 6.3, LEGO version 1.3.1 and Isabelle99. Check the file for a summary of changes since version 2.1.
To use Proof General, simply unpack the sources with
tar -xpzf ProofGeneral-3.0.tar.gz
(use gunzip first in place of -z if you don't have GNU tar),
and then add this one line to your .emacs file:
(load-file "directory/generic/proof-site.el")
Where directory is the directory in which you unpacked
the sources.
If you use the RPM package, directory is
/usr/share/emacs/ProofGeneral
Further customization is possible via the Customize menus in
Emacs.
See the
file in the distribution for more details.
Please send us any problems, suggestions, or patches.