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 https://proofgeneral.github.io. Visit this page for the latest version of this manual, other documentation, system downloads, etc.

News for Version 4.6

N/A

News for Version 4.5

Proof-General is now distributed under the GPLv3+ license.

This release contains several bugfixes and many new features (see the CHANGES file or the Git changelog for more details).

The support of the following systems have been added: EasyCrypt, qrhl-tool.

The old code for the support of the following systems have been removed: Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, Isabelle, HOL98.

News for Version 4.4

Proof General 4.4 is the first release since PG has moved to GitHub.

This release contains several bugfixes and improvements (see the Git ChangeLog for more details) and supports both Coq 8.4 and Coq 8.5.

News for Version 4.3

In Proof General version 4.3, the multiple file handling for Coq has been improved. It now supports asynchronous and parallel compilation of required modules.

The proof tree display now supports the newest features of Coq 8.4. Proof General version 4.3 is compatible with Prooftree version 0.11 (or better).

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 section Unicode symbols and special layout support;
to allow “document centred” working, annotating scripts with prover output and automatically sending commands to the prover, see section Document centred working;
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 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 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!

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 no longer maintained. Coq Proof General was written by Healfdene Goguen, with later contributions from Patrick Loiseleur. It is now maintained by Pierre Courtieu. Isabelle Proof General was written and is being maintained by David Aspinall. It has benefited greatly from tweaks and suggestions by Markus Wenzel, who wrote the first support for Isar 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, 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, with words borrowed from user documentation of LEGO mode, prepared by Dilip Sequeira. Healfdene Goguen wrote some text for Coq Proof General. Since Proof General 2.0, this manual has been maintained by David Aspinall, with contributions from Pierre Courtieu, Markus Wenzel and Hendrik Tews.

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 helped with web pages and infrastructure; since then the the computing support team at the School of Informatics have given help. For testing and feedback for older versions of Proof General, thanks go to Rod Burstall, Martin Hofmann, and James McKinna, and several on the longer list below.

For the Proof General 4.0 release, special thanks go to Stefan Monnier for patches and suggestions, to Makarius for many bug reports and help with Isabelle support and to Pierre Courtieu for providing new features for Coq support.

Between Proof General 4.3 and 4.4 releases, the PG sources have been migrated from CVS to to GitHub; special thanks go to Clement Pit–Claudel for help in this migration.

Proof General 4.4’s new icons were contributed by Yoshihiro Imai (http://proofcafe.org/wiki/Generaltan) under CC-BY-SA 3.0 (https://creativecommons.org/licenses/by-sa/3.0/)

During the development of Proof General 3.x and 4.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, Esben Andreasen, Lennart Beringer, Pascal Brisset, James Brotherston, Martin Buechi, Pierre Casteran, Lucas Dixon, Erik Martin-Dorel, Matt Fairtlough, Ivan Filippenko, Georges Gonthier, Robin Green, Florian Haftmann, Kim Hyung Ho, Mark A. Hillebrand, Greg O’Keefe, Alex Krauss, Peter Lammich, Pierre Lescanne, John Longley, Erik Martin-Dorel, Assia Mahboubi, Adam Megacz, Stefan Monnier, Tobias Nipkow, Clement Pit–Claudel, Leonor Prensa Nieto, David von Oheimb, Lawrence Paulson, Paul Roziere, Randy Pollack, Robert R. Schneck, Norbert Schirmer, Sebastian Skalberg, Mike Squire, Hendrik Tews, Norbert Voelker, Tjark Weber, Mitsuharu Yamamoto.

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

This document was generated on November 21, 2024 using texi2html 1.82.