[isabelle-dev] jEdit: Inconsistent behaviour with skipped by-proofs
Makarius
makarius at sketis.net
Mon Dec 3 12:28:51 CET 2012
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
More information about the isabelle-dev
mailing list