[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML

[Makarius]

On Thu, 12 Nov 2015, Japheth Lim wrote:

> For a long time, Poly/ML has supported hierarchical heaps 
> (PolyML.SaveState.saveChild). As I understand it, this feature was not 
> used because it makes heaps no longer self-contained; moving them to a 
> different path would break the loading process.

Hierarchic heaps were once used in Isabelle, but discontinued since the 
persistency of mutable values was not properly supported.  This has 
changed in various ways over the years, so it is something to be 
revisited eventually.


> David Matthews has kindly implemented a solution for that problem, 
> allowing the application to specify all the paths in the hierarchy. See 
> the announcement
>
>  http://lists.inf.ed.ac.uk/pipermail/polyml/2015-November/001698.html

I have seen that thread on the Poly/ML mailing list, and marked it as 
relevant.  It remains to be seen if something happens before the coming 
release of Isabelle2016. Adding more and more features on the spot is 
always a temptation and a danger.

Both Poly/ML and Isabelle/ML have changed significantly in the past few 
months, and the main priority is to wrap up for the release of both 
really-soon-now.

For example, the native Windows support of Poly/ML can still crash in some 
situations.  Pinning this down precisely has priority over optional 
add-ons.


 	Makarius