--- 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)
--- 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"
--- 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
--- 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"
--- 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"),