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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
