NonGNU-devel ELPA - proof-general


A generic Emacs interface for proof assistants
proof-general-4.6snapshot0.20240406.170701.tar (.sig), 2024-Apr-06, 3.34 MiB
Atom feed
Browse ELPA's repository
CGit or Gitweb

To install this package from Emacs, use package-install or list-packages.

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-tool, 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).

Old versions

proof-general-4.6snapshot0.20240331.190844.tar.lz2024-Mar-31 956 KiB
proof-general-4.6snapshot0.20240328.234401.tar.lz2024-Mar-31 956 KiB
proof-general-4.6snapshot0.20240327.145242.tar.lz2024-Mar-27 956 KiB
proof-general-4.6snapshot0.20240315.201317.tar.lz2024-Mar-16 956 KiB
proof-general-4.6snapshot0.20240223.140534.tar.lz2024-Feb-23 956 KiB
proof-general-4.6snapshot0.20240128.153331.tar.lz2024-Jan-28 957 KiB
proof-general-4.6snapshot0.20231219.82832.tar.lz2023-Dec-19 955 KiB
proof-general-4.6snapshot0.20221130.94645.tar.lz2022-Nov-30 954 KiB
proof-general- 952 KiB
proof-general-4.5snapshot0.20220707.75856.tar.lz2022-Jul-07 951 KiB


-*- outline -*-  

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

* Changes of Proof General 4.6 from Proof General 4.5

** Generic changes
*** Improve the omit-proofs feature to handle a number of cases where
    proofs must not be omitted.
*** Renew support for proof-tree visualization via the external command
    prooftree, see and Section 7
    "Graphical Proof-Tree Visualization" in the Proof General manual.
    Proof-tree visualization is currently only supported for Coq. The
    prooftree support has been substantially rewritten, making use of
    the much better support since Coq version 8.11.

** Coq changes
*** support Coq 8.19
**** New option coq-compile-coqdep-warnings to configure the warning
     command line argument (-w) of coqdep. The default of this option
     is +module-not-found to let Proof General reliably detect missing
     modules as coqdep error.
*** Renew support for proof-tree visualization, see description in
    generic changes above.

**** New options coq-compile-extra-coqc-arguments and
     coq-compile-extra-coqdep-arguments to configure additional
     command line arguments to calls of, respetively, coqc and coqdep
     during auto compilation.

**** Fix issues #687 and #688 where the omit-proofs feature causes
     errors on correct code.

* 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 triggered 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