<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;">I have no idea whether this is related, but I noticed some strange behaviour after updating to Isabelle/6989752bba4b (from some version about one or two weeks ago):<div class=""><br class=""></div><div class="">Sometimes, during interactive proof development, the poly process appears to be doing something in the background even when (as far as I can tell) it should be idle. This makes the IDE less responsive.</div><div class=""><br class=""></div><div class="">This "something in the background" appears to happen on a regular basis:</div>every 2-3 seconds, the poly process consumes 200%CPU for about a second.<div class="">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.</div><div class=""><br class=""></div><div class="">The only way to stop this apparently is to invalidate something in the beginning of the (currently open) theory.</div><div class=""><div class=""><br class=""></div><div class=""><div class="">Also the Monitor panel looks like something is going on in the background (see the attached screenshots).</div><div class="">Reprocessing the whole theory (by invalidating something in the beginning) makes the behaviour disappear.</div><div class=""><br class=""></div><div class="">Any ideas what might be going on there? Does anyone else experience this behavior?</div><div class="">How I could debug this when I encounter it the next time, e.g., how to figure out what poly (or perhaps also PIDE) is doing or is trying to do in the background?</div><div class=""><br class=""></div><div class="">I am not sure how to reproduce this, but it happens every hour or so during interactive proof development (i.e., many edits in the document model, nonterminating proof methods behind the current edit).</div><div class=""><br class=""></div><div class="">Fabian</div><div class=""><br class=""></div><div class=""><img apple-inline="yes" id="AB8310C8-DCB6-4088-AFE2-4B5F94570022" src="cid:84FE716F-9723-4F7C-983F-B49EC9AB3D9B@informatik.tu-muenchen.de" class=""><img apple-inline="yes" id="44657995-7F44-4BB2-93CB-3E18592201C0" src="cid:81F0C76F-E42A-40BC-BB90-98C987F315B5@informatik.tu-muenchen.de" class=""><img apple-inline="yes" id="87A0B97C-DC1E-4400-B6B8-92543D94836F" src="cid:EFAE14F5-04B0-42FB-83EB-E6314C580BC8@informatik.tu-muenchen.de" class=""><img apple-inline="yes" id="8CC1681E-E225-498E-B138-F00681898908" src="cid:67B4E1D0-5B93-4A94-831F-542445B0710E@informatik.tu-muenchen.de" class=""><img apple-inline="yes" id="364925D0-577F-416E-A66B-148A8F2D2B50" src="cid:DA82F946-09C3-4E54-A190-C5A15CF24BF9@informatik.tu-muenchen.de" class=""><img apple-inline="yes" id="4A856DB7-5ED4-4A26-BF48-BC89BE52E040" src="cid:230904EE-FA1E-487B-A3D7-3D7CFCF28CA2@informatik.tu-muenchen.de" class=""></div><div class=""><div class=""></div><br class=""><blockquote type="cite" class="">Am 03.06.2018 um 22:45 schrieb Makarius <<a href="mailto:makarius@sketis.net" class="">makarius@sketis.net</a>>:<br class=""><br class="">*** Isabelle/jEdit Prover IDE ***<br class=""><br class="">* Slightly more parallel checking, notably for high priority print<br class="">functions (e.g. State output).<br class=""><br class=""><br class="">This refers to Isabelle/b00b40dc41af -- with various fine points in the<br class="">organization of PIDE execution forks, not just the preceeding cd387c55e085.<br class=""><br class="">As we are heading towards the release, it is important to keep an eye on<br class="">the system, that everything works smoothly. I will try not to touch more<br class="">such delicate points of PIDE document processing.<br class=""><br class=""><br class=""><span class="Apple-tab-span" style="white-space:pre"> </span>Makarius<br class="">_______________________________________________<br class="">isabelle-dev mailing list<br class=""><a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class=""></blockquote><br class=""></div></div></div></body></html>