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



On Tue, 16 Sep 2014, Andreas Lochbihler wrote:

Today, I experienced a PIDE greyout again, this time in Isabelle2014 while running quickcheck. I've attached the Syslog content and the output of error messages in the terminal from which I had started Isabelle/jEdit.

(This thread is already quite old, but not forgotten. After several weeks I am back to normal network connectivity, to make a clean sweep ...)

Do you remember anything specific about the situation? E.g. a very big message being output, say a large subgoal?

The bash output looks like a stack-overflow in isabelle.Protocol.clean_message, although the trace is truncated and the exception header is missing.


The JVM is very unflexible in thread stack management: the value given on startup is taken for all newly created threads, and cannot be changed at runtime. This makes it hard to guess right once and for all, and for everyone.

The Isabelle/jEdit settings have these defaults for heap and stack:

  JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"

I am using myself this one on a modest 8GB 64bit machine:

  JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"

Bigger machines should easily afford -Xss8m or more.


Oracle basically ships a Harley-Davidson -- it requires a lot of polishing and handywork from the power-user.

David Matthews provides more flexibility in Poly/ML: the stack can grow dynamically to some GBs, but even then it is possible to drive the system to the limits ...


	Makarius





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