Re: [isabelle] jEdit apparantly proves False



To be more precise: On my machine, the time required until the command
appears as processed is, nondeterministically, something between a few
seconds (!) and a few minutes, so it is almost impossible to distinguish
a long-running method-invocation from a diverging one.

--
  Peter

On Di, 2013-11-19 at 16:44 +0100, Peter Lammich wrote:
> Another, even nastier, way to reproduce this behaviour:
> 
> Load the theory and wait some time (a few minutes or so),
> then the purple mark goes away automagically.
> 
> This is confusing, in particular if you use some long-running proof
> methods or switch to another workspace while your proofs run through ...
> if you return to jEdit after a few minutes, it seems as everything went
> through.
> 
> --
>   Peter
> 
> 
> 
> On Di, 2013-11-19 at 13:40 +0100, Peter Lammich wrote:
> > 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.