We are happy to announce the release of Proof General version 4.5.
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.
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
- proof-general is now a MELPA (MELPA) and NonGNU ELPA (NonGNU-devel ELPA - proof-general) 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 Documentation
- 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
Show Proof Diffsfeatures.
- 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.
- To keep PG up-to-date (Proof General), we recommend to install PG from MELPA or NonGNU-devel-ELPA and use
M-x proof-upgrade-elpa-packages RETevery once in a while.
The ProofGeneral Team