[MLton] MLton HOL

[Joe Hurd]

After a break, I'm returning to my project to port HOL4 to MLton.

I've now succeeded in compiling significant fractions of HOL using

MLton 20040227 (built Fri Feb 27 21:23:55 2004 on redhat71),

including a version that uses 120,000 lines of HOL theories. This
takes about 10 minutes to compile.

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:

         backend starting
            ssaToRssa starting
            ...lots of lines...
            average position in bucket = 2.285
sfwrite failed (No space left on device)

Is it possible to tell MLton to use a different directory for
temporary storage during compilation?

Regards,

Joe