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
and placed the cursor at $, then opened Query/Find theorems and searched for
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