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.
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.
Makarius