Download User manual - Proof General

Preface
1
Preface
Welcome to Proof General!
This preface has some news about the current release, future plans, and acknowledgements to
those who have helped along the way. The appendix [History of Proof General], page 77 contains
old news about previous releases, and notes on the development of Proof General.
Proof General has a home page at http://proofgeneral.inf.ed.ac.uk. Visit this page for
the latest version of this manual, other documentation, system downloads, etc.
News for Version 4.2
Proof General version 4.2 adds the usual round of compatibility fixes, to support newer versions
of Emacs and Coq. It also contains some updates to support HOL Light in a primitive fashion.
It also contains a new mechanism to display proof trees, provided by Hendrik Tews and using a
bespoke rendering application named Prooftree.
News for Version 4.1
Proof General version 4.1 adds some compatibility fixes to Proof General 4.0, specifically for
Coq version 8.3 and Isabelle 2011.
It also contains a new implementation of multiple file handling for Coq provided by Hendrik
Tews.
News for Version 4.0
Proof General version 4.0 is a major overhaul of Proof General. The main changes are:
• support for GNU Emacs only, you cannot use XEmacs any more;
• a new Unicode Tokens mode, which now replaces X-Symbol, see Chapter 4 [Unicode symbols
and special layout support], page 27;
• to allow “document centred” working, annotating scripts with prover output and automatically sending commands to the prover, see Section 3.1 [Document centred working],
page 21;
• support for latest versions of provers (Isabelle2009-2 and Coq 8.2);
• numerous smaller enhancements and efficiency improvements.
See the ‘CHANGES’ file in the distribution for more complete details of changes, and the appendix
[History of Proof General], page 77 for old news.
Future
The aim of the Proof General project is to provide powerful environments and tools for interactive
proof.
Proof General has been Emacs based so far and uses heavy per-prover customisation. The
Proof General Kit project proposes that proof assistants use a standard XML-based protocol
for interactive proof, dubbed PGIP. PGIP will enable middleware for interactive proof tools and
interface components. Rather than configuring Proof General for your proof assistant, you will
need to configure your proof assistant to understand PGIP. There is a similarity however; the
design of PGIP was based heavily on the Emacs Proof General framework.
At the time of writing, the Proof General Kit software is in a prototype stage and the PGIP
protocol is still being refined. We have a prototype Proof General plugin for the Eclipse IDE
and a prototype version of a PGIP-enabled Isabelle. There is also a middleware component for
co-ordinating proof written in Haskell, the Proof General Broker. Further collaborations are