[MLton] Isabelle on MLton?

[Matthew Fluet]

> 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.
> At the moment we use PolyML (mostly) and sml/nj.

If the interactive top-level is a requirement for Isabelle, then the short 
answer is "no", since there are no plans on adding a REPL in the 
forseeable future.

Of course, one might consider not using the host ML type-system/REPL as 
the means of theorem checking and interaction; instead, roll an embedded 
interpreter of one form or another.

We had a lengthy discussion with some of the HOL (hol.sourceforge.net) 
developers approximately a year ago:
    http://mlton.org/pipermail/mlton/2005-March/026846.html
    http://mlton.org/pipermail/mlton/2005-March/date.html
    http://mlton.org/pipermail/mlton/2005-April/date.html

Are there specific aspects of the interactive top-level that are required 
for Isabelle?