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

On Tue, 12 Aug 2014, Andreas Lochbihler wrote:

The greyout happened again (with Isabelle2014-RC3). This time, I had typed

thm $

and placed the cursor at $, then opened Query/Find theorems and searched for simp_implies.

I've attached the activity log and the output of the syslog. The Prover.echo command still works. There are no exceptions in the shell from which I have started PIDE.

Thanks for continued testing.

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.

We somehow need to get to the bottom if it. Such problems are sometimes hardware specific, but if we are lucky it is just a soft mistake in my own machine room of Isabelle/ML.

Can you just continue testing with threads_trace = "5" in $ISABELLE_HOME_USER/etc/preferences? You need to edit that file offline, while Isabelle/jEdit is not running. That option will produce massive amounts of tracing information for syslog, but while the panel is *not* open the performance hit should be bearable. Once the greyout happens again, you open an instance of the panel and look at the tail end of the last 100 messages.


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