On 14/02/2019 12:04, Florian Haftmann wrote: >>> 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. >> >> 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 ... > > Something like that indeed. A completeness proof relative to a locale > which has the computational results as assumption apt for later > interpretation.
In contrast to my proposal concerning Flyspeck-Tame-Base it is better to keep the main AFP document unchanged, e.g. like this: session Flyspeck-Tame-Eval (very_slow) = Flyspeck-Tame + ... This will change the timing for Flyspeck-Tame in the recorded database, but such renamings occasionally happen over the years. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev