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

lemma shows False


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.


isabelle-dev mailing list

Reply via email to