On 14/02/2016 21:13, Matthew Fernandez wrote:
On Sunday, 14 February 2016, Makarius <makarius at sketis.net> wrote:
On Sun, 14 Feb 2016, Matthew Fernandez wrote:
I received several off-list replies to this, including a pointer to
previous experiments by Data 61 colleagues
How is this related to the experiment with heap hierarchies? I.e. a stack of heaps according to the session parent structure.
Makarius: are you referring to the Poly/ML saved state mechanism or something else?
They are essentially orthogonal. AIUI the heap hierarchies change involved modifying Isabelle to use existing Poly/ML support for saved states that reference others, but not modifying Poly/ML itself. In contrast, this proposed change is purely to Poly/ML. Both have the effect of reducing disk usage and their effects are cumulative.
As far I'm aware Isabelle just uses the shared state facilities of Poly/ML. That provides the ability to save states that are the direct descendant of the executable or the descendant of another saved state.
From a quick look at the code the main effect that child states have is that StateLoader::LoadFile needs to seek within the saved state file to get the name of the parent file. That has to be loaded before the child because the child may, almost certainly will, overwrite some of the parent data. That may affect how you compact the data. How well do the compression libraries cope with seeking within the file?
From my own point of view I'm concerned that compacting the heap files may add to the cost of loading. In my experimental IDE, while a file is being edited a lot of saved states are loaded and reloaded repeatedly to provide the context. I'd like to see what effect adding compaction has on it but it may be necessary to provide separate functions to save states with and without compaction. Loading is easier because the loader can look at the format. Note that there's no need to provide backwards compatibility because a saved state can only ever be reloaded into the executable that created it.
David