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 the main function is still PolyML.rootFunction, creating a new heap H' that is a delta on top of H seems to become difficult: my impression is that all of the source files that went into generating H have to be re-used before the new stuff making up H' can be looked at.
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.
I would have no objection to a modification to "polyc" in which the executable to be run as "poly" could be overridden by a parameter. If you want to propose a patch to polyc.in (the version before "configure" has added the actual paths) to do that I'll take a look at it.
David