Re: [isabelle] Fwd: Installation problem



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.