[isabelle-dev] NEWS: sightly more parallel checking

[Makarius]

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.


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


	Makarius