Re: [isabelle] »strict« or »sequential« mode in Isabelle/jEdit?




On 22/04/2014 16:09, Makarius wrote:
> On Sun, 13 Apr 2014, Tobias Nipkow wrote:
> 
>> - Adjusting the AFP frequently leads me into the follwing situation: I run
>> "afp_build -A"; there is an error in some entry; I fix the error; I restart
>> "afp_build -A"; isabelle (more precisely java) dies with some out of memory
>> error right away, sometimes blaming it on a corrupt log file. At this point I
>> need to remove all log files and rerun *everything*.
> 
> You need to remove only the log file that is in the way, but that is still a bit
> awkward.
> 
> Maybe you just have the default ISABELLE_BUILD_JAVA_OPTIONS, which are meant to
> work on most systems without any bad surprise about JVM startup failure due to
> lack of address space.  (The situation is complicated by having to guess at
> total heap space and individual thread stack space.)
> 
> To allow heavy-duty AFP maintenance, I use something like this in
> $ISABELLE_HOME_USER/etc/settings:
> 
>   ISABELLE_BUILD_JAVA_OPTIONS="-Xmx4096m -Xss1m"
> 
> or like this:
> 
>   ISABELLE_BUILD_JAVA_OPTIONS="-Xmx4096m -Xss2m"
> 

I currently have what you had sent me some time ago:

JEDIT_JAVA_OPTIONS="-Xms256m -Xmx4096m -Xss2m -Dactors.corePoolSize=8
-Dactors.enableForkJoin=false"

Is the above ISABELLE_BUILD_JAVA_OPTIONS independent to that, or does one imply
the other?

Tobias

>     Makarius




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