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
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
