<!DOCTYPE html><html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8" /></head><body><div data-html-editor-font-wrapper="true" style="font-family: arial, sans-serif; font-size: 13px;">Dear list,<br>We are happy to announce the release of [Proof General version 4.5](https://github.com/ProofGeneral/PG/releases/tag/v4.5).<br><br>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.<br><br>Website: https://proofgeneral.github.io/<br>Core maintainers e-mail: proof-general-maintainers@groupes.renater.fr<br><br>Proof General includes these features, amongst others:<br><br>- Script management: proof assistant state reflected in editor<br>- Commands for building and replaying proofs<br>- Syntax highlighting of proof scripts and prover output; hiding proofs<br>- Menu for jumping to theorems in a proof script<br>- Provision to easily run proof assistant on a remote host<br>- Works on any system where emacs and coq are running<br><br>## Summary of changes from 4.4 to 4.5:<br><br>### Generic changes<br><br>- **proof-general** is now a MELPA (https://melpa.org/#/proof-general) and NonGNU ELPA (https://elpa.nongnu.org/nongnu-devel/proof-general.html) Emacs package.<br>- It now requires GNU Emacs 25.2 or later<br>- License changed to GPL-3.0-or-later<br>- Remove support for the following systems:<br> Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.<br>- Support for Qrhl-tool (by Dominique Unruh)<br>- Support for EasyCrypt (by Pierre-Yves Strub)<br>- PG's manual is continuously deployed at https://proofgeneral.github.io/doc/master/userman/<br><br>### Coq changes<br><br>- Auto Compilation of Requires improved:<br> - support of vos/vok compilation<br> - background compilation<br>- "Omit complete opaque proofs" mode for speed.<br>- Automatic insertion of "Proof using" annotations.<br>- Folding/unfolding hypotheses.<br>- Support Ssreflect's `move=>` intro style with `C-c C-a TAB`<br>- Support Coq's ``Diffs`` and ``Show Proof Diffs`` features.<br><br>### Miscellaneous<br><br>- New mode: `opam-switch-mode` (https://github.com/ProofGeneral/opam-switch-mode), also distributed on MELPA, allows to easily perform `opam switch` (and thus switch between coq versions) from within Emacs.<br>- To keep PG up-to-date (https://proofgeneral.github.io/#keeping-proof-general-up-to-date), 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.<br><br>The ProofGeneral Team</div></body></html>