[ < ] | [ > ] |  | [ << ] | [ 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 version 3.7.1

Proof General version 3.7.1 is an updated and enhanced version of Proof General 3.7. See ‘`CHANGES`’ for more details.

Proof General version 3.7 collects together a cummulative set of improvements to Proof General 3.5. 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, some after feedback from use at TYPES Summer Schools. Many new features have been added to enhance Coq mode (thanks to Pierre Courtieu) and several improvements made for Isabelle (thanks to Makarius Wenzel, Stefan Berghofer and Tjark Weber).

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 in place of ASCII sequences), Math-Menu (for Unicode symbols) and MMM Mode (for multiple modes in one buffer) are bundled with Proof General. A new Unicode Tokens package has been added which will replace X-Symbol eventually.

Proof General 3.7 is available in RPM package format which includes pre-compiled code for GNU Emacs or XEmacs and 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.5, 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 powerful environments and tools for interactive proof.

Proof General has been Emacs based so far and uses heavy per-prover customisation. The new 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. 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 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 from (indirect) funding by EPSRC (Applications of a Type Theory Based Proof Assistant in the late 1990s and The Integration and Interaction of Multiple Mathematical Reasoning Processes, EP/E005713/1 (RA0084) in 2006-8), the EC (the Co-ordination Action Types and previous related projects), and the support of the LFCS. Version 3.1 was prepared whilst David Aspinall was visiting ETL, Japan, supported by the British Council.

For Proof General 3.7, Graham Dutton assisted with the project management system and web pages. 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 and patches, including Cuihtlauac Alvarado, Lennart Beringer, Pascal Brisset, James Brotherston, Martin Buechi, Lucas Dixon, Matt Fairtlough, Ivan Filippenko, Kim Hyung Ho, Mark A. Hillebrand, 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, Norbert Voelker, Tjark Weber Mitsuharu Yamamoto.

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

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

This document was generated by David Aspinall on July, 24 2008 using texi2html 1.78.