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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
