Email Gateway (Aug 19 2022 at 15:51): Email Gateway (Aug 19 2022 at 15:51):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Thanks David. That is indeed what is going on.
There's an Isabelle problem here: the suggested approach to executing
64-bit polyML does not actually result in 64-bit polyML being run.
In the Isabelle NEWS file the following is suggested:
The following example setting prefers 64 bit if available:
ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
I have in my isabelle settings the line:
ML_PLATFORM="$ISABELLE_PLATFORM64"
Running isabelle env | grep ML shows these settings:
ML_IDENTIFIER=polyml-5.5.2_x86_64-linux
POLYML_HOME=/home/tsewell/.isabelle/contrib/polyml-5.5.2
ML_SYSTEM=polyml-5.5.2
ML_PLATFORM=x86_64-linux
ML_OPTIONS=-H 500
ISABELLE_POLYML=true
ML_HOME=/home/tsewell/.isabelle/contrib/polyml-5.5.2/x86-linux
ML_SOURCES=/home/tsewell/.isabelle/contrib/polyml-5.5.2/src
So, the isabelle environment is now thoroughly confused which version of
polyML is running, to the extent that my heap files are being saved in a
directory called "polyml-5.5.2_x86_64-linux" despite the fact that the
poly process which is running is actually the x86-linux variant.
In short, that is all a bit confusing. Is there a better way to switch
between 32 and 64 bit modes? For the moment, I've just moved the
~/.isabelle/contrib/polyml-5.2.2/x86-linux directory aside, which
results in Isabelle falling back to 64-bit mode. Amusingly, polyML then
objects to the version of the saved heap files.
Well, enough said. I hope this is easy to fix.
Thanks all,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 15:51):From: Lars Noschinski <noschinl@in.tum.de>
Indeed, there doesn't seem to be a really clean way.
The etc/settings file of the polyml-5.2.2-1 component automatically
chooses between ISABELLE_PLATFORM32 and 64 by trying to run 32-bit poly
and there is no way of overriding this.
To fully switch to 64-bit poly, you need to set
ML_PLATFORM=$ISABELLE_PLATFORM64
ML_HOME=$POLYML_HOME/$ML_PLATFORM"
after initializing the component.
Also, ML_OPTIONS is different for 64-bit mode, so you may want to set
ML_OPTIONS="-H 1000"
too.
-- Lars
Email Gateway (Aug 19 2022 at 15:51):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Thanks Lars.
OK, so I've learned a lot from this. Apparently the order of the
"init_components" line with respect to the other lines of the settings
file matters quite a lot.
The polyml component currently overrules any settings that were
previously set, and then sets quite a few settings of its own. The
missing "clean" approach would probably involve requesting 64-bit mode
before the component initialises, and having the component notice this
has been done.
To override the settings after the component has initialised, you must
override all the settings it set, but there's no obvious way to ask what
they were. Perhaps in the past it was sufficient to adjust ML_PLATFORM.
To confuse matters, further settings (environment variables) seem to be
updated after the end of the user's settings file. For instance,
adjusting ML_PLATFORM seems to imply an update to ML_IDENTIFIER, but not
to ML_HOME or POLYML_HOME, thus the confusing outcome.
Well, I now know a lot more about how this works. However, I'm going to
continue enabling 64-bit mode by sabotaging 32-bit mode until someone
suggests a significantly better way.
Thanks for educating me,
Thomas.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Email Gateway (Aug 19 2022 at 15:53):From: Makarius <makarius@sketis.net>
It seems that some more basic Isabelle education is required. As usual
there are two approaches: to work with the system, or to work against it.
Working with the system means to look around carefully how things are
usually done, under the assumption that the system is mostly right.
Concerning settings the "system" manual also has a lot to say -- here it
needs to be read in the context of Isabelle component settings in
particular.
Taking a NEWS entry from 2010 in isolation is unlikely to succeed, without
its historical context. In the past there were no Isabelle components and
people usually had the full bunch of ML settings somewhere. Then it was
obvious what the change of a single line line ML_PLATFORM="..." meant.
Today in Isabelle2014, the component polyml-5.5.2-1/etc/settings still
make it possible to work like that, taking the with a commented-out
section of "basic settings" as a starting point:
ML_SYSTEM=polyml-5.5.2
ML_PLATFORM="$ISABELLE_PLATFORM32"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
ML_SOURCES="$POLYML_HOME/src"
Applying some care and common-sense, it should be obvious who to work with
that, without any need to "fix" Isabelle, nor to "sabotage" anything.
Makarius
Email Gateway (Aug 19 2022 at 16:05):From: Thomas Sewell <thomas.sewell@nicta.com.au>
Hello isabelle-users.
I've been struggling lately with fairly frequent "Insufficient memory"
exceptions when trying to build heaps/images. The strange thing is that
I don't seem to have run out of memory in any sense.
From reading the log, it looks a lot like PolyML ran out of something
while trying to do its final cleanup before saving the session. In the
session log, all the theories have been loaded already. There's also
plenty more total memory available on this machine at the time of
failure, so I don't think it's a fail-to-allocate problem. Perhaps
PolyML has exhausted some fixed resource used while doing a
shareCommonData or similar, such as stack space on some thread?
Finally, in the past I've noticed that the problem is slightly
nondeterministic. If I delete a few heaps and try again, sometimes the
process succeeds, usually after three or four attempts. This is not a
lot of fun.
Does anyone have any idea what kinds of things might cause this problem,
and where I should be looking? I've noticed that polyML itself has a
number of command-line memory-debugging arguments, and I'm not sure what
will happen if I try to convince Isabelle to pass them along.
I don't set any limits on PolyML's memory usage in my isabelle settings
or via ulimit or similar. (There's a limit on Java's memory consumption,
but that's not what's being hit here.)
Here are the last few ML statistics messages from the log of the failed
session:
^LML_statistics =
^E^F:^Fnow=1410497588.77^Ftasks_ready=0^Ftasks_pending=0^Ftask
s_running=1^Ftasks_passive=0^Fworkers_total=4^Fworkers_active=1^Fworkers_waiting
=0^Ffull_GCs=4^Fpartial_GCs=1275^Fsize_allocation=548405248^Fsize_allocation_fre
e=292779660^Fsize_heap=3074088960^Fsize_heap_free_last_full_GC=18342268^Fsize_he
ap_free_last_GC=553199172^Fthreads_in_ML=1^Fthreads_total=7^Fthreads_wait_condva
r=4^Fthreads_wait_IO=0^Fthreads_wait_mutex=0^Fthreads_wait_signal=1^Ftime_CPU=43
6.427259^Ftime_GC=37.738374^Fuser_counter0=0^Fuser_counter1=0^Fuser_counter2=0^F
user_counter3=0^Fuser_counter4=0^Fuser_counter5=0^Fuser_counter6=0^Fuser_counter
7=0^E^E^F^E
^LML_statistics =
^E^F:^Fnow=1410497589.27^Ftasks_ready=0^Ftasks_pending=0^Ftask
s_running=1^Ftasks_passive=1^Fworkers_total=4^Fworkers_active=1^Fworkers_waiting
=0^Ffull_GCs=4^Fpartial_GCs=1275^Fsize_allocation=548405248^Fsize_allocation_fre
e=143978084^Fsize_heap=3074088960^Fsize_heap_free_last_full_GC=18342268^Fsize_he
ap_free_last_GC=553199172^Fthreads_in_ML=1^Fthreads_total=7^Fthreads_wait_condva
r=4^Fthreads_wait_IO=0^Fthreads_wait_mutex=0^Fthreads_wait_signal=1^Ftime_CPU=43
6.827284^Ftime_GC=37.738374^Fuser_counter0=0^Fuser_counter1=0^Fuser_counter2=0^F
user_counter3=0^Fuser_counter4=0^Fuser_counter5=0^Fuser_counter6=0^Fuser_counter
7=0^E^E^F^E
And the final few lines:
^LML_statistics =
^E^F:^Fnow=1410497589.57^Ftasks_ready=0^Ftasks_pending=0^Ftasks_running=0^Ftasks_passive=0^Fworkers_total=0^Fworkers_active=0^Fworkers_waiting=0^Ffull_GCs=4^Fpartial_GCs=1276^Fsize_allocation=528482304^Fsize_allocation_free=394241872^Fsize_heap=3075137536^Fsize_heap_free_last_full_GC=18342268^Fsize_heap_free_last_GC=532482744^Fthreads_in_ML=0^Fthreads_total=3^Fthreads_wait_condvar=0^Fthreads_wait_IO=0^Fthreads_wait_mutex=0^Fthreads_wait_signal=1^Ftime_CPU=437.319315^Ftime_GC=37.802378^Fuser_counter0=0^Fuser_counter1=0^Fuser_counter2=0^Fuser_counter3=0^Fuser_counter4=0^Fuser_counter5=0^Fuser_counter6=0^Fuser_counter7=0^E^E^F^E
^LTiming =
^E^F:^Fthreads=4^Felapsed=330.020^Fcpu=467.429^Fgc=37.442^Ffactor=1.42^E^E^F^E
val it = (): unit
ML> Exception- Fail "Insufficient memory" raised
Thanks for your time/thoughts,
Thomas.
Email Gateway (Aug 19 2022 at 16:07):From: David Matthews <dm@prolingua.co.uk>
Looking at those figures I would guess that you are running the 32-bit
version of Poly/ML. I think that is the default for Isabelle because,
generally, it gives better performance than the 64-bit version. The
problem with it is that the total address space of a 32-bit application
is limited by the operating system to around 3Gbytes. Poly/ML uses
several memory pools and a situation can arise where the address space
limit is reached. Try it with the 64-bit version and if it happens
there I will try and investigate further.
David
Last updated: Nov 21 2024 at 12:39 UTC