Proof General
Proof General

Organize your proofs!

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 comes ready-to-go for these proof assistants:

Isabelle logo Isabelle Proof General for Isabelle
By David Aspinall and Makarius.
Coq logo Coq Proof General for Coq
By Healfdene Goguen, Patrick Loiseleur, David Aspinall, and Pierre Courtieu.
PhoX logo PhoX Proof General for PhoX
By Christophe Raffalli, Paul Roziere and Jean-Roch Sotty.

There are also unsupported or experimental instances of Proof General, including

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.


Web pages by David Aspinall. Please report issues on PG trac.
Last modified 11 October 2013.