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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
