Please register

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 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. 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.

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.

Please check the for using Proof General.

What you need to run Proof General

To run Proof General, you should have:

• Version 20.4 or later (21.1 is recommended) of XEmacs (this UK ftp mirror may help).
  or version 20.2 or later (20.4 recommended) of the much poorer FSF GNU Emacs.
  Both Emacsen are available for a variety of platforms, including Unix variants and NT.
• For displaying logical and mathematical symbols, the excellent X-Symbol package.
  X-Symbol presently only works with XEmacs. Its use with Proof General is optional.
• For FSF Emacs, a version of func-menu.el to get .
  I can't find a version of this that works with current FSF Emacs releases. I'd be grateful for a pointer to one. (Alternatively, the package imenu.el may be a suitable replacement, and it ships with both Emacs. Perhaps somebody could contribute patches to use that instead of func-menu).
  Proof General works fine without this feature.

All these components are distributed under the GPL license.

Proof General Version 3.0, released 26th November 1999

Proof General is available in two formats:

• gzip'ed tar file:
• Linux RPM package:
  You probably don't need the .

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.

Easy installation!

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.