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.

You can join the Proof General mailing list for announcements of new versions. Developers and early-adopters may like to download a development release of Proof General. If you use an old version of a proof assistant and/or an old Emacs version, you may need to download one of the previous releases.

Proof General Version 3.4, released 29th August 2002.

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	NB: to build yourself use the tar file with `rpm -ta`.
individual files	browse individual files

The archives and RPM include almost everything: the generic code, specific code for the supported provers, installation instructions and documentation in Info and HTML formats. Documentation is available in other formats here here.

This version of Proof General has been tested with XEmacs 21.4 and GNU Emacs 21.2. It should work with some earlier versions of XEmacs, but we recommend using these Emacs versions for the most reliable results. Support on GNU Emacs is catching up, but XEmacs is still the better tested and more fully-featured environment. See below for links.

See the for more details, or check the file for a summary of changes since version 3.3.

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

What you need to run Proof General

To run Proof General, you must have:

Version 21.1 or 21.4 of XEmacs (this UK ftp mirror may help).
or version 21.2 of GNU Emacs.
Both Emacsen are available for a variety of platforms, including Unix variants, Windows 95/98/NT/2k, and Mac OS.
A proof assistant, for example: ; or ; ; .
(click on links for version details; see front page for other assistants).
Or write your own support for a new assistant!

There is also an optional component 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.
Versions of X-Symbol supported: version 3.4 (stable), and partially, version 4.4 (beta).
The stable version of X-Symbol only works with XEmacs on systems running X. The beta version also works with Emacs 21.4 (not yet available), and has limited support for XEmacs on Windows.

Compatibility across the multitude of Emacs versions is quite troublesome.
XEmacs has been better tested with Proof General than GNU Emacs.
Earlier versions of either variant may work with Proof General but are not officially supported because we cannot test backward compatibility widely. Please send us fixes rather than bug reports if you discover problems. Later versions of both Emacs variants should work with Proof General: if you discover problems, please check to see if they have been solved in a more recent development release before reporting.

Easy installation of Proof General

To use Proof General, simply unpack the sources with

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

X-Symbol is easy to install in XEmacs and configures itself automatically.

Simply download the binary package file, and do something like this to install in your home directory:

mkdir -p ~/.xemacs/xemacs-packages cd ~/.xemacs/xemacs-packages tar xpzf ../x-symbol-pkg.tar.gz

For GNU Emacs, you must remove the .elc files supplied, and add some code to your .emacs. See this page for details. More installation options are given in the the X-Symbol manual.