[isabelle-dev] Proposal to use hierarchical heaps with Poly/ML
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
@@ -37,7 +37,8 @@ struct
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-val save_state = PolyML.SaveState.saveState;
+fun save_state file =
+ PolyML.SaveState.saveChild (file, length
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