Re: [isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
On Mon, 3 Dec 2012, Makarius wrote: On Tue, 13 Nov 2012, Lars Noschinski wrote: Hi, sometimes, I am encountering some erraneous behaviour of qed when a structured proof contains some facts for which the final by step failed. Before the closing block the output buffer reads: goal: No subgoals! But qed then fails with an error message: Failed to finish proof: goal (4 subgoals): {(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG 1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) The subgoals in this message are the remaining goals of a failed qed-step earlier in this proof. This is probably an effect of the implicit propagation of exceptions between task groups, which is essential in batch mode to get all exceptions together in the end. Here it gets in the way, because the hopping of failures from one task to another duplicates them in the document view. I have made some iterations on it leading up to Isabelle/a7484a7b6c8a, so there is a chance that it works smoothly for the release. There is some danger here of provoking odd effects, like loosing errors that are not officially identified by the position information of the document model. Please keep an eye on it for the coming release. Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
On Tue, 13 Nov 2012, Lars Noschinski wrote: Hi, sometimes, I am encountering some erraneous behaviour of qed when a structured proof contains some facts for which the final by step failed. Before the closing block the output buffer reads: goal: No subgoals! But qed then fails with an error message: Failed to finish proof: goal (4 subgoals): {(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG 1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) The subgoals in this message are the remaining goals of a failed qed-step earlier in this proof. This is probably an effect of the implicit propagation of exceptions between task groups, which is essential in batch mode to get all exceptions together in the end. Here it gets in the way, because the hopping of failures from one task to another duplicates them in the document view. I need to rethink this (again+). Makarius___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
Hi, sometimes, I am encountering some erraneous behaviour of qed when a structured proof contains some facts for which the final by step failed. Before the closing block the output buffer reads: goal: No subgoals! But qed then fails with an error message: Failed to finish proof: goal (4 subgoals): {(x, w), (y, w), (w, x), (w, y)} ⊆ edges sG 1. (x, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 2. (y, w) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 3. (w, x) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) 4. (w, y) ∈ edges (Abs_graph (insert w (verts G), insert (x, w) (insert (w, x) (insert (w, y) (insert (y, w) (edges G - {(x, y), (y, x)}, fst, snd)) The subgoals in this message are the remaining goals of a failed qed-step earlier in this proof. No minimal example yet, I might be able to produce one later this week, if Makarius does not already now what happens here. -- Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev