Re: [isabelle] jEdit apparantly proves False

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


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.