Before downloading Proof General, we'd be grateful if you
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 also like to consider joining the Proof General mailing list.
You can download the latest stable release or the latest pre-release.
This version of Proof General has been tested
with XEmacs 20.4 and FSF Emacs 20.2, 20.3
It 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.0.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 unstable as new
features are added and experimented with.
Check the
file for a summary of changes since the last stable version.
Please make test with the latest pre-release before reporting any problems
in a pre-release.
If you are interested in helping to develop the core of Proof General, you may like to download a complete archive of all the sources used to build the Proof General pre-release. The difference from the working version distribution above is that we include our low-level list of things to do, some developer's make files used to generate documentation files and the release itself from our CVS repository, some test files, sources for some of the images (in GIMP form), and the web pages.
You probably don't need to download this if you're only interested in hacking the Emacs lisp part of the program (but you may still like to check the latest ).
If there is any interest from developers, we could make our CVS repository open to anonymous cvs server access. Please ask.