[isabelle-dev] Max threads & Sledgehammer

[David Matthews]

On 07/01/2013 17:49, Stefan Berghofer wrote:
>> You could certainly hit limits on memory for stacks with a large
>> number of threads particularly if the default stack size is large.
>> What does "ulimit -s" say?  You could try setting that smaller.
>
> "ulimit -s" says 102400

This is surprisingly large.  That works out at 100Mbytes per thread, 
assuming that this is "k" as on my Debian machines.  My machines show 
8192 here.  Poly/ML needs only a small space on the C stack so maybe it 
should set the stack size explicitly when the threads are created.

David