[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