[MLton] MLton HOL

[Joe Hurd]

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
0.5Gb.

> 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
invocation was

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.

The code

wc bin/psl1.sml
 307788 1619954 16571682 bin/psl1.sml

is available at

http://www.cl.cam.ac.uk/~jeh1004/psl1.sml

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).

Regards,

Joe