Re: [isabelle] New error messages in Isabelle 2013

On Mon, 21 Jan 2013, Alfio Martini wrote:

Maybe it is just me, but I still get confused by the new error messages in Isabelle 2013. Of course, it is already a big improvement over simply "failed to finish proof" from Isabelle 2012.

Is my confusion justified?

There were no reactions so far, so maybe nobody else has tried it yet.

This refinement of error messages was the result of myself using the system over 1-2 weeks to prepare some Isabelle tutorial last October. At some point I got tired of looking up the Output again and again. Instead it is now possible to do quite a lot of proofs right there in the text, without peeking at the goal state. You just hover over the red squiggles of the failed proof methods and immediately see what happened. This is escpecially relevant for structured Isar proofs.

Output and goal states are not fully obsolete yet, but it is one more step to overcome them.

For instance, the success of establishing a "have" or a "show" is usually
show in the output window
with a message like "have fact"  " show fact ... successful attempt to
solve goal by exported rule"

Now, when there´s a failure, the error message is still prefixed in the
output window by the
very messages we get when we are successful, as mentioned above. Besides in
the error case, the
output window also show after the error message that there are no subgoals

I attach two images to make my point clearer.
In this particular example, if the error message was not prefixed by
"Successful attempt ...", I think it would
be much better.

There are several things being mixed up in the all-inclusive Output window. The "Successful attempt" is just a preview of the attempt to apply the command, stemming from old TTY-times. It is more and more getting in the way.

Also note that there is some non-determinism stemming from the fork of 'by' steps that is now enabled by default, cf. NEWS. That sometimes leads to nice top-down checking of proof outlines, where the system jumps over failed justification. Sometimes this does not work, due to bad timing, and the proof text produces a lot of structural errors about displaced qed after a failed sub-proof.

There might be also some genuine problems in the RC1 snapshot left. Just the week before making it, I had to rework the error reporting once more to avoid duplication of errors from one 'by' step to another 'by' step.

I will myself look again if it is as right as possible right now, unless someone else points directly to remaining drop-outs.


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