Miscellaneous feature wishes for discussion
Here is a small list of features I missed in Why3 1.0 for discussion:
- The error message
Error in transformation function: apply: there are N terms missing
would be vastly more useful if it included the names of theN
missing terms. Possible? - Applying a transformation with superfluous arguments or with missing keys (e.g.,
with
) results in the error messagesFirst arguments were parsed and typed correctly but the last following are useless:
, which is not fully clear. MaybeThe last N arguments are not applicable (or did you miss a keyword?)
? - When trying to apply a transformation a second time, the IDE only prints message
Transformation already applied
. The IDE could additionally jump to the corresponding VC as if the transformation was applied for the first time. - Reloading (
C-r
) is slow for large files (>1k lines), also when they contain parsing/typing errors. (Errors are detected quickly in large files bywhy3 prove
.) Could the IDE check for errors before spending a lot of time on other tasks? - After verifying one VC the IDE jumps to the first unverified VC in the module. It would be more intuitive if it jumped to the next unverified VC (or not at all)
- The following syntax would be useful
fun (x, y) -> ...
- The following syntax would be useful in
inductive
:let (x, y) = ...
(it currently causes the errorIll-Formed inductive clause ...
butlet xy = ...
is OK) - Propagate small dot-symbol of previously succeeded but outdated proofs to the VC
- Focus/Unfocus should be under menu View not Tools
- Keyboard shortcuts to jump between commands and tree
- A table of content for generated documentation (
why3 doc
) including headings{N ...}
whould be useful to navigate in large files.