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

On Thu, 9 Oct 2014, Andreas Lochbihler wrote:

On 08/10/14 22:51, Makarius 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.

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

No, everything was quite small, actually. At that time, I was preparing exercises for the Isabelle course at ETH, so I just had a single theory file based on HOL/Main, and quickcheck normally outputs only small counterexamples.

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

    JEDIT_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss2m"
    JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"

I had the -Xmx4096m option set before, but I will now also adapt your settings for -Xss and -Xms. Let's see what happens.

I will keep an eye on the JVM stack, and experiment with bigger values for a future release.

The memory problem is mainly due to the 32bit limitation of our JVM bundle, especially for Windows. Of course there is a proper 64bit Java for that platform, but we don't use it yet.



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