Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing

Hi Makarius,

Today, I experienced a PIDE greyout again, this time in Isabelle2014 while running quickcheck. I've attached the Syslog content and the output of error messages in the terminal from which I had started Isabelle/jEdit.

Hope this helps in narrowing down the problem,

On 18/08/14 13:35, Makarius wrote:
On Thu, 14 Aug 2014, Andreas Lochbihler wrote:

I opened Raw Output after the greyout. I'll keep Raw Output open the whole time when I
continue testing.

>  The Prover.echo command still works.

Some days ago, I've run myself into a situation of permanent "PIDE greyout" while editing
some ML files within Isabelle/HOL, which automatically means it is under heavy load,
because of the immense size of that session. This was presumably due to a Document.update
protocol crash, but I did not have the Raw Output panel open to confirm it. The
Prover.echo protocol command still worked afterwards.

For the next release candidate, which will be published later today, I have made an end to
this game: PIDE protocol exceptions will be part of the buffered syslog channel.  Thus
they can be retrieved later, in the rare situations when such a breakdown happens.

Moreover, I have made two rounds through the sources, to see where such a crash can happen
theoretically.  I found nothing particular about query commands, but the protocol for PIDE
document "garbage collection" had a weakness stemming from its first implementation 3
years ago: depending on timing, it was possible to have the ML process refer to undefined
items and thus crash.

My own crash of ML blob editing fits exactly into this pattern, although I could not
reproduce it systematically.  The query crash might be the same or something different.
If something like that ever happens again (after Isabelle2014-RC4), it is important to
preserve the content of the Syslog panel afterwards and show that to me.


Description: Zip archive

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.