213 for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
213 for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
214 sensible maximum value is determined by the underlying hardware. For |
214 sensible maximum value is determined by the underlying hardware. For |
215 machines with many cores or with hyperthreading, this is often requires |
215 machines with many cores or with hyperthreading, this is often requires |
216 manual adjustment (on the command-line or within personal settings or |
216 manual adjustment (on the command-line or within personal settings or |
217 preferences, not within a session \<^verbatim>\<open>ROOT\<close>). |
217 preferences, not within a session \<^verbatim>\<open>ROOT\<close>). |
218 |
|
219 \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap |
|
220 space management. This is relevant for big sessions that may exhaust the |
|
221 small 32-bit address space of the ML process (which is used by default). |
|
222 When the option is enabled for some \isakeyword{theories} block, a full |
|
223 sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the |
|
224 specified theories. |
|
225 |
218 |
226 \<^item> @{system_option_def "condition"} specifies a comma-separated list of |
219 \<^item> @{system_option_def "condition"} specifies a comma-separated list of |
227 process environment variables (or Isabelle settings) that are required for |
220 process environment variables (or Isabelle settings) that are required for |
228 the subsequent theories to be processed. Conditions are considered |
221 the subsequent theories to be processed. Conditions are considered |
229 ``true'' if the corresponding environment value is defined and non-empty. |
222 ``true'' if the corresponding environment value is defined and non-empty. |