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
signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
