# HG changeset patch
# User wenzelm
# Date 1473351537 -7200
# Node ID b24d0e53dd03264047f99be86fed64673c44d36d
# Parent  9321b3d50abdd444bbd3e838e1ed46c887cdf6cf
option "checkpoint" helps to fine-tune global heap space management;

diff -r 9321b3d50abd -r b24d0e53dd03 NEWS
--- a/NEWS	Thu Sep 08 10:35:08 2016 +0200
+++ b/NEWS	Thu Sep 08 18:18:57 2016 +0200
@@ -864,6 +864,11 @@
 * Poly/ML heaps now follow the hierarchy of sessions, and thus require
 much less disk space.
 
+* System option "checkpoint" helps to fine-tune the global heap space
+management of isabelle build. This is relevant for big sessions that may
+exhaust the small 32-bit address space of the ML process (which is used
+by default).
+
 
 
 New in Isabelle2016 (February 2016)
diff -r 9321b3d50abd -r b24d0e53dd03 etc/options
--- a/etc/options	Thu Sep 08 10:35:08 2016 +0200
+++ b/etc/options	Thu Sep 08 18:18:57 2016 +0200
@@ -105,6 +105,9 @@
 option process_output_tail : int = 40
   -- "build process output tail shown to user (in lines, 0 = unlimited)"
 
+option checkpoint : bool = false
+  -- "checkpoint for theories during build process (heap compression)"
+
 
 section "ML System"
 
diff -r 9321b3d50abd -r b24d0e53dd03 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu Sep 08 10:35:08 2016 +0200
+++ b/src/Doc/System/Sessions.thy	Thu Sep 08 18:18:57 2016 +0200
@@ -192,6 +192,13 @@
     manual adjustment (on the command-line or within personal settings or
     preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
 
+    \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
+    space management. This is relevant for big sessions that may exhaust the
+    small 32-bit address space of the ML process (which is used by default).
+    When the option is enabled for some \isakeyword{theories} block, a full
+    sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
+    specified theories.
+
     \<^item> @{system_option_def "condition"} specifies a comma-separated list of
     process environment variables (or Isabelle settings) that are required for
     the subsequent theories to be processed. Conditions are considered
diff -r 9321b3d50abd -r b24d0e53dd03 src/HOL/ROOT
--- a/src/HOL/ROOT	Thu Sep 08 10:35:08 2016 +0200
+++ b/src/HOL/ROOT	Thu Sep 08 18:18:57 2016 +0200
@@ -20,7 +20,8 @@
   *}
   options [document = false, quick_and_dirty = false]
   theories Proofs (*sequential change of global flag!*)
-  theories "~~/src/HOL/Library/Old_Datatype"
+  theories List
+  theories [checkpoint] "~~/src/HOL/Library/Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
     "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
diff -r 9321b3d50abd -r b24d0e53dd03 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Sep 08 10:35:08 2016 +0200
+++ b/src/Pure/Tools/build.ML	Thu Sep 08 18:18:57 2016 +0200
@@ -106,7 +106,8 @@
     val conds = filter_out (can getenv_strict) condition;
   in
     if null conds then
-      (Options.set_default options;
+      (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
+        Options.set_default options;
         Isabelle_Process.init_options ();
         (Thy_Info.use_theories {
           document = Present.document_enabled (Options.string options "document"),