[MLton] Eliminating library elaboration time

[Vesa Karvonen]

The Basis library elaboration overhead seems to be a big issue to some
people.  So, I was wondering whether we could mostly eliminate the
overhead through the save/load world functionality of MLton.  Googling
revealed that, indeed, MLton used to do that, but the feature was
removed:

  http://mlton.org/pipermail/mlton/2003-November/024667.html

Now, I think that it we should reintroduce the feature and generalize
it.  Here is what I was thinking.  We would add two options:

  -with-precompiled-basis <path.mlb>
  -precompile-to <path>

The first option is used to specify all the ML Basis files that you
wish to precompile (pre-elaboration).  The effect would be the same as
if your top-level MLB file would start with

  local <path.mlb> in end

for each <path.mlb> that you specified.  The second option would
specify where MLton saves the world after precompiling or loads at
startup.  The mlton script would check if the path does in fact
exists.  If it doesn't, it runs MLton with a default world.  After
MLton starts, it checks that all the bases specified on the
command-line have been precompiled and that the precompiled bases are,
in fact, up to date by checking file dates.  If the check fails, then
MLton precompiles the bases, saves the world to the file named by the
-precompile-to option and exists.  The mlton script then restarts
mlton (this avoids issues on some platforms).  Otherwise mlton
proceeds to compile as usual.

So, what do you think?  Would a scheme like this work and eliminate
(Basis) library elaboration time?

-Vesa Karvonen