Re: [isabelle] jEdit apparantly proves False



It seems to work with any diverging command, not only simp.

Thus, a minimal example is to type

  lemma False by (intro TrueE) <RETURN>

and after you typed RETURN, the thing appears proven in jEdit.


-- Peter

On Di, 2013-11-19 at 21:53 +0100, bnord wrote:
> Hi,
> 
> I can reproduce this easily on OS X and Windows with Isabelle2013-1.
> Any edit after the non terminating command suffies, no saving or waiting 
> required.
> So if one, in good hope, simply presses return, after the command was 
> dispatched, the markup disappears and the command seems to be fine.
> Very nasty. ;) Couldn't reproduce it with Isabelle2013.
> 
> Best
>      Benedikt
> 
> Am 19.11.2013 13:40, schrieb Peter Lammich:
> > Hi all,
> >
> > while giving a tutorial on Isabelle, I run into the following strange
> > effect, where jEdit seems to indicate that a lemma is proven. Actually,
> > the lemma just contains a diverging method invocation. See screenshot.
> >
> > To reproduce this behaviour, just load the attached theory file, wait a
> > few seconds (the simp add: A A[symmetric] is marked purple now). Then
> > move the cursor after the lemma and type some newlines, save the file,
> > and you get (on my machine) the above effect. You can even use the lemma
> > to prove further non-theorems from it without any problems!
> >
> > --
> >    Peter
> >
> > p.s.
> >    As I can see from some homework submissions, some of our students seem
> > to run into this effect regularly when solving homeworks :(
> >
> > pps:
> >   Thm.peek_status @{thm f} returns
> >    val it = {failed = true, oracle = false, unfinished = false}:
> >     {failed: bool, oracle: bool, unfinished: bool}
> >
> >
> 






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