*To*: bnord <bnord01 at gmail.com>*Subject*: Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 22 Apr 2014 12:36:51 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <53564C5E.2070900@gmail.com>*References*: <53564C5E.2070900@gmail.com>

Without reopening the “what is a bug” debate, I need to say that this sort of thing is inevitable with the approach taken by Isabelle/jEdit, in attempting to process everything, parsing errors and all. If you type in a syntactically incorrect proof, it tries to recover as best it can. In this case, it ignores the syntactically incorrect “show” command, causing the behaviour you observe. An alternative would be to silently insert “sorry” in order to complete the previous proof, preventing that behaviour but having other undesirable consequences. The best overall approach to all such situations is to fix syntax errors as soon as they are flagged. If I am working on a proof and notice that processing power is being wasted processing some proof text down below, I delete or disable this material. Inserting “sorry” beforehand should always do the trick. Needless to say, your work isn't done until every “sorry” has been removed again. Larry Paulson On 22 Apr 2014, at 12:02, bnord <bnord01 at gmail.com> wrote: > I'd expect the following issue to be well known but didn't find it in the "known issues". > > When inserting a new goal (have ...) into a proof, proof methods belonging to later goals seem to be applied wrongly sometimes causing them to loop and make my PC noisy after a while. ;) > > Here's a small example: > > lemma assumes "m ∈ M" and "M ⊆ N" shows "m ∈ N" proof - > have P(* incomplete goal *) > show "m ∈ N" using assms by (metis in_mono) (* loops *) > qed > > The "show" already produces a syntax error but the later "by" is applied anyhow yet to the wrong goal causing it to loop. > > A student of mine is highly skilled in producing such situations in many theorems simultaneously causing the editor to become very unresponsive. > > Best Benedikt >

**Follow-Ups**:

**References**:

- Previous by Date: Re: [isabelle] few questions about Isabelle/jEdit
- Next by Date: Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
- Previous by Thread: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
- Next by Thread: Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
- Cl-isabelle-users April 2014 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