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