This is the continuation / conclusion of the pending thread about flexflex
pairs in blast, see also
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-December/msg00085.html
In Isabelle/b45b1b217f43 from 01-Jan-2014 the smashing of flexflex pairs
is already removed, just like for any other proof tools. The general idea
is that global goal information like maxidx and flexflex pairs (called
tpairs internally) accumulates monotonically, without any premature
censorship by proof tools. Instead the cleanup is deferred to certain
checkpoints of the system infrastructure, e.g. the goal wrappers
Goal.prove or goals in Isar proof text.
Here is also an exhaustive list of places where flexflex pairs accumulate
in practice due to "blast" (or indirectly via "auto"):
Isabelle/9a52ee8cae9b
AFP/4fbb736e4e28
(line 99 of "~~/src/HOL/Cardinals/Wellorder_Embedding.thy")
(line 406 of "~~/src/HOL/Library/Ramsey.thy")
(line 408 of "~~/src/HOL/Library/Ramsey.thy")
(line 318 of "$AFP/Markov_Models/ex/PCTL.thy")
(line 1162 of "$AFP/Nat-Interval-Logic/IL_TemporalOperators.thy")
(line 376 of "$AFP/Stuttering_Equivalence/PLTL.thy")
(line 384 of "$AFP/Stuttering_Equivalence/PLTL.thy")
(line 534 of "$AFP/Stuttering_Equivalence/PLTL.thy")
These incidents are rather unexciting. I have occasionally seen other
proof tools like "fast" produce spurious flexflex pairs as well, without
doing any immediate harm.
I was about to push b45b1b217f43 already last year, but it was delayed by
mysterious total failure of existence of the test environment for
JinjaThreads. It is still unclear what actually happened. It might have
been just due to extra tracing messages emitted in the test, which are
occasionally deadly as we know already. JinjaThread has always defined
the edge of what is possible at all, and thus might occasionally fall off
that edge.
So for my part, this thread can be closed now.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
