Skip to content

proof-general v4.5

Latest
Compare
Choose a tag to compare
@erikmd erikmd released this 14 Nov 10:38
· 141 commits to master since this release
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.

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

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