[MLton] HOL's Moscow ML implementation, and pushing MLton to
emulate it
Daniel C. Wang
danwang@CS.Princeton.EDU
Fri, 01 Apr 2005 02:23:34 -0500
I haven't looked to closely at the HOL4 infrastructure in a while, but I
suspect that most of these theories don't share any state. If that's the
case you could develop an architecture where various different MLton process
communicate via RPC/IPC. This can avoid the need to build one big monolithic
system. If the RPC/IPC becomes a performance bottleneck, you take the
appropiate modules you need and build the monolith you want, but otherwise
you can do quick experiments by just recompling the theory you are hacking
on. (Also, if you're clever you can take advantage of a dual processor or a
cluster to do distributed theorem proving!)
Stephen Weeks wrote:
>>I would have thought that the reason that they didn't want this sort
>>of approach is that in addition to having the _code_ for every
>>theory in the executable, this would require the _data_ for every
>>theory resident in the heap at all times.
>
>
> That would hurt. Maybe it could be avoided by loading dummy libraries
> with trivial theorems (of negligible size) for those theories that
> will be unused. But that definitely doesn't support dynamic loading
> of theories, and so one will need all the theories in an executable
> that exposes an interpreter.
>