Proof General Home


This is a flattened outline file: click on a title to hide/reveal the leaf underneath it.
Click here to show whole body, or here to hide whole body.

Changes of Proof General 4.2 from Proof General 4.1

Generic/misc changes

Added user option: `proof-next-command-insert-space'

Support proof-tree visualization via the external Prooftree program

Compilation fixes for Emacs 24.

Fix "pgshell" mode for shell/CLI prover interaction

Coq changes

Smarter three windows mode:

Multiple file handling for Coq Feature.

Support proof-tree visualization

New commands for Print/Check/About/Show with "Printing All" flag

Coq menus and shortcut in response and goals buffers.

Tooltips hidden by default

"Insert Requires" now uses completion based on coq-load-path

New setting for hiding additional goals from the *goals* buffer

Double hit terminator

Indentation improvements using SMIE. Supporting bullets and { }.

"Show" shows the (cached) state of the proof at point.

Minor parsing fixes

Windows resizing fixed


Basic support now works, see hol-light directory [WORK IN PROGRESS]

Changes of Proof General 4.1 from Proof General 4.0

Generic changes

Parsing now uses cache by default (proof-use-parser-cache=t).

Isabelle changes

Unicode tokens enabled by default

Coq changes

A new indentation algorithm, using SMIE.

Experimental multiple file handling for Coq.

Fixes for Coq 8.3

Main Changes for Proof General 4.0 from 3.7.1

Install/support changes

XEmacs is no longer supported; PG only works with GNU Emacs 23.1+

Primary distribution formats changed

Generic changes

Font-lock based Unicode Tokens mode replaces X-Symbol

Document-centred mechanisms added:

Automatic processing mode

Fast buffer processing option

Improved prevention of Undo in locked region

Proof General -> Options menu extended and rearranged

New query identifier info button and command (C-c C-i, C-M-mouse1)

New user configuration options (also on Proof General -> Options)

Removed user configuration options

"Movie" output: export an annotated buffer in XML

Isabelle/Isar changes

Support undo back into completed proofs (linear_undo).

Electric terminator works without inserting terminator

Line numbers reported during script management

Sync problems with bad input prevented by command wrapping

Isabelle Settings now organised in sub-menus

Coq changes

Only supports Coq 8.1+, support for earlier versions dropped.

Holes mode can be turned on/off and has its own minor mode

Some keyboard shortcuts are now available in goals buffer

Experimental storing buffer

bug fixes, bugs

Notable internal changes

Altered prover configuration settings (internal)

Simplified version of comint now used for proof shell (internal)

Click here to go back to the front page.

Web pages by David Aspinall. Please report issues on PG trac.
Last modified 21 December 2017.