> On 24 Sep 2015, at 02:02, Phil Clayton wrote:
>
> 23/09/15 03:11, Michael Norrish wrote:
>> Or is there another way of getting what I need? I'd like to dispense with
>> explicit calls in our own code to PolyML.export, and then needing to call
>> the linker, but we do want to be able to build
23/09/15 03:11, Michael Norrish wrote:
Or is there another way of getting what I need? I'd like to dispense with
explicit calls in our own code to PolyML.export, and then needing to call the
linker, but we do want to be able to build heaps in this way, layer by layer.
Have you looked at Poly
On 23/09/2015 03:11, Michael Norrish wrote:
It would be useful for HOL4 if polyc could be used with a different
base executable. At the moment, the shell-script is hardcoded to use
e.g., /usr/local/bin/poly. If HOL has created a different heap H
with a lot of preloaded context, but for which th
