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



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"


	Makarius




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