NonGNU ELPA - proof-general


A generic Emacs interface for proof assistants
proof-general-4.5.tar, 2022-Jul-13, 3.32 MiB
Browse ELPA's repository
CGit or Gitweb

To install this package, run in Emacs:

M-x package-install RET proof-general RET

Full description

Proof General is a generic Emacs interface for proof assistants
(also known as interactive theorem provers).

It is supplied ready to use for the proof assistants Coq,
EasyCrypt, qrhl, and PhoX.

See for installation instructions
and online documentation.  Or browse the accompanying info manual:
(info-display-manual "ProofGeneral")

Regarding the Coq proof assistant, you may be interested in the
company-coq extension of ProofGeneral (also available in MELPA).


-*- outline -*-  

This is a summary of main changes.  For details, please see
the Git ChangeLog, the GitHub repo

* Changes of Proof General 4.5 from Proof General 4.4

** Generic changes
*** License changed to GPLv3+
*** Remove support for the following systems:
Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.

*** require GNU Emacs 25.2 or later

The current policy aims at supporting multiple Emacs versions,
including those available in distributions Debian Stable
( and Ubuntu LTS
(, until their End-Of-Support (see
also Support for Emacs 25 will
be dropped in April 2023 when Ubuntu Bionic reaches end of
standard support.

*** new command and menu item to easily upgrade all packages
    - To upgrade all ELPA packages (including ProofGeneral if it was
      installed via MELPA), do "M-x proof-upgrade-elpa-packages RET"
      or use the "Proof-General > Upgrade ELPA packages..." menu item

*** bug fixes
    - Using query-replace (or replace-string) in the processed region
      doesn't wrongly jump to the first match anymore.
    - cheat face (admit etc) now visible when locked.

*** remove key-binding for proof-electric-terminator-toggle
    - The default key-binding for proof-electric-terminator-toggle
      (C-c .) was too easy to enter by mistake. And it was not that
      useful as we can expect users to configure electric-terminator
      once and for all. Hence the removal of this default key-binding.

*** add another (fallback) key-binding for proof-goto-point
    - The default key-binding for proof-goto-point (C-c <C-return>)
      was not available in TTYs. Now, this function can also be run
      with "C-c RET", which happens to be automatically trigerred if
      we type "C-c <C-return>" in a TTY.

*** new proof-priority-action-list
    Similar to proof-action-list, but holding actions that need
    to go to the proof assistant at the next opportunity.

** Qrhl-tool

   Support for qrhl-tool theorem prover has been added by Dominique
   - Initial pull request:
   - Qrhl-tool web site:

** EasyCrypt

   Support for EasyCrypt has been added.

** Coq changes

*** fix highlighting issues for ssr tactics ending with colon

    Now, { exact: term. } will always be correctly highlighted.

    However, only (forall {T: Type}, Type) will be highlighted,
    unlike term (forall { T: Type }, Type) that has a spurious space.

    Also in (forall [T: Type], Type), variable T is now highlighted.

*** new menu Coq -> Auto Compilation for all background compilation options

*** support for 8.11 vos and vok compilation

    See menu Coq -> Auto Compilation -> vos compilation, option
    coq-compile-vos and subsection "11.3.3 Quick and inconsistent
    compilation" in the Coq reference manual.

*** support for 8.5 quick compilation

    See new menu Coq -> Auto Compilation -> Quick compilation.
    Select "no quick" as long as you have not switched to "Proof
    using" to compile without -quick. Select "quick no vio2vo" to
    use -quick without vio2vo (and guess what "quick and vio2vo"
    means ;-), select "ensure vo" to ensure a sound development.
    Quick compilation is only supported for Coq < 8.11. See the
    option `coq-compile-quick' or the subsection "11.3.3 Quick
    and inconsistent compilation" in the Coq reference manual.

*** new option coq-compile-keep-going (in menu Coq -> Auto Compilation)

    Similar to ``make -k'', with this option enabled, background
    compilation does not stop at the first error but rather
    continues as far as possible.

*** Automatic insertion of "Proof using" annotations.

    PG now supports the "Suggest Proof Using" by inserting
    (automatically or by contextual menu or by a command) the "Proof
    using" annotation suggested by Coq. This suggestion happens at