Before downloading Proof General, please
register.
The information collected will be used only to help a case for
support for Proof General in the future.
If you have already registered you do not need to do so again.
You may like to consider joining the Proof General mailing list.
You can download the latest stable release, ProofGeneral-2.1, or the latest pre-release, ProofGeneral-2.2pre990831. There is also a complete archive of the current pre-release for developers.
If you are using an older version of one of the proof assistants, you may wish to check the previous releases of Proof General.
This version of Proof General has been tested
with XEmacs 20.4, XEmacs 21 and FSF Emacs 20.3.
It supports Coq version 6.3, LEGO version 1.3.1 and
Isabelle version 99.
Check the file
for a summary of changes since version 2.0.
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.
To use Proof General, simply unpack the sources with
tar -xpzf ProofGeneral-2.1.tar.gz
(use gunzip 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.
This pre-release of Proof General may be buggy as new
features are added and experimented with.
Check the
file
for a summary of changes since the last stable version, and
the planned changes to come.
Please test with the current pre-release before reporting any problems
in a pre-release.
If you are interested in helping to develop the core of Proof General, we provide a complete archive of all the sources used to build the current Proof General pre-release. The difference from the working version distribution above is that we include:
Note: there are no pre-built documentation files in the developer's release, because developers should have the right tools!
You probably don't need to download this if you're only interested in hacking the Emacs lisp part of the program for a prover that is currently supported. But you may still like to check the latest .
We have a mailing list for developers, at
proofgeneral-devel@dcs.ed.ac.uk.
To subscribe (or unsubscribe), send a message to
majordomo@dcs.ed.ac.uk
with the words "subscribe proofgeneral-devel"
(or "unsubscribe proofgeneral-devel") in the message body.
If you are interested in developing the core of Proof General, we can make our CVS repository accessible to you. Please ask.
Please note that we do not support these old releases in any way.
This version of Proof General has been tested
with XEmacs 20.4 and FSF Emacs 20.2, 20.3.
It supports Coq version 6.2, LEGO version 1.3.1, and
Isabelle version 98-1.