A. Plans and Ideas

This appendix contains some tentative plans and ideas for improving Proof General.

This appendix is no longer extended: instead we keep a list of Proof General projects on the web, and forthcoming plans and ideas in the ‘TODO’ and ‘todo’ files included in the ordinary and developers PG distributions, respectively. Once the items mentioned below are implemented, they will be removed from here.

Please send us contributions to our wish lists, or better still, an offer to implement something from them!

A.1 Proof by pointing and similar features

This is a note by David Aspinall about proof by pointing and similar features.

Proof General already supports proof by pointing, and experimental support was provided in LEGO. We would like to extend this support to other proof assistants. Unfortunately, proof by pointing requires rather heavy support from the proof assistant. There are two aspects to the support:

term structure mark-up
proof by pointing command generation

Term structure mark-up is useful in itself: it allows the user to explore the structure of a term using the mouse (the smallest subexpression that the mouse is over is highlighted), and easily copy subterms from the output to a proof script.

Command generation for proof by pointing is usually specific to a particular logic in use, if we hope to generate a good proof command unambiguously for any particular click. However, Proof General could easily be generalised to offer the user a context-sensitive choice of next commands to apply, which may be more useful in practice, and a worthy addition to Proof General.

Implementors of new proof assistants should be encouraged to consider supporting term-structure mark up from the start. Command generation should be something that the logic-implementor can specify in some way.

Of the supported provers, we can certainly hope for proof-by-pointing support from Coq, since the CtCoq proof-by-pointing code has been moved into the Coq kernel lately. I hope the Coq community can encourage somebody to do this.

A.2 Granularity of atomic command sequences

This is a proposal by Thomas Kleymann for generalising the way Proof General handles sequences of proof commands (see Goal-save sequences in the user manual), particularly to make retraction more flexible.

The blue region of a script buffer contains the initial segment of the proof script which has been processed successfully. It consists of atomic sequences of commands (ACS). Retraction is supported to the beginning of every ACS. By default, every command is an ACS. But the granularity of atomicity should be able to be adjusted.

This is essential when arbitrary retraction is not supported. Usually, after a theorem has been proved, one may only retract to the start of the goal. One needs to mark the proof of the theorem as an ACS. At present, support for goal-save sequences (see Goal-save sequences in the user manual), has been hard wired. No other ACS are currently supported. We propose the following to overcome this deficiency:

proof-atomic-sequents-list

is a list of instructions for setting up ACSs. Each instruction is a list of the form (end start &optional forget-command). end is a regular expression to recognise the last command in an ACS. start is a function. Its input is the last command of an ACS. Its output is a regular expression to recognise the first command of the ACS. It is evaluated once and, starting with the command matched by end, the output is successively matched against previously processed commands until a match occurs (or the beginning of the current buffer is reached). The region determined by (start,end) is locked as an ACS. Optionally, the ACS is annotated with the actual command to retract the ACS. This is computed by applying forget-command to the first and last command of the ACS.

For convenience one might also want to allow start to be the symbol ‘t’ as a convenient short-hand for '(lambda (str) ".") which always matches.

A.3 Browser mode for script files and theories

This is a proposal by David Aspinall for a browser window.

A browser window should provide support for browsing script files and theories. We should be able to inspect data in varying levels of detail, perhaps using outlining mechanisms. For theories, it would be nice to query the running proof assistant. This may require support from the assistant in the form of output which has been specially marked-up with an SGML like syntax, for example.

A browser would be useful to:

Provide impoverished proof assistants with a browser
Extend the uniform interface of Proof General to theory browsing
Interact closely with proof script writing

The last point is the most important. We should be able to integrate a search mechanism for proofs of similar theorems, theorems containing particular constants, etc.

This document was generated on October 4, 2024 using texi2html 1.82.