Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-19 Thread Lars Hupel 
>> Try adding a --stackspace argument to reserve space for thread stacks
>> and anything else. e.g.
>> ML_OPTIONS="--stackspace 200M"
>> This option keeps this space back whenever Poly tries to grow the heap
>> to avoid the heap using all the available memory.  You may need to
>> experiment a bit with how much to reserve depending on why the memory is
>> required.  It is possible that you could still get the error if there is
>> some sort of loop.
>
> Thanks for the suggestion. I've deployed that change on all our build
> boxes. We'll see how it works out.

The problem still persists, as can be witnessed from this log:

  

This time, there are additional messages:

  Warning - Unable to increase stack - interrupting thread
  Warning - Unable to increase stack - interrupting thread
  Warning - Unable to increase stack - interrupting thread
  *** Interrupt
  Algebraic_Numbers FAILED

Oddly enough this is not reproducible. If I run just the failing sessions
on an identical build box, it works fine.


Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-19 Thread Lars Hupel 
> Try adding a --stackspace argument to reserve space for thread stacks
> and anything else. e.g.
> ML_OPTIONS="--stackspace 200M"
> This option keeps this space back whenever Poly tries to grow the heap
> to avoid the heap using all the available memory.  You may need to
> experiment a bit with how much to reserve depending on why the memory is
> required.  It is possible that you could still get the error if there is
> some sort of loop.

Thanks for the suggestion. I've deployed that change on all our build
boxes. We'll see how it works out.

Cheers
Lars
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Re: [isabelle-dev] Formula_Derivatives FAILED: Cannot allocate memory

2016-02-19 Thread David Matthews 

On 17/02/2016 21:47, Dmitriy Traytel wrote:

ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised


This looks like an attempt to allocate memory for something other than 
the heap.  There are quite a few situations where this can happen.


Try adding a --stackspace argument to reserve space for thread stacks 
and anything else. e.g.

ML_OPTIONS="--stackspace 200M"
This option keeps this space back whenever Poly tries to grow the heap 
to avoid the heap using all the available memory.  You may need to 
experiment a bit with how much to reserve depending on why the memory is 
required.  It is possible that you could still get the error if there is 
some sort of loop.


David
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev