On 08/05/2017 20:11, Chun Tian (binghe) wrote:
Maybe a more interesting question is this: if we built two Poly.exe
from the same code base, one is “Windows” subsystem, the other is
“Console” subsystem, can they share the same user-saved “heap”? If
the answer is YES, then user could freely choice one version of the
two for each specific purposes. (I ask this because on Linux/Mac I
see each time after I rebuilt PolyML, even with the same PolyML
source code, all my HOL4 builds must be rebuilt too (otherwise they
refuse to startup). I don’t understand why this is necessary.)
You should be able to achieve this but it may take a bit of fiddling.
When you save a heap though PolyML.SaveState.saveState the saved state
records the time stamp of the parent executable. It will only allow the
saved state to be loaded into an executable with the same parent time
stamp. The reason for this is that the saved state does not contain
everything that it needs to run. Anything that is contained in the
executable, such as the standard basis, other libraries, compiler etc,
will not be saved. The saved heap just contains pointers to these but
the addresses could be different in a different executable.
However, there is just one object file that contains the time stamp as
well as all the ML library code. This is the one that is output through
PolyML.export. In the Linux build this is normally polyexport.o and in
Windows polyexport.obj. The normal build process will build a new
version of this but if you rebuild an executable but use the original
version of this object file the resulting executable should continue to
load the original saved states.
Regards,
David
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
