[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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: [email protected]
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
