[MLton] HOL on MLton

[Stephen Weeks]

> marlin:~/dev/sml/metis$ mlton -basis 1997 -profile time t.sml
> Warning: -basis is deprecated
> shrinker raised mismatched Leave
> 
> The offending source file is attached to this email.

Thanks for the bug report.  It was a bug in the optimizer that only
showed up when profiling.  You can get the fix from the CVS or wait
for the next release.

> Theorem proving in HOL4 consists of interacting with the ML top-level
> interpreter, so this is why we can't simply switch over to MLton. 

Ahh.  I'll add an interpreter/REPL to our todo list.  

> At the moment I'm trying to generate some interest in using MLton
> for the kind of proofs that involve costly simulation (e.g.,
> circuits, or network protocols), so you'd get everything set up just
> right using Moscow ML and then do a one-shot MLton run that might
> take weeks to complete a simulation.

Sounds neat.  We'd love to hear some performance numbers once you have
them ... and to add HOL to our users page once your port is stable.

> I think Moscow ML will switch over to the new basis library soon
> (the incentive has increased now that the mosml Time structure has
> just suffered a Y2K problem!), but in the meantime if the divergence
> between MLton and Moscow ML gets too big then my porting task will
> become infeasible. So please carry on supporting the 1997 basis, at
> least for the next few months!

It'll be in our next public release.  After that, we are moving to a
new library mechanism and I'm not sure whether it will stay around or
not.  But, based on past history, the next release after this one is
4-6 months away.  Hopefully Moscow ML will have caught up by then.  If
not, we'll figure something out.