[MLton] MLton HOL

[Joe Hurd]

On Thu, 1 Jul 2004, Stephen Weeks wrote:

> I also fixed one quadratic performance bug in our code generator that
> Matthew found.  It turns out that this bug caused the bulk of the
> slowdown in the 8.6 hour compile.  As a result, my latest compile of
> HOL took 1.3 hours.

This is great! I'll attempt to build MLton from CVS, and get back to 
you if I have any trouble with this. Thanks for adding the exception 
printer---that'll come in very useful.

I asked the HOL developers about a file format for theories, and their 
main objection was that for interactive proof it's convenient to bind 
theorems to ML identifiers. So my question to you is, assuming I have 
read in a large collection of theorems to a suitable data-structure, 
is it possible to write something like

val theorem_1 = DB.fetch "theorem_1";
val theorem_2 = DB.fetch "theorem_2";
...
val theorem_n = DB.fetch "theorem_n";

in such a way that it won't generate vast amounts of code and 
variables in MLton?

Thanks for your help,

Joe