Dearest developers,
I have been answering questions of a novice Isabelle user over email, and we
encountered a situation that can be perceived as a soundness issue (it isn't)
and that I think can be easily helped through slightly more helpful error
messages plus an extra check, and it may make a big difference to newcomers, I
think. I'll describe the behaviour first (of both Isabelle and the user), and
my suggested fix second.
The user wrote a script that ended with some false lemma (without proof),
here's the script simplified for brevity:
theory Scratch imports HOL
begin
lemma shows False
end
Now Isabelle complains about the 'end': 'Illegal application of proof command
in "prove" mode'. The user responded by removing the 'end' at the end of the
file. Now Isabelle did not complain anymore.
At this point, the user called me to ask me what Isabelle's proof of the lemma
was, since he wasn't able to reproduce the proof (of a false statement) on
paper. In other words: the user believed that Isabelle had proved the lemma
(since Isabelle did not complain). The user understands that 'build' should be
the final test of correctness, but I do not wish to discourage the user from
using the nice jEdit interface this way.
My proposed solution:
- The 'Illegal application of proof command in "prove" mode' should better
explain the issue. Perhaps it could mention that 'end' is not expected until
the proof of the lemma is completed.
- When 'end of file' is encountered while in "prove" mode, there should be some
error as well.
I hope these are easy fixes (if not, never mind and sorry for the noise!), and
I think they can be a great help for novices.
Best,
Sebastiaan
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
