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) (let* ((no-ssl (and (memq system-type '(windows-nt ms-dos)) (not (gnutls-available-p)))) (proto (if no-ssl "http" "https"))) (add-to-list 'package-archives (cons "melpa" (concat proto "://melpa.org/packages/")) t)) (package-initialize)
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.
- A proof assistant, e.g.: Coq, EasyCrypt, PhoX (see links for versions).
- Version 24.3 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.