Re: [isabelle] New error messages in Isabelle 2013



Hi Makarius.

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.


This is great. I did not know that. I am probably being very naive here (to
put it mildly), but what appears in the
window that pops up when you hover over the red squiggles is what I would
expect to appear
in the output window as well (see image attached) .

Best!
On Fri, Jan 25, 2013 at 2:22 PM, Makarius <makarius at sketis.net> wrote:

> 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愀 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.
>
>
>         Makarius
>



-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil

Attachment: hover-error-message.PNG
Description: PNG image



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