Organize your proofs!  Home  Features  Download  Documentation  News  Screenshots  Development  About

Please register

Before downloading Proof General, please register. It's free, it only takes a moment.
Join the Proof General mailing list for announcements of new versions.

Stable: Proof General Version 3.7.1, 23rd July 2008.

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

• ProofGeneral-3.7.1.tgz (1975k)
• ProofGeneral-3.7.1-1.noarch.rpm (2152k)
  ProofGeneral-emacs-elc-3.7.1-1.noarch.rpm (396k) (compiled for GNU Emacs)
  ProofGeneral-xemacs-elc-3.7.1-1.noarch.rpm (385k) (compiled for XEmacs)
• browse individual files

Install Proof General

• RPMs. Install the RPM. Launch Proof General via the desktop menu or the proofgeneral command.
• Tarball. Unpack the file:

  tar xpzf ProofGeneral-3.7.1.tar.gz

  Add this one line to your .emacs or .xemacs/init.el file:

  (load-file "dir/generic/proof-site.el")

  Where dir is where you unpacked the sources. This makes Proof General available whenever you launch Emacs.

The Makefile helps with further installation. See the INSTALL file for details.

Important note for XEmacs users: The tar file contains compiled files for GNU Emacs. You should recompile before running PG. If you don't you will see obscure error messages. To delete and recompile, use the provided Makefile:

make clean; make compile EMACS=xemacs

What you need to run Proof General

• A proof assistant, for example: Coq; Isabelle/Isar; LEGO; PhoX  (see links for versions).
• Version 21.4.1, 22.1.1 or 23.X beta version of GNU Emacs
  or version 21.4.20 or 21.5.beta28 of XEmacs.
  GNU Emacs is the preferred option. Both Emacsen are available for a wide variety of platforms, including Unix, Windows, and Mac OS. See the Emacs Wiki for advice.

Compatibility across the multitude of platforms, provers and Emacs versions is very troublesome. Earlier Emacs versions may work but we cannot test backward compatibility widely and remove it eventually. Later versions should work but invariably things break with Emacs APIs changes and new bugs. Please report problems and send fixes so we can maintain support for latest versions.

Other versions

• Developers and early-adopters: check the interim development release. This version may also have compatibility fixes for new Emacs or prover versions.
• If you have an old version of a proof assistant and/or an old Emacs version, you may need a previous release.