[isabelle-dev] NEWS: sightly more parallel checking

[Fabian Immler]

> Am 05.06.2018 um 13:39 schrieb Makarius <makarius at sketis.net>:
> 
> On 04/06/18 20:17, Fabian Immler wrote:
>> 
>> This "something in the background" appears to happen on a regular basis:
>> every 2-3 seconds, the poly process consumes 200%CPU for about a second.
>> poly should be idle (or used to be in such a situation) because (as far
>> as I can tell) nothing else (e.g., sledgehammer, find theorems) seems to
>> be active.
> 
> This is probably due to the implicit "consolidation" of finished
> theories, which I have made a bit more official as PIDE document edit
> (see Isabelle/09ac56914b29). That is important, because of the final
> "presentation", e.g. for generated LaTeX.
> 
> In Isabelle/38272f9481c2, I have also changed the delay from 1s to 2.5s
> -- you can make this 10s or more until I figure out a way to reduce the
> impact of it.
Thanks, this really seems to be the "consolidation": I can see the effect of chainging editor_consolidate_delay.

>> 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.

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/ebe76ebf/attachment.bin>