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.
Thanks, Michael
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
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
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 PolyML.SaveState ? http://www.polyml.org/documentation/Reference/PolyMLSaveState.html
Phil
On 24 Sep 2015, at 02:02, Phil Clayton <phil.clayton at lineone.net> 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 heaps in this way, layer by layer.
Have you looked at PolyML.SaveState ? http://www.polyml.org/documentation/Reference/PolyMLSaveState.html
No, but that's very interesting thanks! Perhaps that'd be altogether better.
Michael
________________________________
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
-
David.Matthews＠prolingua.co.uk -
Michael.Norrish＠nicta.com.au -
phil.clayton＠lineone.net