[isabelle] Installation problem · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Installation problem

Email Gateway (Aug 19 2022 at 11:16):

From: Antoine Grospellier <antoine.grospellier@ens-lyon.fr>
Hello,

I try to install Isabelle on my linux machine and I have this error message:
Build started for Isabelle/HOL ...
Building Pure ...
poly: heapsizing.cpp:606: bool
HeapSizeParameters::getCostAndSize(POLYUNSIGNED&, double&, bool):
Assertion `sizeMin >= minHeapSize && sizeMin <= maxHeapSize' failed.
/home/antoine/Documents/stage/isabelle/Isabelle2013/lib/scripts/run-polyml :
ligne 77 : 16932 Abandon "$POLY" -q $ML_OPTIONS
Pure FAILED

Thank you.
Antoine Grospellier.

Email Gateway (Aug 19 2022 at 11:17):

From: Antoine Grospellier <antoine.grospellier@ens-lyon.fr>
I'm really stuck. Does anyone have an idea to help me?

Thanks a lot,
Antoine Grospellier

Hello,

Thank you.
Antoine Grospellier.

Email Gateway (Aug 19 2022 at 11:17):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Antoine,

This assertion looks as if PolyML has difficulties with determining the size of its heap.
How much memory does your machine have? Maybe, it helps to adjust the initial heap size.
You can do so by changing the value of -H in Isabelle's ML_OPTIONS variable. Go to
~/.isabelle/Isabelle2013/etc and add a file with name "settings" with the following line
as content:
ML_OPTIONS="-H 500"

AFAIK, 500 is Isabelle's default value for the initial size of the heap. Try to increase
or decrease that value and see if it works.

Hope this helps,
Andreas

Email Gateway (Aug 19 2022 at 11:17):

From: Antoine Grospellier <antoine.grospellier@ens-lyon.fr>
Hi,

Thank you for your answer Andreas.
I have an old computer which has only 500 Mb of memory.
I tried to increase and decrease the ML_OPTIONS value but it doesn't
change the error. Note that the number 16932 changes at each try.

Thanks.
Antoine

Quoting Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>:

Email Gateway (Aug 19 2022 at 11:17):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Antoine,

I am afraid that 500Mb don't suffice to run Isabelle nowadays (you could try to set -H to
something as low as 100 and retry). Makarius might tell you more, but IIRC he's on vacation.

Best,
Andreas

Email Gateway (Aug 19 2022 at 11:17):

From: David Matthews <dm@prolingua.co.uk>
Hi Antoine,
The quick answer is: remove the -H option completely by setting
ML_OPTIONS="". This works for me in a 512Mbyte virtual machine.
However, you may find 500Mbytes very tight for Isabelle.

The slightly longer answer is that you've fallen foul of a bug in
Poly/ML 5.5. Prior to 5.5 the -H option had an important role to play
in setting the heap size and adjusting the size once the program was
running. Poly/ML 5.5 has a much more sophisticated heap sizing
algorithm and -H is retained just as a way of setting the initial size.
The default maximum size is calculated from the memory size and if the
memory size is smaller or similar to the -H option the bug is triggered.

Regards,
David

Last updated: Apr 16 2024 at 20:15 UTC