189 for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
189 for parallel checking of theories and proofs. The default \<open>0\<close> means that a |
190 sensible maximum value is determined by the underlying hardware. For |
190 sensible maximum value is determined by the underlying hardware. For |
191 machines with many cores or with hyperthreading, this is often requires |
191 machines with many cores or with hyperthreading, this is often requires |
192 manual adjustment (on the command-line or within personal settings or |
192 manual adjustment (on the command-line or within personal settings or |
193 preferences, not within a session \<^verbatim>\<open>ROOT\<close>). |
193 preferences, not within a session \<^verbatim>\<open>ROOT\<close>). |
|
194 |
|
195 \<^item> @{system_option_def "checkpoint"} helps to fine-tune the global heap |
|
196 space management. This is relevant for big sessions that may exhaust the |
|
197 small 32-bit address space of the ML process (which is used by default). |
|
198 When the option is enabled for some \isakeyword{theories} block, a full |
|
199 sharing stage of immutable values in memory happens \<^emph>\<open>before\<close> loading the |
|
200 specified theories. |
194 |
201 |
195 \<^item> @{system_option_def "condition"} specifies a comma-separated list of |
202 \<^item> @{system_option_def "condition"} specifies a comma-separated list of |
196 process environment variables (or Isabelle settings) that are required for |
203 process environment variables (or Isabelle settings) that are required for |
197 the subsequent theories to be processed. Conditions are considered |
204 the subsequent theories to be processed. Conditions are considered |
198 ``true'' if the corresponding environment value is defined and non-empty. |
205 ``true'' if the corresponding environment value is defined and non-empty. |