option "checkpoint" helps to fine-tune global heap space management;
authorwenzelm
Thu Sep 08 18:18:57 2016 +0200 (2016-09-08)
changeset 63827b24d0e53dd03
parent 63826 9321b3d50abd
child 63828 ca467e73f912
option "checkpoint" helps to fine-tune global heap space management;
NEWS
etc/options
src/Doc/System/Sessions.thy
src/HOL/ROOT
src/Pure/Tools/build.ML
     1.1 --- a/NEWS	Thu Sep 08 10:35:08 2016 +0200
     1.2 +++ b/NEWS	Thu Sep 08 18:18:57 2016 +0200
     1.3 @@ -864,6 +864,11 @@
     1.4  * Poly/ML heaps now follow the hierarchy of sessions, and thus require
     1.5  much less disk space.
     1.6  
     1.7 +* System option "checkpoint" helps to fine-tune the global heap space
     1.8 +management of isabelle build. This is relevant for big sessions that may
     1.9 +exhaust the small 32-bit address space of the ML process (which is used
    1.10 +by default).
    1.11 +
    1.12  
    1.13  
    1.14  New in Isabelle2016 (February 2016)
     2.1 --- a/etc/options	Thu Sep 08 10:35:08 2016 +0200
     2.2 +++ b/etc/options	Thu Sep 08 18:18:57 2016 +0200
     2.3 @@ -105,6 +105,9 @@
     2.4  option process_output_tail : int = 40
     2.5    -- "build process output tail shown to user (in lines, 0 = unlimited)"
     2.6  
     2.7 +option checkpoint : bool = false
     2.8 +  -- "checkpoint for theories during build process (heap compression)"
     2.9 +
    2.10  
    2.11  section "ML System"
    2.12  
     3.1 --- a/src/Doc/System/Sessions.thy	Thu Sep 08 10:35:08 2016 +0200
     3.2 +++ b/src/Doc/System/Sessions.thy	Thu Sep 08 18:18:57 2016 +0200
     3.3 @@ -192,6 +192,13 @@
     3.4      manual adjustment (on the command-line or within personal settings or
     3.5      preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
     3.6  
     3.7 +    \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap
     3.8 +    space management. This is relevant for big sessions that may exhaust the
     3.9 +    small 32-bit address space of the ML process (which is used by default).
    3.10 +    When the option is enabled for some \isakeyword{theories} block, a full
    3.11 +    sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the
    3.12 +    specified theories.
    3.13 +
    3.14      \<^item> @{system_option_def "condition"} specifies a comma-separated list of
    3.15      process environment variables (or Isabelle settings) that are required for
    3.16      the subsequent theories to be processed. Conditions are considered
     4.1 --- a/src/HOL/ROOT	Thu Sep 08 10:35:08 2016 +0200
     4.2 +++ b/src/HOL/ROOT	Thu Sep 08 18:18:57 2016 +0200
     4.3 @@ -20,7 +20,8 @@
     4.4    *}
     4.5    options [document = false, quick_and_dirty = false]
     4.6    theories Proofs (*sequential change of global flag!*)
     4.7 -  theories "~~/src/HOL/Library/Old_Datatype"
     4.8 +  theories List
     4.9 +  theories [checkpoint] "~~/src/HOL/Library/Old_Datatype"
    4.10    files
    4.11      "Tools/Quickcheck/Narrowing_Engine.hs"
    4.12      "Tools/Quickcheck/PNF_Narrowing_Engine.hs"
     5.1 --- a/src/Pure/Tools/build.ML	Thu Sep 08 10:35:08 2016 +0200
     5.2 +++ b/src/Pure/Tools/build.ML	Thu Sep 08 18:18:57 2016 +0200
     5.3 @@ -106,7 +106,8 @@
     5.4      val conds = filter_out (can getenv_strict) condition;
     5.5    in
     5.6      if null conds then
     5.7 -      (Options.set_default options;
     5.8 +      (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
     5.9 +        Options.set_default options;
    5.10          Isabelle_Process.init_options ();
    5.11          (Thy_Info.use_theories {
    5.12            document = Present.document_enabled (Options.string options "document"),