Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.
On Wed, 11 Dec 2013, Makarius wrote:
Anyway, after heating my office with more CPU power (running Isabelle +
AFP + IsaFoR a few times), I have the impression that there is nothing
to see on this thread, and we can just move on. This means we can
probably remove the extra clean-up step from blast in coming Isabelle
Further explanations when the current build has terminated ...
There were various delays, failures, non-termination, but mostly due to
other reasons. We have again a situation where AFP feels very "heavy"
(even on 8 cores), and the many repository clones and branches sometimes
cause confusion what needs to be tested.
Anyway, according to the current situation in Isabelle2013-2, there are
merely these few spots where flexflex-pairs occur and blast smashes them:
(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/thys/Markov_Models/ex/PCTL.thy")
(line 376 of "$AFP/thys/Stuttering_Equivalence/PLTL.thy")
(line 534 of "$AFP/thys/Stuttering_Equivalence/PLTL.thy")
All of these are harmless. Doing nothing about flexflex pairs within
blast means they are smashed a bit later at the end of the proof, as
I've recently seen other proof tools like "fast" introducing left-over
flexflex pairs, but the only problem was some divergence in the enclosing
goal infrastructure, where they were treated non-uniformly by accident.
So it looks like the global flexflex context of a goal state (the
"tpairs") is best left alone by regular proof tools. They just accumulate
monotonically like maxidx, and final results are somehow standardized by
the system infrastructure.
Thus tools that do require pending fleflex constraints to work, will have
We should try that, but of course observations might change again in the
coming months before the next release.
This archive was generated by a fusion of
Pipermail (Mailman edition) and