On 21/10/15, Gerwin Klein wrote:
It turns out that with our collection of large Isabelle sessions that we run regularly, polyml heap image space is becoming a noticeable problem for us.
We found another way to solve this problem. Isabelle uses saveState to save heaps. If we use saveChild instead, we get a substantial reduction in heap sizes.
However, this makes the saved states less portable because they contain the pathname of the parent. Then loading will fail if the heaps are moved to a different path. Here it would be nice if Poly/ML could use relative paths for the parent, and look them up relative to the child.
There are other ways to fix this (e.g. chdir before loadState) but I'd rather get the above behaviour from Poly/ML directly. Any thoughts?
Japheth
________________________________
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 30/10/2015 07:49, Japheth Lim wrote:
On 21/10/15, Gerwin Klein wrote:
It turns out that with our collection of large Isabelle sessions that we run regularly, polyml heap image space is becoming a noticeable problem for us.
We found another way to solve this problem. Isabelle uses saveState to save heaps. If we use saveChild instead, we get a substantial reduction in heap sizes.
However, this makes the saved states less portable because they contain the pathname of the parent. Then loading will fail if the heaps are moved to a different path. Here it would be nice if Poly/ML could use relative paths for the parent, and look them up relative to the child.
There are other ways to fix this (e.g. chdir before loadState) but I'd rather get the above behaviour from Poly/ML directly. Any thoughts?
What about PolyML.SaveState.renameParent? See http://www.polyml.org/documentation/Reference/PolyMLSaveState.html
David
Hi,
On 30/10/15 19:13, David Matthews wrote:
On 30/10/2015 07:49, Japheth Lim wrote:
On 21/10/15, Gerwin Klein wrote:
It turns out that with our collection of large Isabelle sessions that we run regularly, polyml heap image space is becoming a noticeable problem for us.
We found another way to solve this problem. Isabelle uses saveState to save heaps. If we use saveChild instead, we get a substantial reduction in heap sizes.
However, this makes the saved states less portable because they contain the pathname of the parent. Then loading will fail if the heaps are moved to a different path. Here it would be nice if Poly/ML could use relative paths for the parent, and look them up relative to the child.
There are other ways to fix this (e.g. chdir before loadState) but I'd rather get the above behaviour from Poly/ML directly. Any thoughts?
What about PolyML.SaveState.renameParent? See http://www.polyml.org/documentation/Reference/PolyMLSaveState.html
This does work for most situations but I don't find it ideal. renameParent would need to be called whenever a state file is moved. It also wouldn't work when a file is loaded through multiple paths at the same time (think e.g. a file that is shared over NFS). I propose that changing the behaviour of Poly/ML here would make it more useful.
Japheth
________________________________
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 30/10/2015 09:53, Japheth Lim wrote:
What about PolyML.SaveState.renameParent? See http://www.polyml.org/documentation/Reference/PolyMLSaveState.html
This does work for most situations but I don't find it ideal. renameParent would need to be called whenever a state file is moved. It also wouldn't work when a file is loaded through multiple paths at the same time (think e.g. a file that is shared over NFS). I propose that changing the behaviour of Poly/ML here would make it more useful.
I don't like the idea of changing the existing behaviour but there may be other alternatives. Something that occurs to me would be to provide a function to load a complete hierarchy, say PolyML.SaveState.loadHierarchy: string list -> unit
Then PolyML.SaveState.loadHierarchy["grandparent", "parent", "child"] would load a set of files. Each file currently has a signature for the parent as well as a path and these are checked in case a parent has changed so the only difference would be that the paths to all the files would be provided from ML.
David
Hi David,
On 30/10/15 23:35, David Matthews wrote:
I don't like the idea of changing the existing behaviour but there may be other alternatives. Something that occurs to me would be to provide a function to load a complete hierarchy, say PolyML.SaveState.loadHierarchy: string list -> unit
Then PolyML.SaveState.loadHierarchy["grandparent", "parent", "child"] would load a set of files. Each file currently has a signature for the parent as well as a path and these are checked in case a parent has changed so the only difference would be that the paths to all the files would be provided from ML.
That sounds good as well. Then the path calculation could be implemented using showParent.
Japheth
________________________________
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 -
Japheth.Lim＠nicta.com.au