Re: [isabelle] Fwd: Installation problem



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

On 14/06/2013 10:39, Andreas Lochbihler wrote:
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

On 14/06/13 11:31, Antoine Grospellier wrote:
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 at 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

On 14/06/13 10:36, Antoine Grospellier wrote:
I'm really stuck. Does anyone have an idea to help me?

Thanks a lot,
Antoine Grospellier




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.








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