Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Report of another crash

view this post on Zulip Email Gateway (Aug 19 2022 at 16:53):

From: "Elsa L. Gunter" <egunter@illinois.edu>
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:

---Elsa

view this post on Zulip Email Gateway (Aug 19 2022 at 16:54):

From: Makarius <makarius@sketis.net>
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

Last updated: Apr 20 2024 at 01:05 UTC