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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
