NonGNU-devel 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.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 http://askra.de/software/prooftree 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.
*** New command `proof-check-proofs' to generates the proof status
    of all opaque proofs. Currently only available for Coq, see Coq
    changes below for more details.

** 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 command `proof-check-proofs' to generates the proof status
    of all opaque proofs. This command is useful for a development
    process where invalid proofs are permitted and vos compilation and
    the omit proofs feature are used to work at the most interesting
    or challenging point instead of on the first invalid proof. The
    command generates a list of all opaque proofs in the current
    buffer together with the information whether the proof script is
    currently valid or invalid. The command can also be run in batch
    mode, for instance in a continuous integration environment.
*** 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
(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 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
...
...