Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- To: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>
- Subject: Re: [isabelle] Isabelle2014-RC2: PIDE does not resume processing
- From: Makarius <makarius at sketis.net>
- Date: Wed, 8 Oct 2014 22:51:08 +0200 (CEST)
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <email@example.com>
- References: <53E4C786.firstname.lastname@example.org> <alpine.LNX.email@example.com> <alpine.LNX.firstname.lastname@example.org> <53E9F7D1.email@example.com> <alpine.LNX.firstname.lastname@example.org> <alpine.LNX.email@example.com> <53EC4820.firstname.lastname@example.org> <alpine.LNX.email@example.com> <firstname.lastname@example.org>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
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
(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
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 ...
This archive was generated by a fusion of
Pipermail (Mailman edition) and