proof-general v4.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.

• Website: https://proofgeneral.github.io/
• 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://melpa.org/#/proof-general) and NonGNU ELPA (https://elpa.nongnu.org/nongnu-devel/proof-general.html) 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://proofgeneral.github.io/doc/master/userman/

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://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 (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.

PG 4.4

Proof General 4.4