[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory
dm at prolingua.co.uk
Mon Feb 22 09:38:54 CET 2016
On 22/02/2016 07:58, Lars Hupel wrote:
>> Another possibility is to set the maximum heap size with --maxheap e.g.
>> ML_OPTIONS="--maxheap 28G"
>> If the application needs it Poly/ML will try to grow the heap to avoid
>> doing a lot of garbage collection. That can result in it crowding out
>> other parts of the system that also need memory. The "Unable to
>> increase stack" probably results from it being unable to grow an ML
>> stack if the application recurses very deeply. I'm guessing that you
>> don't have any swap space configured so there's no leeway there. You
>> may have to experiment with the setting. You don't need --stackspace if
>> you set the maximum heap size.
> Thanks for the hint. Indeed, there's no swap space configured, because
> all the build boxes have 32 GB of RAM.
> I've tried setting the --maxheap to 4 GB, but here's the error I'm getting:
> Value of --maxheap option is too large
> (Relevant build log:
That suggests that you're running the 32-bit version of Poly/ML in which
case the heap is limited to around 3-3.5G by the system and the problem
you're having is the total 4G memory limit. Switch to the 64-bit
version as a starting point. I was assuming that with 32G of memory you
were running the 64-bit version already.
More information about the isabelle-dev