Skip to content

Latest commit

 

History

History
142 lines (112 loc) · 6.11 KB

index.md

File metadata and controls

142 lines (112 loc) · 6.11 KB
layout title subtitle
page
Proof General
A generic Emacs interface for proof assistants.

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 v3.0 or later.

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.

{% comment %} Proof General offers a full support for latest versions of the Coq proof assistant:

  • Coq logo Coq Proof General, for Coq
    by Healfdene Goguen, Patrick Loiseleur, David Aspinall, and Pierre Courtieu.

Proof General also supports previous versions of the following other proof assistants:

These instances may be incomplete or not work with the latest theorem prover versions.

Proof General is ready to be customized to new proof assistants. It can be very easy to get basic support working. Full documentation on configuration is provided. We welcome offers to support, extend and improve Proof General instances. Please get in touch if you plan major work.

If you are considering supporting (or implementing) a new prover, please read about the Proof General Kit architecture. The idea is that proof assistants should support PGIP, a uniform protocol for interaction, rather than use system-specific customization inside interfaces. The main research prototype using PGIP is an experimental Eclipse plugin, although Emacs Proof General supports some PGIP configuration.

About Proof General branches

Two editions of Proof General are currently available:

  • the (legacy) REPL-based, stable version of Proof General, gathered in the master branch, and licensed under GPLv3+;
  • the (newest) Coq-specific, experimental version of Proof General, supporting asynchronous proof processing, gathered in the async branch, also licensed under GPLv3+.

{% endcomment %}

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 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 .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.

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 RET or M-x p-u-e-p RET;
  • the menu item Proof-General -> Upgrade ELPA packages... (screenshot below)

M-x proof-upgrade-elpa-packages RET

{% comment %} TODO: Add a link to the doc {% endcomment %}

Documentation

For more information about Proof General, see the README file on the GitHub repo, or browse the documentation page.