Proof General
Proof General

Organize your proofs!

Proof General Version 4.2, 19th October 2012.

Proof General is distributed under the terms of the GNU General Public License, Version 2.
See below for software pre-requisites for running Proof General.

Download Proof General (for GNU Emacs 23.3 and later)

Join the Proof General mailing list for announcements of new versions.

Install Proof General

The Makefile helps with further installation. Read INSTALL for details.

Important note: The tar file contains compiled files for GNU Emacs 23.2. To be sure of compatibility with a different version of Emacs you may need to recompile. To delete and recompile, use the provided Makefile being sure to set EMACS to point to your Emacs executable, e.g.:

make clean; make compile EMACS=/Applications/
Proof General will also run using the interpreted code, at some speed penalty.

What you need to run Proof General

You need:

Compatibility across the multitude of platforms, provers and Emacs versions is very troublesome as invariably things break with Emacs or prover API changes and new bugs. You may have luck with older versions but there are no guarantees!

Please report problems and send fixes so we can maintain support for latest versions.

Other versions

Web pages by David Aspinall. Please report issues on PG trac.
Last modified 30 September 2015.