GUIWishes

Wish list for graphical user interfaces

See also CoqIDEWishes.

Please complete or add comments or add stars "*" to vote for features.

Proof development

• Proof-by-pointing features (Pcoq's spirit) using right-clic:
  • right-clicking on constants would propose "unfold",
  • moving equality statements in hypothesis to goal or other hypothesis with a left or right move would rewrite the given hypothesis,
  • selection of subterms by clicking on main symbol or by full selecting?
  • ability to mark hypotheses to which the next induction will apply
  • ...
• Support for easy goal switching?
• Automatically expand unnamed intros into intros with explicit names

Debugging

• Allow partial evaluation of ; sequences as in Matita : for example evaluating only T1;T2 in the sequence T1;T2;T3 without writing T1;T2. T3 (note: available in the Ltac debugger for CoqIDE).
  • could be a switchable option, useful for debugging complex proof scripts.
  • what about other tacticals?

Editing

• Use tab to indent proofs
• Globally rename all occurrences of an identifier (taking care of qualification)
• Support for easy selection of expressions (definitions, terms, subterms, identifiers...)?
  • could be a separate view (see below)
  • pcoq can do this
  • Alfa ancestor of Agda 1 also did this: it's deeply integrated with its natural language support.

Project development

• Automatically compile .v if necessary when 'Require' are evaluated
• One-click full project compilation with jump to next error and jump to next warning

Querying information

• A graphical advanced search windows for driving SearchAbout.
• Support for queries by right-clicking constants or selected expressions? what about a tooltip (if you keep the pointer on a constant more than 3 seconds, it displays its type, definitions...)
• Key or right-click for making explicit hidden information (coercions, implicit arguments, notations, ...) on selected subterms.
• Jump to definition (then jump back)

Rendering / views

• Reflect the tree structure of the proof into a tree widget to allow hiding parts of the proof.
  • most procedural proof scripts don't have much of a tree structure. does this apply to proof-terms, declarative proofs or what?
• Support for natural language explanations in proofs?
  • useful for beginners
  • coq 6.* and pcoq had this
  • alfa integrated this with support for 2D views
  • declarative proofs may make this unnecessary
    • but need some means of converting from proof terms (Matita does this) or procedural proof scripts
  • drawback: full natural-language proofs quickly become overwhelming
    • Alfa supports hybrid representation: use symbols for low-level manipulation, natlang for the higher-level structure

Graphical notations

• Support for 2-dimension notations?
  • pcoq and alfa/agda1 have some support for this
  • as a convention, every notation of the form ^* could be written as an exponent and every part of an ident ended by _digits or

Links

• Diagram representation in Penrose
• Structured editing in Deuce
• The SerAPI library for machine-to-machine interaction with Coq