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 must have:

• Version 21.1 or later of XEmacs (this UK ftp mirror may help).
  or version 20.5 or later of the much poorer FSF GNU Emacs.
  Both Emacsen are available for a variety of platforms, including Unix variants and Windows 95/98/NT.
• One or more of the supported proof assistants. Or write your own support for a new assistant.
  See the for links to supported assistants.

There are also some optional components for using Proof General:

• For displaying logical and mathematical symbols, the excellent X-Symbol package.
  It's very easy to install. See here for installation notes.
  X-Symbol presently only works with XEmacs on systems running X.

All components mentioned above are distributed under the GPL license.

Proof General Version 3.1, released 23rd March 2000

Proof General is available as an archive and an RPM package.

• gzip'ed tar file: ,
  or the same thing in a zip 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 3.0.

Check the latest file (also ) before reporting problems. If you find a problem not already mentioned, please .

Easy installation

To use Proof General, simply unpack the sources with

tar xpzf ProofGeneral-3.1.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.

Easy installation of X-Symbol

Contrary to what you may expect from the documentation of X-Symbol, it's very 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