18 Jan
2011
18 Jan
'11
12:40 p.m.
Hi all,
I'm trying to build JinjaThreads, a massive Isabelle theory, using the 32-bit linux version of Poly/ML 5.4.0. The machine is equipped with 6 GiB of RAM and runs a 64-bit linux kernel. After a while, Poly/ML aborts with "Run out of store - interrupting threads". But at this time, the poly process only has allocated around 2.7GiB of memory (VIRT).
Why does Poly/ML does not try to allocate more memory? I tried to request a bigger initial heap size with "-H 3500", but this seemed to result in a heap size of 2GiB. As I tested with a small C program, a 32-bit process can allocate (and use) 4070MiB on this machine.
Greetings, Lars