On 14/02/2016 21:13, Matthew Fernandez wrote:
On Sunday, 14 February 2016, Makarius <makar...@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
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
