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. _______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
