[isabelle-dev] NEWS: sightly more parallel checking

[Fabian Immler]

> Am 05.06.2018 um 14:47 schrieb Makarius <makarius at sketis.net>:
> 
> 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?
In this particular case, it was a relatively short theory (300 lines) with no long-running or non-terminating commands. I inserted and removed some diagnostic commands (code_thms, export_code foo in SML), but those were not present anymore when I observed this 4-second-consolidation-loop.

Fabian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5451 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180605/e6765c18/attachment.bin>