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.