Proof General — Organize your proofs!
Proof General is a generic Emacs interface for proof assistants. The aim of the Proof General project is to provide a powerful, generic environment for using interactive proof assistants.
This is version 4.6-git of Proof General.
About Proof General branches
Two editions of Proof General are currently available:
- the (standard) REPL-based, stable version of Proof General, gathered in the master branch;
- the (unmaintained) Coq-specific, experimental version of Proof General, supporting asynchronous proof processing, gathered in the async branch.
Installing Proof General
Proof General requires GNU Emacs
25.2 or later.
Using NonGNU ELPA
MELPA is a repository of Emacs packages. Skip
this step if you already use MELPA. Otherwise, add the following to
.emacs and restart Emacs:
(require 'package) ;; (setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") ; see remark below (add-to-list 'package-archives '("melpa" . "https://melpa.org/packages/") t) (package-initialize)
Remark: If you have Emacs 26.1 (which is precisely
the packaged version in Debian 10),
you may get the error message
Failed to download 'melpa' archive
during the package refresh step. This is a known bug
which has been fixed in Emacs 26.3 and 27.1, while a simple workaround
consists in uncommenting the line
(setq gnutls-algorithm-priority "NORMAL:-VERS-TLS1.3") above in your
Note: If you switch to MELPA from a previously manually-installed
Proof General, make sure you removed the old versions of Proof General
from your Emacs context (by removing from your
.emacs the line
PG/generic/proof-site, or by uninstalling the proofgeneral
package provided by your OS package manager).
Then, run M-x package-refresh-contents RET followed by
M-x package-install RET proof-general RET to install and
You can now open a Coq file (
.v), an EasyCrypt file (
qrhl-tool file (
.qrhl), or a PhoX file (
.phx) to automatically
load the corresponding major mode.
Using Git (manual compilation procedure)
Remove old versions of Proof General, clone the PG repo from GitHub and byte-compile the sources:
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
Keeping Proof General up-to-date
As explained in the MELPA documentation, updating all MELPA packages in one go is as easy as typing M-x package-list-packages RET then r (refresh the package list), U (mark Upgradable packages), and x (execute the installs and deletions).
Assuming you have cloned the repo in
~/.emacs.d/lisp/PG, you would
have to run:
cd ~/.emacs.d/lisp/PG make clean git pull make
- INSTALL for installation details
- COPYING for license details
- COMPATIBILITY for version compatibility information
- FAQ.md for frequently asked questions
- coq/README for additional notes specific to the Coq prover
- https://proofgeneral.github.io/doc for online documentation of Proof General
- https://coq.zulipchat.com for chatting with PG maintainers and developers on the Zulip chat of Coq (in streams Proof General devs and Proof General users)
- https://coq.gitlab.io/zulip-archive for the corresponding public Zulip archive (read-only, no authentication required)
Supported proof assistants:
Proof General used to support other proof assistants, but those instances are no longer maintained nor available in the MELPA package:
- Experimental support of: Shell
- Obsolete instances: Demoisa
- Removed instances: Twelf, CCC, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98, LEGO, Isabelle
A few example proofs are included in each prover subdirectory.