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

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.


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