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