[MLton] MLton HOL
Joe Hurd
joe.hurd@comlab.ox.ac.uk
Thu, 1 Jul 2004 15:02:46 +0100 (BST)
On Thu, 1 Jul 2004, Stephen Weeks wrote:
>
> Hi Joe. I'm pleased to report some progress on compiling HOL. I left
> a compile running last night that completed in 8.6 hours. It produced
> a 33M executable, which, when run, produces the following output in
> 4.5 minutes.
That's great! Following your last message, I'm pushing the other hol
developers for a non-SML file format for theory files. Running all the
proof script files in MLton would take quite a bit of hacking, because
the whole architecture is geared towards this "xScript.sml creates
the file xTheory.sml", and there are many extensions where
xScript.sml prints extra SML code that becomes part of xTheory.sml and
is later compiled.
> % psl1
> unhandled exception: HOL_ERR
>
> Perhaps you could look into this error while we continue to improve
> the compile time. I'm shooting for 20 minutes -- it should just take
> some more efforts on improving quadratic algorithms to get there.
Unfortunately debugging the MLton HOL programs is hard, and I'm often
reduced to feeding in prefixes of the program to see if they produce
the same error :-( The exception HOL_ERR contains useful debugging
information, but since I don't know where it's being raise I can't
wrap the correct function in an exception handler.
I don't suppose it would be possible for ask MLton to print more than
just "unhandled exception: x"? Even just the arguments of x would help
a lot. HOL_ERR is defined as:
type error_record = {origin_structure : string,
origin_function : string,
message : string}
exception HOL_ERR of error_record
Thanks for the update,
Joe