Re: [isabelle] Isabelle2016-1-RC1 processing theories twice



On 31/10/16 19:59, Manuel Eberl wrote:
> Additionally, it seems that the IDE gets very
> unresponsive if you change stuff in an "early" theory in the dependency
> tree. Sometimes it's so bad that I have to restart the entire thing.

This sounds more like the normal situation when the JVM heap fills up --
this is inherent in JVM memory menagement.  The default configuration
for x86_64 platforms has -Xmx2560m in a platform-specific place. A
typical value is -Xmx4096m and more can be tried depending on the hardware.

E.g. the new HOL-Analysis session is so big that it easily exhausts the
defaults. I have tried it on the 32bit Windows version, where the JVM is
confined to 1 or 1.5 GB, and it locks up almost immediately due to
overfull heap.


Here is cumulative information from NEWS for Isabelle2016 and
Isabelle2016-1:

* Java runtime options are determined separately for 32bit vs. 64bit
platforms as follows.

  - Isabelle desktop application: platform-specific files that are
    associated with the main app bundle

  - isabelle jedit: settings
    JEDIT_JAVA_SYSTEM_OPTIONS
    JEDIT_JAVA_OPTIONS32 vs. JEDIT_JAVA_OPTIONS64

* Many Isabelle tools that require a Java runtime system refer to the
settings ISABELLE_TOOL_JAVA_OPTIONS32 / ISABELLE_TOOL_JAVA_OPTIONS64,
depending on the underlying platform.


Instead of adding more options next time, I will try once again to tune
the whole system such that it can carry even bigger application. That
game is a variant of Tetris, but so far it could always be continued one
step further.


	Makarius





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