[MLton] Isabelle on MLton?

[Stephen Weeks]

> Is there any chance that we will be able to use MLton to run
> Isabelle (isabelle.in.tum.de) in the forseeable future?  We need an
> interactive top-level, which I believe you currently don't support.

Right.  Furthermore, if you want MLton for performance, then simply
adding an interactive top level to MLton will not be sufficient.  You
will need an interactive top level that interoperates with
whole-program-natively-compiled code and that doesn't significantly
hurt the performance of such code.  Other SML compilers achieve a REPL
by sacrificing whole-program optimization and performance.  We could
go that route, but it's not clear what the point would be -- what
would MLton have to offer over the other compilers that already do
that?

In the thread that Matthew mentioned, I sent the beginnings of a
proposal to integrate an embedded interpreter with a whole program
compiled by MLton without sacrificing performance:

  http://mlton.org/pipermail/mlton/2005-April/026950.html

But that is an untested research idea that may or may not pan out, and
in any case won't happen anytime soon with MLton.

So, if you want to use MLton with Isabelle in the near future, the
only way forward is to modify Isabelle.

  1. Eliminate as many of the uses of "use" and the REPL as possible.
     When I last looked at the Isabelle sources in 2000, a number of
     "use"s could be eliminated in favor of an extra-lingual program
     specification mechanism (CM or MLB).

  2. As Matthew suggests, use a hand-written embedded interpreter for
     the remaining needed programmability.