Proof General

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.

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

Quick installation instructions

Remove old versions of Proof General, then download and install the new release from GitHub:

git clone ~/.emacs.d/lisp/PG
cd ~/.emacs.d/lisp/PG

Then add the following to your .emacs:

;; Open .v files with Proof General's Coq mode
(load "~/.emacs.d/lisp/PG/generic/proof-site")

If Proof General complains about a version mismatch, make sure that the shell’s emacs is indeed your usual Emacs. If not, run the Makefile again with an explicit path to Emacs. On macOS in particular you’ll probably need something like

make clean; make EMACS=/Applications/

For more information, see the README and INSTALL files on the GitHub repo.

What you need to run Proof General

You need:

Emacs is available for a huge variety of platforms, including Unix, Windows, and macOS. See the Emacs Wiki for advice.

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

If you have an old version of a proof assistant and/or an old Emacs version, you may need a previous release of Proof General: