Re: [isabelle] New error messages in Isabelle 2013



> 
> 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) .

I agree with Alfio. When I write proofs, I usually do this
incrementally. If, at some point, I type eg
  have foo by auto
and the proof method fails unexpectedly, I would like to immediately see
why, without moving my arm from the keyboard to the mouse, hover the
mouse over the text and wait for the popup.

Still, this feature is better than what we have in the 2012-version,
where you had to go back to the "by" and change it to an apply, just in
order to see the remaining subgoals in the output buffer.

Best,
  Peter




> 
> 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
> >
> 
> 
> 







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