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