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

Proof General Version 4.1, 3rd October 2011.

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.

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.

Download Proof General

• ProofGeneral-4.1.tgz (1395k)
• browse individual files

Install Proof General

• Download and unpack the file:

  tar xpzf ProofGeneral-4.1.tar.gz

  Add this one line to your .emacs file, or inside its own file inside .emacs.d:

  (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. 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/Emacs.app/Contents/MacOS/Emacs

What you need to run Proof General

• A proof assistant, for example: Coq; Isabelle/Isar; LEGO; PhoX  (see links for versions).
• Version 23.2 or later of GNU Emacs
  Emacs is available for a huge variety of platforms, including Unix, Windows, and Mac OS. See the Emacs Wiki for advice and Proof General wiki for compatibility notes (please help extend them).

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

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