[MLton] MLton HOL

[Joe Hurd]

On Thu, 27 May 2004, Stephen Weeks wrote:

> The Rssa (an
> IL) program size is about 142M which isn't so bad.  Given that, I
> wouldn't expect there to be a space problem in representing the next
> IL down the line.  So, perhaps there is something quadratic going on
> there.  I will investigate, but it may take some time.

I've now assembled the full MLton program that I want to compile. It's
a HOL formalization of the semantics for TCP, and it's being run on
thousands of actual network traces that take hours each to validate.
Hence, a move from Moscow ML to MLton would potentially allow about 10
times more traces to be checked, which would presumably result in a
better semantics. So there's a big incentive to compile this program,
the full incarnation being half a million lines of code:

$ wc bin/netsem1.sml
 444017 2885322 22718012 bin/netsem1.sml

At the moment, the parse/elaborate stage is failing, because the
program contains a call to the Moscow ML Regex dynamic library

http://www.dina.dk/~sestoft/mosmllib/Regex.html

Is there anything equivalent in MLton that I can use for this? If not,
I could perhaps get the developers to replace the call with something
in Standard ML, but only if the whole program was then likely to
compile. Any progress in solving the space blowup when compiling huge
programs?

Regards,

Joe