Join the Proof General mailing list for announcements of new versions.
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 know 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 (
a qrhl-tool file (
.qrhl), or a PhoX file (
to automatically load the corresponding major mode.
- A proof assistant, e.g.: Coq, EasyCrypt, qrhl-tool, PhoX (see links for versions).
- Version 25.1 or later of GNU Emacs.
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!
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).
For more information, see the README file on the GitHub repo.