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
    itself?

  * 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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.