Am 14.02.19 um 13:34 schrieb Makarius: > 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.
See now https://bitbucket.org/isa-afp/afp-devel/commits/00b771f6c60d99745fb933d4043c1ed123a427e5 Florian
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev