200 |
200 |
201 For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be used to guard |
201 For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be used to guard |
202 extraordinary theories, which are meant to be enabled explicitly via some |
202 extraordinary theories, which are meant to be enabled explicitly via some |
203 shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close> before invoking @{tool build}. |
203 shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close> before invoking @{tool build}. |
204 |
204 |
205 \<^item> @{system_option_def "timeout"} specifies a real wall-clock timeout (in |
205 \<^item> @{system_option_def "timeout"} and @{system_option_def "timeout_scale"} |
206 seconds) for the session as a whole. The timer is controlled outside the |
206 specify a real wall-clock timeout for the session as a whole: the two |
207 ML process by the JVM that runs Isabelle/Scala. Thus it is relatively |
207 values are multiplied and taken as the number of seconds. Typically, |
208 reliable in canceling processes that get out of control, even if there is |
208 @{system_option "timeout"} is given for individual sessions, and |
209 a deadlock without CPU time usage. |
209 @{system_option "timeout_scale"} as global adjustment to overall hardware |
|
210 performance. |
|
211 |
|
212 The timer is controlled outside the ML process by the JVM that runs |
|
213 Isabelle/Scala. Thus it is relatively reliable in canceling processes that |
|
214 get out of control, even if there is a deadlock without CPU time usage. |
210 |
215 |
211 The @{tool_def options} tool prints Isabelle system options. Its |
216 The @{tool_def options} tool prints Isabelle system options. Its |
212 command-line usage is: |
217 command-line usage is: |
213 @{verbatim [display] |
218 @{verbatim [display] |
214 \<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] |
219 \<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...] |
313 |
318 |
314 \<^medskip> |
319 \<^medskip> |
315 The build process depends on additional options |
320 The build process depends on additional options |
316 (\secref{sec:system-options}) that are passed to the prover eventually. The |
321 (\secref{sec:system-options}) that are passed to the prover eventually. The |
317 settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide |
322 settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide |
318 additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf |
323 additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>. |
319 threads=4"\<close>. Moreover, the environment of system build options may be |
324 Moreover, the environment of system build options may be augmented on the |
320 augmented on the command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, |
325 command line via \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<^verbatim>\<open>-o\<close>~\<open>name\<close>, which abbreviates |
321 which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple |
326 \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on |
322 occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given order. |
327 the command-line are applied in the given order. |
323 |
328 |
324 \<^medskip> |
329 \<^medskip> |
325 Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected |
330 Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected |
326 sessions. By default, images are only saved for inner nodes of the hierarchy |
331 sessions. By default, images are only saved for inner nodes of the hierarchy |
327 of sessions, as required for other sessions to continue later on. |
332 of sessions, as required for other sessions to continue later on. |