[MLton-devel] MLton HOL

[Joe Hurd]

On Sat, 18 Oct 2003, Stephen Weeks wrote:

> > Thanks for the patch: now I can compile the entire HOL system.
>
> Great!  Out of curiosity, how big is HOL?

It's partially machine generated, but what I'm feeding to the MLton
compiler is this:

carp:~/hol$ wc selftest.sml
 300129 1585487 16252175 selftest.sml

On my Pentium III 600MHz, MLton takes this long:

MLton finished in 234.04 + 352.29 (60% GC)

> I like both suggestions.  So much so that I'd already implemented them
> in our internal version :-).

Great. I'm green with envy.

> If you'd like to get access to this feature and do some beta testing
> for us, I'd be happy to put up a package.

Yes please. Though I doubt I'll have any more suggestions about the
feature, I'd be pleased to be a consumer.

Joe




-------------------------------------------------------
This SF.net email sponsored by: Enterprise Linux Forum Conference & Expo
The Event For Linux Datacenter Solutions & Strategies in The Enterprise 
Linux in the Boardroom; in the Front Office; & in the Server Room 
http://www.enterpriselinuxforum.com
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel