[MLton] MLton HOL
Fri, 2 Jul 2004 00:42:54 +0100 (BST)
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,