[isabelle-dev] Timeouts in Flyspeck_Tame

[Makarius]

On 14/02/2019 10:43, Florian Haftmann wrote:
> 
> But https://isabelle.sketis.net/devel/build_status/ still indicates
> failure for Flyspec-Tame from Wed 13th.  Is there any chance that some
> other non-termination proof requiring image_cong_simp [cong del] is
> still left in Flyspeck-Tame?

Maybe it is just a coincidence, it did work for Isabelle/18cb541a975f
vs. AFP/9181c1974aa0, but later failed again for AFP/e064b4022c1c -- see
also the "CSV" link on https://isabelle.sketis.net/devel/build_status

Later today we should get new measurements.


> Btw. that the ancient cond_eval hack has been replaced by a proper tag
> has completely slipped out of my attention, hence I didn't notice that
> Flyspeck-Tame is completely untested without very_slow.
> 
> At the moment I am thinking whether the old approach of checking
> everything except the computations can be restored without using fancy
> low-level stuff.  Maybe by a locale.

This is indeed a bit fragile. I used to make manual tests of
Flyspeck-Tame over some time, but now ignore that problem.

Several days of unclear situation is a natural consequence of this
arrangement.

Maybe it is possible to make a non-slow session "Flyspeck-Tame-Base"
that does everything except the actual "eval" steps, and postpone the
checks to session Flyspeck-Tame (very_slow) = Flyspeck-Tame-Base ...


	Makarius