Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.
On Tue, 10 Dec 2013, Makarius wrote:
From the empirical data that is available, we cannot draw such a
conclusion yet. There is merely an indication that it is probably better
not to smash flex-flex here, but some uncertainty remains.
Larry might have had very good reasons to smash the flex-flex pairs in
1998. These reasons might no longer apply, or the experiments so far did
not get to the point where the difference is visible.
Larry, can you give further hints about that?
Alternatively, someone else can volunteer to make further experiments on
all reachable Isabelle applications, to consolidate the empirical
findings. This will only take a few hours.
In particular the following questions are relevant:
* Do flex-flex pairs after invocation of blast actually happen in
practice, i.e. does blast proof reconstruction introduce any by
* Is there any performance impact on changing the behaviour? So far
the success or failure was not affected, but there were no
measurements of timing so far.
This archive was generated by a fusion of
Pipermail (Mailman edition) and