[MLton] HOL on MLton

[Stephen Weeks]

> I've now tried to compile HOL on a machine with 1.5Gb, using
> mlton-20030716. Though it gets pretty far, it fails while trying to
> write a large temporary file
> 
> -rw-------    1 jeh1004  jeh1004  92639232 Oct 19 17:29 FromSpacevzJm5f
> 
> into a 100Mb /tmp partition. For interest, the compile log follows.
> Any chance I could tell mlton not to use /tmp, but somewhere else?

Sadly, the /tmp is hardwired into the runtime.  The only way to change
this would be to modify runtime/gc.c, recompile the runtime, and
rebuild and relink mlton against the new runtime.

Anyways, this is due to some little used code in the runtime that only
runs when there isn't enough virtual memory to grow the heap.  So, the
runtime writes out the entire heap to disk, freeing up as much virtual
memory as it can, and then tries to allocate an even larger chunk of
memory.  Since your machine has 1.5G, the file is probably *very*
large.  You can get a little more info by compiling with

	@MLton gc-messages --

which will show more about what the runtime is doing.

This indicates that MLton is truly running out of memory.  Writing to
a place other than /tmp probably won't help.  Hopefully compiling with
-verbose 3 will give us a better idea of why things are getting so
huge.

If you make the program available on the web, I'll try to compile it
on my machine with 4G of RAM.

_______________________________________________
MLton mailing list
MLton@mlton.org
http://www.mlton.org/mailman/listinfo/mlton