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