--- a/NEWS Tue Jan 29 22:47:45 2019 +0100
+++ b/NEWS Wed Jan 30 13:25:33 2019 +0100
@@ -261,6 +261,8 @@
* Update to Java 11: the latest long-term support version of OpenJDK.
+* System option "checkpoint" has been discontinued: obsolete thanks to
+improved memory management in Poly/ML.
New in Isabelle2018 (August 2018)
--- a/etc/options Tue Jan 29 22:47:45 2019 +0100
+++ b/etc/options Wed Jan 30 13:25:33 2019 +0100
@@ -113,9 +113,6 @@
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)"
-
option profiling : string = ""
-- "ML profiling (possible values: time, allocations)"
--- a/src/Doc/System/Sessions.thy Tue Jan 29 22:47:45 2019 +0100
+++ b/src/Doc/System/Sessions.thy Wed Jan 30 13:25:33 2019 +0100
@@ -216,13 +216,6 @@
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/Pure/Tools/build.ML Tue Jan 29 22:47:45 2019 +0100
+++ b/src/Pure/Tools/build.ML Wed Jan 30 13:25:33 2019 +0100
@@ -119,8 +119,7 @@
val conds = filter_out (can getenv_strict) condition;
in
if null conds then
- (if Options.bool options "checkpoint" then ML_Heap.share_common_data () else ();
- Options.set_default options;
+ (Options.set_default options;
Isabelle_Process.init_options ();
Future.fork I;
(Thy_Info.use_theories context qualifier master_dir