Proof General

Proof General is distributed under the terms of the GNU General Public License, Version 2. See below for software pre-requisites for running Proof General.

Join the Proof General mailing list for announcements of new versions.

Quick installation instructions

The 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 to your .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 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 .emacs.

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 loading 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 byte-compile proof-general.

You can now open a Coq file (.v), an EasyCrypt file (.ec), a qrhl-tool file (.qrhl), or a PhoX file (.phx) to automatically load the corresponding major mode.

What you need to run Proof General

You need:

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!

Please report problems and send fixes so we can maintain support for latest versions.

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.