*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] jEdit apparantly proves False*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 19 Nov 2013 16:54:27 +0100*In-reply-to*: <1384875857.7447.122.camel@lapbroy33>*References*: <1384864829.7447.117.camel@lapbroy33> <1384875857.7447.122.camel@lapbroy33>

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

**References**:**[isabelle] jEdit apparantly proves False***From:*Peter Lammich

**Re: [isabelle] jEdit apparantly proves False***From:*Peter Lammich

- Previous by Date: Re: [isabelle] jEdit apparantly proves False
- Next by Date: Re: [isabelle] Code_String: linorder in String.literal
- Previous by Thread: Re: [isabelle] jEdit apparantly proves False
- Next by Thread: Re: [isabelle] jEdit apparantly proves False
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list