Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



I can't imagine a situation where I would like Isabelle/jEdit to recover from a syntax error by ignoring a single show command. I'd rather expect it to ignore everything from the syntax error until the next "save" place e.g. a theorem.

I'm also very much against the "insert a sorry" approach. I'd embrace an "oops" version discarding the last goal.

Best
    Benedikt

Am 22.04.14 13:36, schrieb Lawrence Paulson:
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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.