The future of Proof General

Having selected Isabelle, it is worthwhile considering the future directions of the de facto Isabelle GUI, namely Proof General, previously described on page .

David Aspinall has announced plans [7] for the future development of Proof General, in order to address drawbacks for both the users and developers of the system.

Points noted as problems for users include the Emacs-centric environment, the lack of prover-specific GUI features, the provisions of only limited methods for network-wide development, and the need to learn the command language of the prover.

The developers dislike the need for all customisation and extension to be done in Emacs Lisp. Even worse, there is a non-trivial amount of duplicated information about the proof assistants in the interfaces code. The variation in communication between Proof General and each of the provers it supports also complicates the configuration.

The range of measures designed to remedy most of the points discussed above, does so through a modularisation of the current system (made up of the proof assistant, communicating directly with the proof interface which manages multiple tasks: display, input, theory browser, proof replayer, program extractor and controlling the theory libraries). The main idea is to implement a mediator program between the proof assistant and the main functions of the user interface. Each of these functions can be implemented by a separate process (if so desired). This may be a very handy segmentation of functionality, allowing the designers for each function to focus on performing that function well. The proof mediator will still need to be general enough to provide enough information to each of these modules, which is sure to require cooperation from the proof assistant.

Assumptions made of the proof assistant will include:

• the starting point of a proof is a target goal
• proof building proceeds in steps
• these steps must be reversible
• proofs can be abandoned, saved or closed at any time

Communication between these modules is to be implemented with an XML [23] based document structure. XML based grammars are easy to parse (with many free libraries available), are portable by design, and individual messages are encoded in plain text and are nearly human readable.

The low-level transport mechanism for these XML messages has not been finalised (possibly allowing features such as network transparency: building a proof on a graphical workstation with a nice display while the proof assistant runs on a powerful but loud server locked away in a cramped server room).

The proposed protocol is called ``Proof General Interactive Proof'' (PGIP), the subset of which dedicated to the proof assistant in describing the proof in progress is named the ``Proof General Markup Language'' (PGML).Not to be confused with Adobe's Precision Graphics Markup Language, a vector graphics description language. A number of XML standards for displaying mathematical documents exist, (MathML [8], OpenMath [2]), but were deemed by Aspinall to add too much complexity for the current range of proof assistants to be written to accommodate. Future versions of PGML may well bear closer resemblance to MathML.

An unfortunate consequence of working with PGIP is due to the pre-alpha state of the definition itself, and the implementation available for Isabelle. It is highly unlikely that Igloo will be fully operational in the near future. On the other hand, I claim that this is the best way to influence the future direction of theorem-proving interfaces.