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-report' to generates the proof status
    of all opaque proofs. Currently only available for Coq, see Coq
    changes below for more details.
*** New command `proof-check-annotate' to annotate all failing proofs
    with FAIL comments.

** 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-report 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 command `proof-check-annotate' to annotate all failing proofs
    with FAIL comments. Useful in the development process as described
    above to ensure all currently failing proofs are marked as such.
*** flag Printing Parentheses and Printing Notations can be set/unset
    via menu and Coq keymap (C-c C-a C-9 and C-c C-a C-0 for
    Parentheses (optimized for British and American keyboards); C-c
    C-a n and C-c C-a N for Notations).
*** 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
...
...