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

[Japheth Lim]

Hi all,

Isabelle currently saves fully self-contained heaps. This is wasteful
since a low-level session like HOL will be duplicated in every heap that
depends on it.

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.

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

A lot of space could be saved if Isabelle saves heaps in this way. For
our L4.verified project we found a 7× reduction in size.

Japheth

________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.