History of Proof General

It all started some time in 1994. There was no Emacs interface for LEGO. Back then, Emacs militants worked directly with the Emacs shell to interact with the LEGO system.

David Aspinall convinced Thomas Kleymann that programming in Emacs Lisp wasn’t so difficult after all. In fact, Aspinall had already implemented an Emacs interface for Isabelle with bells and whistles, called Isamode. Soon after, the package lego-mode was born. Users were able to develop proof scripts in one buffer. Support was provided to automatically send parts of the script to the proof process. The last official version with the name lego-mode (1.9) was released in May 1995.

The interface project really took off the ground in November 1996. Yves Bertot had been working on a sophisticated user interface for the Coq system (CtCoq) based on the generic environment Centaur. He visited the Edinburgh LEGO group for a week to transfer proof-by-pointing technology. Even though proof-by-pointing is an inherently structure-conscious algorithm, within a week, Yves Bertot, Dilip Sequeira and Thomas Kleymann managed to implement a first prototype of proof-by-pointing in the Emacs interface for LEGO [BKS97].

Perhaps we could reuse even more of the CtCoq system. It being a structure editor did no longer seem to be such an obstacle. Moreover, to conveniently use proof-by-pointing in actual developments, one would need better support for script management.

In 1997, Dilip Sequeira implemented script management in our Emacs interface for LEGO following the recipe in [BT98]. Inspired by the project CROAP, the implementation made some effort to be generic. A working prototype was demonstrated at UITP’97.

In October 1997, Healfdene Goguen ported lego-mode to Coq. Part of the generic code in the lego package was outsourced (and made more generic) in a new package called proof. Dilip Sequeira provided some LEGO-specific support for handling multiple files and wrote a few manual pages. The system was reasonably robust and we shipped out the package to friends.

In June 1998, David Aspinall reentered the picture by providing an instantiation for Isabelle. Actually, our previous version wasn’t quite as generic as we had hoped. Whereas LEGO and Coq are similar systems in many ways, Isabelle was really a different beast. Fierce re-engineering and various usability improvements were provided by Aspinall and Kleymann to make it easier to instantiate to new proof systems. The major technical improvement was a truly generic extension of script management to work across multiple files.

It was time to come up with a better name than just proof mode. David Aspinall suggested Proof General and set about reorganizing the file structure to disentangle the Proof General project from LEGO at last. He cooked up some images and bolted on a toolbar, so a naive user can replay proofs without knowing a proof assistant language or even Emacs hot-keys. He also designed some web pages, and wrote most of this manual.

Despite views of some detractors, we demonstrated that an interface both friendly and powerful can be built on top of Emacs. Proof General 2.0 was the first official release of the improved program, made in December 1998.

