What is Proof General?
Proof General is a generic interface for proof assistants (also known as interactive theorem provers), based on the extensible, customizable text editor Emacs.
Proof General has been developed at the LFCS in the University of Edinburgh, mainly by David Aspinall, with contributions from other sites. It is distributed under the conditions of the GNU General Public License.
The authors of Proof General are listed in the AUTHORS file. Many more people have also contributed. Please see the CREDITS section in the manual for a more complete list of contributors.
Quick installation instructions
master version of Proof General is available on
MELPA, a repository of Emacs packages.
Skip this step if you already use MELPA. Otherwise, add the following
.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' archiveduring the package refresh step. This is a known bug (debbug #34341) 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
.emacsthe line loading
PG/generic/proof-site, or by uninstalling the proofgeneral package provided by your OS package manager).
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 (
.ec), or a
PhoX file (
.phx) to automatically load the corresponding major mode.
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).
Alternatively, you can use one of the following shortcuts:
M-x proof-upgrade-elpa-packages RETor
M-x p-u-e-p RET;
- the menu item
Proof-General -> Upgrade ELPA packages...(screenshot below)