Re: [isabelle] jEdit apparantly proves False



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.