GUIWishes - coq/coq GitHub Wiki
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