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
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 the main function is still
