[MLton] MLton HOL

[Stephen Weeks]

> 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
more data.

If you make the code available for download, I'd be happy to try it
out on my 4G machine.