[isabelle-dev] Timeouts in Flyspeck_Tame

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20190216/b72d1317/attachment.sig>