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

Japheth Lim Japheth.Lim at nicta.com.au
Thu Nov 12 06:45:51 CET 2015

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


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.



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.

More information about the isabelle-dev mailing list