Before downloading Proof General, please register. It's free, it only takes a moment. If you have already registered you do not need to do so again. The statistics collected from registrations are used to help make a case for support for Proof General, and nothing else. It is likely that development of Proof General will finish soon unless we find new resources. As a courtesy, we do not make registration compulsory and I can tell from the server logs that the majority of people downloading do not register. But if you don't register now, please consider returning to register later if you find Proof General interesting or useful. If you don't want to fill the form, please send an email directly or even a paper letter to the LFCS. And if you can offer to help resource the development of Proof General in some way, please contact us (quickly!).
You may like to join 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.
Proof General is distributed under the terms of
the
.
See below for software pre-requisites for running Proof General.
Proof General is available as an archive and an RPM package.
| gzip'ed tar file | |
| zip file | |
| RPM package | |
| individual files | browse individual files |
Both the tarball and the RPM package include the generic elisp code, code for the supported provers, installation instructions and documentation in Info and HTML formats. Documentation is available in other formats here here. If you want to format the documentation yourself, you may like to download the . Note that we don't ship an SRPM now, since you can build the RPM directly from the source tarball using rpm -ta.
This version of Proof General has been tested with XEmacs 21.4 and (briefly with) GNU Emacs 20.7. It supports earlier versions of both Emacsen, but we recommend using these versions. This version of Proof General does not support GNU Emacs 21.x, please try out a development release instead.
Check the file for >a summary of changes since version 3.2.
Check the latest file (also ) before reporting problems. If you find a problem not already mentioned, please .
To run Proof General, you must have:
There are also some optional components for using Proof General:
All components mentioned above are distributed under the GPL license.
To use Proof General, simply unpack the sources with
tar xpzf ProofGeneral-3.3.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
If you're using Windows, then download the zip file.
Use a zip file utility to unpack it somewhere, for example
c:\\ProofGeneral
Further customization is possible via the Customize menus in
Emacs.
See the
file in the distribution for more details.
X-Symbol is easy to install and configures itself automatically.
Simply download the binary package file, and do something like this to install in your home directory:
mkdir -p ~/.xemacs
cd ~/.xemacs
tar xpzf ../x-symbol-pkg.tar.gz
NB: if you have version 21.x of XEmacs, you may need to install x-symbol inside a subdirectory ~/.xemacs/xemacs-packages instead of ~/.xemacs.