[isabelle-dev] Max threads & Sledgehammer
dm at prolingua.co.uk
Tue Jan 8 14:21:41 CET 2013
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.
More information about the isabelle-dev