And the solution finds itself within minutes of hitting the send button: my setup looked like it was using the 64bit version of poly, but was actually running the 32bit version. Just forgot to set a path correctly.
Sorry for the spam. Cheers, Gerwin > On 17.05.2015, at 08:57, Gerwin Klein <[email protected]> wrote: > > Hi, > > I’m running into problems with large heap sizes on 64bit Darwin. > > The machine I’m running on has 32GB physical memory, and runs out of polyml > memory on sessions that take about 12GB on 64bit Linux. The error message is > > val it = (): unit > ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised > > (This is from an Isabelle build of the image CBaseRefine in > https://github.com/seL4/l4v/tree/master/proof) > > The initial heap size was specified as “-H 2000”. Playing around with that > option, I got for instance for “-H 8000” the message: > > "Value of -H option is too large" > > I’m getting the same for trying to increase —maxheap. The same -H 8000 option > on a 64-bit Linux machine works fine. > > The check that throws this error seems to be: > > libpolyml/mpoly.cpp:177 > > // Check that the number of kbytes is less than the address space. > // The value could overflow when converted to bytes. > if (result >= ((POLYUNSIGNED)1 << (SIZEOF_VOIDP*8 - 10))) > Usage("Value of %s option is too large\n", arg); > > As far as I can see, config sets the value of SIZEOF_VOIDP to 8 on both > platforms, so I’m a bit mystified why one works and the other doesn’t. > > The polyml version is 5.5.2 (-3 in the Isabelle distribution, but same > problem for vanilla 5.5.2). > > Any ideas? > > Cheers, > Gerwin > > ________________________________ > > 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. _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
