On Sunday, 14 February 2016, Makarius <[email protected]> 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
>
>
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml

Reply via email to