[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

# 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 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.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## Latest news for 3.6

Proof General versions 3.6 (and 3.5 shortly before it) collect together a cummulative set of improvements to Proof General 3.4. There are compatibility fixes for newer Emacs versions, and particularly for GNU Emacs: credit is due to Stefan Monnier for an intense period of debugging and patching. The options menu has been simplified and extended, and the display management is improved and repaired for Emacs API changes. There are some other usability improvements, prompted in part by feedback after Proof General's appearance at the TYPES 2002 Summer School.

Support has been added for the useful Emacs packages Speedbar and Index Menu, both usually distributed with Emacs. Compatible versions of the Emacs packages X-Symbol (for mathematical symbols) and MMM Mode (for multiple modes in one buffer) are now bundled with Proof General to save the need for additional downloads.

Proof General 3.6 runs reliably as compiled Elisp code, and is available in RPM package format which includes desktop integration on freedesktop.org compliant desktops (including, for example, many recent Linux distributions).

See the ``CHANGES'` file in the distribution for more complete details of changes since version 3.4, and the appendix History of Proof General for old news.

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## Future

The aim of the Proof General project is to provide a powerful and configurable interfaces which help user-interaction with interactive proof assistants. The strategy Proof General uses is to targets power users rather than novices; other interfaces have often neglected this class of users. But we do include general user interface niceties, such as toolbar and menus, which make use easier for all.

Proof General has been Emacs based so far, but plans are afoot to liberate it from the points and parentheses of Emacs Lisp. The successor project Proof General Kit 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.

In 2004 a project to develop PGIP inside the Eclipse IDE will begin. There is also a prototype version of a PGIP-enabled Isabelle under development, and a middleware component for co-ordinating proof written in Haskell. Further collaborations are sought for more developments, especially the PGIP enabling of other provers. For more details, see the Proof General Kit webpage. Help us to help you organize your proofs!

[ < ] | [ > ] |  | [ << ] | [ Up ] | [ >> ] |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

## Credits

The original developers of the basis of Proof General were:

- David Aspinall,
- Healfdene Goguen,
- Thomas Kleymann, and
- Dilip Sequeira.

LEGO Proof General (the successor of `lego-mode`) was written by Thomas Kleymann and Dilip Sequeira. It is presently maintained by David Aspinall and Paul Callaghan <P.C.Callaghan@durham.ac.uk>. Coq Proof General was written by Healfdene Goguen, with later contributions from Patrick Loiseleur. It is now maintained by Pierre Courtieu <courtieu@lri.fr>. Isabelle Proof General was written and is being maintained by David Aspinall <David.Aspinall@ed.ac.uk>. It has benefited greatly from tweaks and suggestions by Markus Wenzel <wenzelm@informatik.tu-muenchen.de>, who wrote Isabelle/Isar Proof General and added Proof General support inside Isabelle. David von Oheimb supplied the original patches for X-Symbol support, which improved Proof General significantly. Christoph Wedler, the author of X-Symbol, has provided much useful support in adapting his package for PG.

The generic base for Proof General was developed by Kleymann, Sequeira, Goguen and Aspinall. It follows some of the ideas used in Project CROAP. The project to implement a proof mode for LEGO was initiated in 1994 and coordinated until October 1998 by Thomas Kleymann, becoming generic along the way. In October 1998, the project became Proof General and has been managed by David Aspinall since then.

This manual was written by David Aspinall and Thomas Kleymann. Some words found their way here from the user documentation of LEGO mode, prepared by Dilip Sequeira. Healfdene Goguen supplied some text for Coq Proof General. Since Proof General 2.0, this manual has been maintained and improved by David Aspinall. Pierre Courtieu and Markus Wenzel contributed some sections.

The Proof General project has benefited indirectly from funding by EPSRC (Applications of a Type Theory Based Proof Assistant), the EC (Types for Proofs and Programs) and the support of the LFCS. Version 3.1 was prepared whilst David Aspinall was visiting ETL, Japan, supported by the British Council.

For testing and feedback for older versions of Proof General, thanks go to Rod Burstall, Martin Hofmann, and James McKinna, and some of those who continued to help with the latest 3.x series, named next.

During the development of Proof General 3.x releases, many people helped provide testing and other feedback, including the Proof General maintainers, Paul Callaghan, Pierre Courtieu, and Markus Wenzel, Stefan Berghofer, Gerwin Klein, and other folk who tested pre-releases or sent bug reports, including Cuihtlauac Alvarado, Lennart Beringer, Pascal Brisset, James Brotherston, Martin Buechi, Lucas Dixon, Matt Fairtlough, Kim Hyung Ho, Greg O'Keefe, Pierre Lescanne, John Longley, Stefan Monnier, Tobias Nipkow, Leonor Prensa Nieto, David von Oheimb, Lawrence Paulson, Paul Roziere, Randy Pollack, Robert R. Schneck, Norbert Schirmer, Sebastian Skalberg, Mike Squire, and Norbert Voelker.

Thanks to all of you (and apologies to anyone missed).

[ << ] | [ >> ] |  |  |  |  |  | [Top] | [Contents] | [Index] | [ ? ]

This document was generated by David Aspinall on November, 7 2006 using texi2html 1.76.