[MLton] MLton HOL
Thu, 27 May 2004 22:27:29 +0100 (BST)
On Wed, 26 May 2004, Stephen Weeks wrote:
> > 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.
Indeed, it still died when I gave it 1.5Gb of disk space instead of
> 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.
I tried this, but it didn't change anything. The full compiler
mlton @MLton gc-messages -- -polyvariance false -inline 100 -basis
1997 -verbose 3
> If you make the code available for download, I'd be happy to try it
> out on my 4G machine.
307788 1619954 16571682 bin/psl1.sml
is available at
The machine I'm using to compile in is a 4Gb machine, but according to
top mlton is only using 2Gb, and my efforts to persuade it to use more
(-fixed-heap 3500m) didn't meet with any success (it stayed at 2Gb).