[TYPES/announce] ProofGeneal release 4.5

[pierre.courtieu at cnam.fr]

Dear list,
We are happy to announce the release of [Proof General version 4.5](https://urldefense.com/v3/__https://github.com/ProofGeneral/PG/releases/tag/v4.5__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDhL2n9kFg$ ).

Proof General is a generic Emacs mode for proof assistants. It can be instantiated for the proof assistant of your choice, and is supplied ready-customized for Coq, PhoX, EasyCrypt, Qrhl-tool.

Website: https://urldefense.com/v3/__https://proofgeneral.github.io/__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDgZe5gBLA$ 
Core maintainers e-mail: proof-general-maintainers at groupes.renater.fr

Proof General includes these features, amongst others:

- Script management: proof assistant state reflected in editor
- Commands for building and replaying proofs
- Syntax highlighting of proof scripts and prover output; hiding proofs
- Menu for jumping to theorems in a proof script
- Provision to easily run proof assistant on a remote host
- Works on any system where emacs and coq are running

## Summary of changes from 4.4 to 4.5:

### Generic changes

- **proof-general** is now a MELPA (https://urldefense.com/v3/__https://melpa.org/*/proof-general__;Iw!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDjngAIi6g$ ) and NonGNU ELPA (https://urldefense.com/v3/__https://elpa.nongnu.org/nongnu-devel/proof-general.html__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDgsR7a85Q$ ) Emacs package.
- It now requires GNU Emacs 25.2 or later
- License changed to GPL-3.0-or-later
- Remove support for the following systems:
 Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.
- Support for Qrhl-tool (by Dominique Unruh)
- Support for EasyCrypt (by Pierre-Yves Strub)
- PG's manual is continuously deployed at https://urldefense.com/v3/__https://proofgeneral.github.io/doc/master/userman/__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDghKm3sRw$ 

### Coq changes

- Auto Compilation of Requires improved:
 - support of vos/vok compilation
 - background compilation
- "Omit complete opaque proofs" mode for speed.
- Automatic insertion of "Proof using" annotations.
- Folding/unfolding hypotheses.
- Support Ssreflect's `move=>` intro style with `C-c C-a TAB`
- Support Coq's ``Diffs`` and ``Show Proof Diffs`` features.

### Miscellaneous

- New mode: `opam-switch-mode` (https://urldefense.com/v3/__https://github.com/ProofGeneral/opam-switch-mode__;!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDiHZBvpkg$ ), also distributed on MELPA, allows to easily perform `opam switch` (and thus switch between coq versions) from within Emacs.
- To keep PG up-to-date (https://urldefense.com/v3/__https://proofgeneral.github.io/*keeping-proof-general-up-to-date__;Iw!!IBzWLUs!V69kuQwkn1BzqYx5z9l0SyjqaCuIXgTGyA0_YaIrDYDy2tp2IqEEB-VG7TIIPLt8WyO9t50ONX91tC5KCQxfg9EgbS8ZiTP8zDgzWE0gLQ$ ), we recommend to install PG from MELPA or NonGNU-devel-ELPA and use `M-x proof-upgrade-elpa-packages RET` every once in a while.

The ProofGeneral Team
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20221114/a12c046a/attachment.htm>