Version 2.1 was released in August 1999. It was used at the Types Summer School held in Giens, France in September 1999 (see http://www-sop.inria.fr/types-project/types-sum-school.html). About 50 students learning Coq, Isabelle, and LEGO used Proof General for all three systems. This experience provided invaluable feedback and encouragement to make the improvements that went into Proof General 3.0.

Old News for 3.0

Proof General 3.0 (released November 1999) has many improvements over 2.x releases.

First, there are usability improvements. The toolbar was somewhat impoverished before. It now has twice as many buttons, and includes all of the useful functions used during proof which were previously hidden on the menu, or even only available as key-presses. Key-bindings have been re-organized, users of previous versions may notice. The menu has been redesigned and coordinated with the toolbar, and now gives easy access to more of the features of Proof General. Previously several features were only likely to be discovered by those keen enough to read this manual!

Second, there are improvements, extensions, and bug fixes in the generic basis. Proofs which are unfinished and not explicitly closed by a “save” type command are supported by the core, if they are allowed by the prover. The design of switching the active scripting buffer has been streamlined. The management of the queue of commands waiting to be sent to the shell has been improved, so there are fewer unnecessary "Proof Process Busy!" messages. The support for scripting with multiple files was improved so that it behaves reliably with Isabelle99; file reading messages can be communicated in both directions now. The proof shell filter has been optimized to give hungry proof assistants a better share of CPU cycles. Proof-by-pointing has been resurrected; even though LEGO’s implementation is incomplete, it seems worth maintaining the code in Proof General so that the implementors of other proof assistants are encouraged to provide support. For one example, we can certainly hope for support in Coq, since the CtCoq proof-by-pointing code has been moved into the Coq kernel lately. We need a volunteer from the Coq community to help to do this.

An important new feature in Proof General 3.0 is support for X-Symbol, which means that real logical symbols, Greek letters, etc can be displayed during proof development, instead of their ASCII approximations. This makes Proof General a more serious competitor to native graphical user interfaces.

Finally, Proof General has become much easier to adapt to new provers — it fails gracefully (or not at all!) when particular configuration variables are unset, and provides more default settings which work out-of-the-box. An example configuration for Isabelle is provided, which uses just 25 or so simple settings.

This manual has been updated and extended for Proof General 3.0. Amongst other improvements, it has a better description of how to add support for a new prover.

See the CHANGES file in the distribution for more information about the latest improvements in Proof General. Developers should check the ChangeLog in the developer’s release for detailed comments on internal changes.

Most of the work for Proof General 3.0 has been done by David Aspinall. Markus Wenzel helped with Isabelle support, and provided invaluable feedback and testing, especially for the improvements to multiple file handling. Pierre Courtieu took responsibility from Patrick Loiseleur for Coq support, although improvements in both Coq and LEGO instances for this release were made by David Aspinall. Markus Wenzel provided support for his Isar language, a new proof language for Isabelle. David von Oheimb helped to develop the generic version of his X-Symbol addition which he originally provided for Isabelle.

A new instantiation of Proof General is being worked on for Plastic, a proof assistant being developed at the University of Durham.

Old News for 3.1

Proof General 3.1 (released March 2000) is a bug-fix improvement over version 3.0. There are some minor cosmetic improvements, but large changes have been held back to ensure stability. This release solves a few minor problems which came to light since the final testing stages for 3.0. It also solves some compatibility problems, so now it works with various versions of Emacs which we hadn’t tested with before (non-mule GNU Emacs, certain Japanese Emacs versions).

We’re also pleased to announce HOL Proof General, a new instance of Proof General for HOL98. This is supplied as a "technology demonstration" for HOL users in the hope that somebody from the HOL community will volunteer to adopt it and become a maintainer and developer. (Otherwise, work on HOL Proof General will not continue).

Apart from that there are a few other small improvements. Check the CHANGES file in the distribution for full details.

The HOL98 support and much of the work on Proof General 3.1 was undertaken by David Aspinall while he was visiting ETL, Osaka, Japan, supported by the British Council and ETL.

Old News for 3.2

Proof General 3.2 introduced several new features and some bug fixes. One noticeable new feature is the addition of a prover-specific menu for each of the supported provers. This menu has a “favourites” feature that you can use to easily define new functions. Please contribute other useful functions (or suggestions) for things you would like to appear on these menus.

Because of the new menus and to make room for more commands, we have made a new key map for prover specific functions. These now all begin with C-c C-a. This has changed a few key bindings slightly.

Another new feature is the addition of prover-specific completion tables, to encourage the use of Emacs’s completion facility, using C-RET. See section Support for completion, for full details.

A less obvious new feature is support for turning the proof assistant output on and off internally, to improve efficiency when processing large scripts. This means that more of your CPU cycles can be spent on proving theorems.

Adapting for new proof assistants continues to be made more flexible, and easier in several places. This has been motivated by adding experimental support for some new systems. One new system which had good support added in a very short space of time is PhoX (see the PhoX home page for more information). PhoX joins the rank of officially supported Proof General instances, thanks to its developer Christophe Raffalli.

Breaking the manual into two pieces was overdue: now all details on adapting Proof General, and notes on its internals, are in the Adapting Proof General manual. You should find a copy of that second manual close to wherever you found this one; consult the Proof General home page if in doubt.

The internal code of Proof General has been significantly overhauled for this version, which should make it more robust and readable. The generic code has an improved file structure, and there is support for automatic generation of autoload functions. There is also a new mechanism for defining prover-specific customization and instantiation settings which fits better with the customize library. These settings are named in the form PA-setting-name in the documentation; you replace PA by the symbol for the proof assistant you are interested in. See section Customizing Proof General, for details.

Finally, important bug fixes include the robustification against write-file (C-x C-w), revert-buffer, and friends. These are rather devious functions to use during script management, but Proof General now tries to do the right thing if you’re deviant enough to try them out!

Work on this release was undertaken by David Aspinall between May-September 2000, and includes contributions from Markus Wenzel, Pierre Courtieu, and Christophe Raffalli. Markus added some Isar documentation to this manual.

Old News for 3.3

Proof General 3.3 includes a few feature additions, but mainly the focus has been on compatibility improvements for new versions of provers (in particular, Coq 7), and new versions of emacs (in particular, XEmacs 21.4).

One new feature is control over visibility of completed proofs, See section Visibility of completed proofs. Another new feature is the tracking of theorem dependencies inside Isabelle. A context-sensitive menu (right-button on proof scripts) provides facility for browsing the ancestors and child theorems of a theorem, and highlighting them. The idea of this feature is that it can help you untangle and rearrange big proof scripts, by seeing which parts are interdependent. The implementation is provisional and not documented yet in the body of this manual. It only works for the "classic" version of Isabelle99-2.

Old News for 3.4

Proof General 3.4 adds improvements and also compatibility fixes for new versions of Emacs, in particular, for GNU Emacs 21, which adds the remaining pretty features that have only been available to XEmacs users until now (the toolbar and X-Symbol support).

One major improvement has been to provide better support for synchronization with Coq proof scripts; now Coq Proof General should be able to retract and replay most Coq proof scripts reliably. Credit is due to Pierre Courtieu, who also updated the documentation in this manual.

As of version 3.4, Proof General is distributed under the GNU General Public License (GPL). Compared with the previous more restrictive license, this means the program can now be redistributed by third parties, and used in any context without applying for a special license. Despite these legal changes, we would still appreciate if you send us back any useful improvements you make to Proof General.

Old News for 3.5

Old News for 3.6

There was no 3.6 release of Proof General.

Old News for 3.7

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 cumulative 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. A compatible version of the Emacs package Math-Menu (for Unicode symbols) is bundled with Proof General. An experimental Unicode Tokens package has been added which will replace X-Symbol.

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.

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