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

Hi Makarius,

Here is another datapoint in the greyout story with Isabelle2014. The attached syslog ends with a DUP exception. This time there were no exceptions on the command line. The greyout happened again while I was using the query panel to find theorems.

My setings are:

JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"
ML_OPTIONS="-H 500 --gcthreads 4"q

Hope this helps,

On 10/10/14 13:48, Makarius wrote:
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.



Description: Zip archive

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