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



Hi Makarius,

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

Andreas

On 13/08/14 17:28, Makarius wrote:
On Wed, 13 Aug 2014, Makarius wrote:
Looking at the results, I would say there is a deadlock in the main Document.update
operation -- as you have pointed out earlier that the CPU use of the poly process is 0.

That conclusion is actually too quick, because it is in conflict with the following
observation:

   > The Prover.echo command still works.

On the other hand ...

   > There are no exceptions in the shell from which I have started PIDE.

but the latter refers to JVM exceptions.

If Prover.echo still works after the greyout, the protocol thread is alive and not
dead-locked.  The abrupt end of the syslog after Document.update could also mean that it
just crashed, but then we need to see ML exceptions on Raw Output.  The latter is
unbuffered, though.  Did you have Raw Output open *before* the incident?


     Makarius




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