[TYPES/announce] ProofGeneal release 4.5
pierre.courtieu at cnam.fr
pierre.courtieu at cnam.fr
Mon Nov 14 08:15:17 EST 2022
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>
More information about the Types-announce
mailing list