What is Proof General?
Proof General is a generic front-end for proof assistants (also known as interactive theorem provers), based on the customizable text editor Emacs. Proof General has been developed at the LFCS in the University of Edinburgh with contributions from other sites. It is distributed under the conditions of the GNU General Public License. The manager and main developer is David Aspinall. Other contributors are listed below and in the AUTHORS file.
Proof General offers a full support for latest versions of the Coq proof assistant:
Coq Proof General,
by Healfdene Goguen, Patrick Loiseleur, David Aspinall, and Pierre Courtieu.
Proof General also supports previous versions of the following other proof assistants:
Isabelle Proof General,
for Isabelle (up to Isabelle2014)
by David Aspinall and Makarius.
PhoX Proof General,
by Christophe Raffalli, Paul Roziere and Jean-Roch Sotty.
- LEGO Proof General, for LEGO
- HOL Proof General, for HOL98/HOL4
- ACL2 Proof General, for ACL2
These instances may be incomplete or not work with the latest theorem prover versions.
Proof General is ready to be customized to new proof assistants. It can be very easy to get basic support working. Full documentation on configuration is provided. We welcome offers to support, extend and improve Proof General instances. Please get in touch if you plan major work.
If you are considering supporting (or implementing) a new prover, please read about the Proof General Kit architecture. The idea is that proof assistants should support PGIP, a uniform protocol for interaction, rather than use system-specific customization inside interfaces. The main research prototype using PGIP is an experimental Eclipse plugin, although Emacs Proof General supports some PGIP configuration.
Quick installation instructions
Remove old versions of Proof General, then download and install the new release from GitHub:
git clone https://github.com/ProofGeneral/PG ~/.emacs.d/lisp/PG cd ~/.emacs.d/lisp/PG make
Then add the following to your
;; 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/Emacs.app/Contents/MacOS/Emacs