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

On Fri, 5 Dec 2014, Harry Butterworth wrote:

For me, sometimes it hangs up so bad I can't even use the editor. Sometimes the editor is still working but the prover isn't making progress. Sometimes when it is hung I see the java process taking 100% cpu.

A java process with 100% (and a few GB memory) could mean that the specified heap is full and GC failing to continue properly. This is a well-known "feature" of the JVM. You need to give more room in advance, e.g. like this in $ISABELLE_HOME_USER/etc/settings:

JEDIT_JAVA_OPTIONS="-Xms1024m -Xmx4096m -Xss4m"

There are a few more examples in $ISABELLE_HOME/src/Tools/jEdit/etc/settings -- you need to restart the application afterwards.

This only refers the "isabelle jedit" command-line tool, or the Linux toplevel "app" script. For Mac OS X, the Info.plist provides similar JVM properties. Likewise for Windows in the Isabelle2014.ini file.

Note that the defaults are for a 2-4 GB machine in 32bit mode, where JVM memory is tight. On Linux or Mac OS X the JVM is usually in 64bit mode, and bigger heap as above can be easily afforded. On Windows the bundled JVM is always for 32bit, though, but a 64bit one could be installed manually, e.g. by replacing the Isabelle2014/contrib/jdk directory.


           1,023,025 people so far

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