[MLton] MLton HOL

[Joe Hurd]

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