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