Future enhancements of Proof General Eclipse (Wish List)

This page is for gathering ideas for improvements to Proof General Eclipse. The ideas here are for user-oriented improvements to help the proof development process. See also:

• PGEclipsePlans - concrete plans for what we want to do next, with implementation remarks
• ProofEngineering - a line of research on proof development building on and extending successful techniques from Software Engineering
• The Proof General Trac which has low-level project management details

General IDE improvements in current system

Incremental parsing

• Parsing should occur incrementally on user idle time, in the background. Parse errors should be indicated with wavy lines.

Decorators for documents

• Decorators for errors and warnings should be used

Indication/control of active proof script document

• Make title in editor bold, perhaps?
• An action to take user to active proof script document
• The toolbar button for switching the active script is maybe not needed: or at least, its action can be automatically triggered with other buttons often

Evolutionary developments

Connections with other systems

IsaPlanner interface

IsaPlanner would benefit from interface support within Proof General. We need to design PGIP extensions to support it and tools like it.

Proof development wizards

Simple wizards based on templates for files would be easy. Examples: what Coq uses in the current PGEmacs, or what the Texlipse plugin uses for LaTeX documents.

Proof build mechanisms for batch mode processing

Not all theorem provers are interactive, and interactive systems also usually support a batch mode of operation (i.e. non-interactive "compilation" of a whole development). Batch processing should be supported using the standard Eclipse mechanisms for building.

Ideally it should be combined with interactive mode, so that a failure in a batch check invokes ordinary script management as if it were a debug view.

At the moment PGIP doesn't consider batch checking at all.

Revolutionary developments

Most of these ideas require further research. Some of this fits into the ProofEngineering plan.

Refactoring

Simple examples: changing definition or lemma names, moving proofs and theory steps around. Hopefully possible at a generic level. Richer examples, e.g. changing representations, require further research.

Proof development patterns

Literate and "document-centred" development

Visual browsing/design of theories

One of the ProofEngineering ideas is to support visual construction and browsing of theories. We plan research into a graphical language for doing this, inspired by (or incorporating) existing work such as IsaPlanner's hiproof navigator.