[isabelle-dev] Timeouts in Flyspeck_Tame

[Florian Haftmann]

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

	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/20190214/3e453ff0/attachment.sig>