NonGNU ELPA - proof-general

-*- outline -*-  

This is a summary of main changes.  For details, please see
the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG

* 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
(https://packages.debian.org/stable/emacs) and Ubuntu LTS
(https://packages.ubuntu.com/emacs), until their End-Of-Support (see
also https://wiki.ubuntu.com/Releases). 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
   Unruh.
   References:
   - Initial pull request: https://github.com/ProofGeneral/PG/pull/636
   - Qrhl-tool web site: https://dominique-unruh.github.io/qrhl-tool

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