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

Japheth Lim Japheth.Lim at nicta.com.au
Fri Nov 13 06:32:49 CET 2015

On 12/11/15 21:17, Lars Hupel wrote:
> Hi Japheth,
>> 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.
> out of curiousity: How did you arrive at this number? Have you
> implemented incremental heaps for Isabelle?

As I said, Poly/ML has supported this for a while. If you do not care
about the compatibility issues (heap pathnames, and Makarius mentioned
system stability concerns), the patch is quite simple:

diff --git a/src/Pure/ML-Systems/polyml.ML b/src/Pure/ML-Systems/polyml.ML
index 907c0f2..e0fec14 100644
--- a/src/Pure/ML-Systems/polyml.ML
+++ b/src/Pure/ML-Systems/polyml.ML
@@ -37,7 +37,8 @@ struct
  open ML_System;

  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-val save_state = PolyML.SaveState.saveState;
+fun save_state file =
+    PolyML.SaveState.saveChild (file, length
(PolyML.SaveState.showHierarchy ()))


In L4.verified we are happy to use this patch for now, since no one in
our group has run into the associated problems.



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