[isabelle-dev] Timeouts in Flyspeck_Tame
florian.haftmann at informatik.tu-muenchen.de
Thu Feb 14 12:04:04 CET 2019
>> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 228 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev