Re: [isabelle] Feature suggestions: More useful output

On Fri, 23 Nov 2012, Joachim Breitner wrote:

Another error that could be make more helpful is “Unknown fact "..."”.
Often I don’t remember the name of a lemma exactly – was it set_finite
or finite_set? I then have to fire up "find_theorems name:..", which is
quite a bit of typing.
GHC recently has started to give spelling corrections (the 10 best fits
based on edit distance, IIRC) for every kind of unknown-something error.
If Isabelle could do the same, this would be great. I’d imagine that in
the context of Isabelle lemmas the edit distance should give special
treatment to reordering the parts of the string that are separated by
‘_’, as it is often the order of the components of the name that I fail
to remember, and count that as one step.
I guess Isabelle usually has many more lemmas in scope than GHC has
functions and this might be a bit slow. But the output does not have to
be generated at once and if the error message is printed before the list
is calculated, this should not harm anyone.²

Sounds like the GHC guys have 10 times more resources to spend. There are many ideas about formal entity lookup in the pipeline, including context-sensitive completion, but nothing like the above so far.

Ask again after some more years of Isabelle/jEdit Prover IDE development.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.