[isabelle-dev] Timeouts in Flyspeck_Tame
makarius at sketis.net
Thu Feb 14 13:34:39 CET 2019
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.
More information about the isabelle-dev