[isabelle-dev] Timeouts in Flyspeck_Tame
makarius at sketis.net
Thu Feb 14 11:57:34 CET 2019
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
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 ...
More information about the isabelle-dev