[isabelle-dev] NEWS: sightly more parallel checking

[Fabian Immler]

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):

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.

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.

The only way to stop this apparently is to invalidate something in the beginning of the (currently open) theory.

Also the Monitor panel looks like something is going on in the background (see the attached screenshots).
Reprocessing the whole theory (by invalidating something in the beginning) makes the behaviour disappear.

Any ideas what might be going on there? Does anyone else experience this behavior?
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?

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

Fabian



> Am 03.06.2018 um 22:45 schrieb Makarius <makarius at sketis.net>:
> 
> *** Isabelle/jEdit Prover IDE ***
> 
> * Slightly more parallel checking, notably for high priority print
> functions (e.g. State output).
> 
> 
> This refers to Isabelle/b00b40dc41af -- with various fine points in the
> organization of PIDE execution forks, not just the preceeding cd387c55e085.
> 
> As we are heading towards the release, it is important to keep an eye on
> the system, that everything works smoothly. I will try not to touch more
> such delicate points of PIDE document processing.
> 
> 
> 	Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180604/4e3dade2/attachment-0002.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Bildschirmfoto 2018-06-04 um 18.38.10.png
Type: image/png
Size: 84086 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180604/4e3dade2/attachment-0012.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Bildschirmfoto 2018-06-04 um 18.33.14.png
Type: image/png
Size: 79016 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180604/4e3dade2/attachment-0013.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Bildschirmfoto 2018-06-04 um 18.33.08.png
Type: image/png
Size: 40846 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180604/4e3dade2/attachment-0014.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Bildschirmfoto 2018-06-04 um 18.32.57.png
Type: image/png
Size: 65327 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180604/4e3dade2/attachment-0015.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Bildschirmfoto 2018-06-04 um 18.32.36.png
Type: image/png
Size: 130480 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180604/4e3dade2/attachment-0016.png>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: Bildschirmfoto 2018-06-04 um 18.32.27.png
Type: image/png
Size: 106482 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180604/4e3dade2/attachment-0017.png>
-------------- 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/20180604/4e3dade2/attachment.bin>