[MLton] MLton HOL
Wed, 26 May 2004 22:50:41 -0700
> However, when I feed it the full 300,000 lines of HOL theories, it
> compiles for about 10 minutes, using 2Gb of memory, and then dies
> because it runs out of space on the 0.5Gb /tmp partition:
Although what I said about TMPDIR is correct, I'm not so confident it
will help in your situation. The memory requirement may simply be too
large, and using a larger tmp directory will simply cause lots of disk
writes followed by a terrible slowdown due to lots of paging.
Just to get things to compile, it might be worth trying compiling with
-polyvariance false and/or using a smaller inlining threshold
(e.g. -inline 100) to see if that cuts down on code size. Compiling
-verbose 3 will also give some more data on IL sizes and where the
blowup is happening. Also, using @MLton gc-messages will give some
If you make the code available for download, I'd be happy to try it
out on my 4G machine.