[isabelle-dev] Timeouts in Flyspeck_Tame

[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.


	Makarius