[isabelle-dev] Request for parser

[Sebastiaan Joosten]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20180312/4b91a3c5/attachment.html>