Re: [isabelle] isabelle build -vb runs out of store



Hi Peter,

Just a quick guess. Are you running PolyML in 32bit mode and thus hit the 32bit memory
wall? Or have you limitted PolyML's maximum heap size with some configuration parameters?
Not that I know of. PolyML should run in 64bit mode. How do I find out?

Normally, Isabelle starts PolyML in 32-bit mode even if you have a 64-bit system. I last compared 32-bit PolyML against 64-bit PolyML two years ago and at that time, 32-bit took a bit more than half the time the 64-bit system took for the same task. IIRC, the following tells you the setting.

  isabelle getenv ML_PLATFORM

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.