[isabelle-dev] NEWS: sightly more parallel checking
Makarius
makarius at sketis.net
Tue Jun 5 14:47:56 CEST 2018
On 05/06/18 14:45, Fabian Immler wrote:
>
>
>>> The only way to stop this apparently is to invalidate something in the
>>> beginning of the (currently open) theory.
>>
>> It should be possible to achieve this effect by removing the concluding
>> 'end' command.
> Just now I was in the middle of a theory (without any 'end' command), where every (are they supposed to happen periodically?) "consolidation" took about 4 seconds.
>
> It seems like something is accumulating somewhere when editing the document, because after invalidating the beginning of the theory and going back to the same place as before, the "consolidation" was not noticeable any more.
What kind of theory is this? Many commands? Long-running /
non-terminating commands?
Makarius
More information about the isabelle-dev
mailing list