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

[Japheth Lim]

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 ()))

  end;



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

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.