[isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

[David Matthews]

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:
> <https://ci.isabelle.systems/jenkins/job/isabelle-repo-nightly-slow/23/console>)

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.

David