Re: [isabelle] Report of another crash



On Sat, 27 Dec 2014, Elsa L. Gunter wrote:

Dear Isabelle Maintainers,
While trying to build my theories in jedit, atop JinjaThreads and List-Infinite from the most recent AFP, on a MacBook Pro (circa Sept 2014) with a 2.8 GHz Intel Core i7 and 16 GB memory, I received the following error message:

 Welcome to Isabelle/HOL (Isabelle2014: August 2014)
 Run out of store - interrupting threads

 Run out of store - interrupting threads

 Failed to recover - exiting

JinjaThreads is usually operating at 120% of what is possible with a given Isabelle version. Since you have 16 GB here, it might help to switch Poly/ML into x86_64 mode like this in $ISABELLE_HOME_USER/etc/settings:

  ML_PLATFORM="$ISABELLE_PLATFORM64"
  ML_HOME="$POLYML_HOME/$ML_PLATFORM"
  ML_OPTIONS="--minheap 2000 --maxheap 12000"

You can also experiment a bit with the heap options: there is no need to give any hard limits at all, but let the system adapt to the situation dynamically. It depends a bit what else you are running on that machine.

The ML_OPTIONS are passed to the poly executable. Its options are explained further by the executable itself, e.g. like this within the running Isabelle environment:

ML ‹Isabelle_System.bash "\"$ML_HOME/poly\" --help"›


	Makarius

----------------------------------------------------------------------------
                http://stop-ttip.org  1,232,687 Participants
----------------------------------------------------------------------------


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