[MLton] HOL on MLton
Fri, 16 Jan 2004 18:59:30 -0800
> 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.