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