--- a/src/Doc/System/Basics.thy Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Basics.thy Wed Nov 04 20:18:46 2015 +0100
@@ -1,35 +1,34 @@
+(*:wrap=hard:maxLineLen=78:*)
+
theory Basics
imports Base
begin
chapter \<open>The Isabelle system environment\<close>
-text \<open>This manual describes Isabelle together with related tools and
- user interfaces as seen from a system oriented view. See also the
- \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite "isabelle-isar-ref"} for
- the actual Isabelle input language and related concepts, and
- \<^emph>\<open>The Isabelle/Isar Implementation
+text \<open>
+ This manual describes Isabelle together with related tools and user
+ interfaces as seen from a system oriented view. See also the \<^emph>\<open>Isabelle/Isar
+ Reference Manual\<close> @{cite "isabelle-isar-ref"} for the actual Isabelle input
+ language and related concepts, and \<^emph>\<open>The Isabelle/Isar Implementation
Manual\<close> @{cite "isabelle-implementation"} for the main concepts of the
underlying implementation in Isabelle/ML.
\<^medskip>
- The Isabelle system environment provides the following
- basic infrastructure to integrate tools smoothly.
+ The Isabelle system environment provides the following basic infrastructure
+ to integrate tools smoothly.
- \<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process
- environment variables to all Isabelle executables (including tools
- and user interfaces).
+ \<^enum> The \<^emph>\<open>Isabelle settings\<close> mechanism provides process environment variables
+ to all Isabelle executables (including tools and user interfaces).
- \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref
- "isabelle_process"}) runs logic sessions either interactively or in
- batch mode. In particular, this view abstracts over the invocation
- of the actual ML system to be used. Regular users rarely need to
- care about the low-level process.
+ \<^enum> The raw \<^emph>\<open>Isabelle process\<close> (@{executable_ref "isabelle_process"}) runs
+ logic sessions either interactively or in batch mode. In particular, this
+ view abstracts over the invocation of the actual ML system to be used.
+ Regular users rarely need to care about the low-level process.
- \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref
- isabelle}) provides a generic startup environment Isabelle related
- utilities, user interfaces etc. Such tools automatically benefit
- from the settings mechanism.
+ \<^enum> The main \<^emph>\<open>Isabelle tool wrapper\<close> (@{executable_ref isabelle}) provides a
+ generic startup environment Isabelle related utilities, user interfaces etc.
+ Such tools automatically benefit from the settings mechanism.
\<close>
@@ -37,299 +36,270 @@
text \<open>
The Isabelle system heavily depends on the \<^emph>\<open>settings
- mechanism\<close>\indexbold{settings}. Essentially, this is a statically
- scoped collection of environment variables, such as @{setting
- ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}. These
- variables are \<^emph>\<open>not\<close> intended to be set directly from the shell,
- though. Isabelle employs a somewhat more sophisticated scheme of
- \<^emph>\<open>settings files\<close> --- one for site-wide defaults, another for
- additional user-specific modifications. With all configuration
- variables in clearly defined places, this scheme is more
- maintainable and user-friendly than global shell environment
- variables.
+ mechanism\<close>\indexbold{settings}. Essentially, this is a statically scoped
+ collection of environment variables, such as @{setting ISABELLE_HOME},
+ @{setting ML_SYSTEM}, @{setting ML_HOME}. These variables are \<^emph>\<open>not\<close>
+ intended to be set directly from the shell, though. Isabelle employs a
+ somewhat more sophisticated scheme of \<^emph>\<open>settings files\<close> --- one for
+ site-wide defaults, another for additional user-specific modifications. With
+ all configuration variables in clearly defined places, this scheme is more
+ maintainable and user-friendly than global shell environment variables.
- In particular, we avoid the typical situation where prospective
- users of a software package are told to put several things into
- their shell startup scripts, before being able to actually run the
- program. Isabelle requires none such administrative chores of its
- end-users --- the executables can be invoked straight away.
- Occasionally, users would still want to put the @{file
- "$ISABELLE_HOME/bin"} directory into their shell's search path, but
+ In particular, we avoid the typical situation where prospective users of a
+ software package are told to put several things into their shell startup
+ scripts, before being able to actually run the program. Isabelle requires
+ none such administrative chores of its end-users --- the executables can be
+ invoked straight away. Occasionally, users would still want to put the
+ @{file "$ISABELLE_HOME/bin"} directory into their shell's search path, but
this is not required.
\<close>
subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
-text \<open>Isabelle executables need to be run within a proper settings
- environment. This is bootstrapped as described below, on the first
- invocation of one of the outer wrapper scripts (such as
- @{executable_ref isabelle}). This happens only once for each
- process tree, i.e.\ the environment is passed to subprocesses
- according to regular Unix conventions.
+text \<open>
+ Isabelle executables need to be run within a proper settings environment.
+ This is bootstrapped as described below, on the first invocation of one of
+ the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
+ only once for each process tree, i.e.\ the environment is passed to
+ subprocesses according to regular Unix conventions.
+
+ \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
+ automatically from the location of the binary that has been run.
- \<^enum> The special variable @{setting_def ISABELLE_HOME} is
- determined automatically from the location of the binary that has
- been run.
-
- You should not try to set @{setting ISABELLE_HOME} manually. Also
- note that the Isabelle executables either have to be run from their
- original location in the distribution directory, or via the
- executable objects created by the @{tool install} tool. Symbolic
- links are admissible, but a plain copy of the @{file
- "$ISABELLE_HOME/bin"} files will not work!
+ You should not try to set @{setting ISABELLE_HOME} manually. Also note
+ that the Isabelle executables either have to be run from their original
+ location in the distribution directory, or via the executable objects
+ created by the @{tool install} tool. Symbolic links are admissible, but a
+ plain copy of the @{file "$ISABELLE_HOME/bin"} files will not work!
+
+ \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
+ @{executable_ref bash} shell script with the auto-export option for
+ variables enabled.
- \<^enum> The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
- @{executable_ref bash} shell script with the auto-export option for
- variables enabled.
-
- This file holds a rather long list of shell variable assigments,
- thus providing the site-wide default settings. The Isabelle
- distribution already contains a global settings file with sensible
- defaults for most variables. When installing the system, only a few
- of these may have to be adapted (probably @{setting ML_SYSTEM}
- etc.).
-
- \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
- exists) is run in the same way as the site default settings. Note
- that the variable @{setting ISABELLE_HOME_USER} has already been set
- before --- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
-
- Thus individual users may override the site-wide defaults.
- Typically, a user settings file contains only a few lines, with some
- assignments that are actually changed. Never copy the central
- @{file "$ISABELLE_HOME/etc/settings"} file!
+ This file holds a rather long list of shell variable assignments, thus
+ providing the site-wide default settings. The Isabelle distribution
+ already contains a global settings file with sensible defaults for most
+ variables. When installing the system, only a few of these may have to be
+ adapted (probably @{setting ML_SYSTEM} etc.).
+
+ \<^enum> The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
+ exists) is run in the same way as the site default settings. Note that the
+ variable @{setting ISABELLE_HOME_USER} has already been set before ---
+ usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
+ Thus individual users may override the site-wide defaults. Typically, a
+ user settings file contains only a few lines, with some assignments that
+ are actually changed. Never copy the central @{file
+ "$ISABELLE_HOME/etc/settings"} file!
- Since settings files are regular GNU @{executable_def bash} scripts,
- one may use complex shell commands, such as \<^verbatim>\<open>if\<close> or
- \<^verbatim>\<open>case\<close> statements to set variables depending on the
- system architecture or other environment variables. Such advanced
- features should be added only with great care, though. In
- particular, external environment references should be kept at a
+ Since settings files are regular GNU @{executable_def bash} scripts, one may
+ use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
+ variables depending on the system architecture or other environment
+ variables. Such advanced features should be added only with great care,
+ though. In particular, external environment references should be kept at a
minimum.
\<^medskip>
A few variables are somewhat special:
- \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
- automatically to the absolute path names of the @{executable
- "isabelle_process"} and @{executable isabelle} executables,
- respectively.
-
- \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
- the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
- the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
- to its value.
+ \<^item> @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
+ automatically to the absolute path names of the @{executable
+ "isabelle_process"} and @{executable isabelle} executables, respectively.
+ \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
+ distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
+ @{setting ML_IDENTIFIER}) appended automatically to its value.
\<^medskip>
- Note that the settings environment may be inspected with
- the @{tool getenv} tool. This might help to figure out the effect
- of complex settings scripts.\<close>
+ Note that the settings environment may be inspected with the @{tool getenv}
+ tool. This might help to figure out the effect of complex settings scripts.
+\<close>
subsection \<open>Common variables\<close>
text \<open>
- This is a reference of common Isabelle settings variables. Note that
- the list is somewhat open-ended. Third-party utilities or interfaces
- may add their own selection. Variables that are special in some
- sense are marked with \<open>\<^sup>*\<close>.
+ This is a reference of common Isabelle settings variables. Note that the
+ list is somewhat open-ended. Third-party utilities or interfaces may add
+ their own selection. Variables that are special in some sense are marked
+ with \<open>\<^sup>*\<close>.
- \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform
- user home directory. On Unix systems this is usually the same as
- @{setting HOME}, but on Windows it is the regular home directory of
- the user, not the one of within the Cygwin root
- file-system.\<^footnote>\<open>Cygwin itself offers another choice whether
- its HOME should point to the @{file_unchecked "/home"} directory tree or the
+ \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
+ On Unix systems this is usually the same as @{setting HOME}, but on Windows
+ it is the regular home directory of the user, not the one of within the
+ Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
+ HOME should point to the @{file_unchecked "/home"} directory tree or the
Windows user home.\<close>
- \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the
- top-level Isabelle distribution directory. This is automatically
- determined from the Isabelle executable that has been invoked. Do
- not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
-
- \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific
- counterpart of @{setting ISABELLE_HOME}. The default value is
- relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare
- circumstances this may be changed in the global setting file.
- Typically, the @{setting ISABELLE_HOME_USER} directory mimics
- @{setting ISABELLE_HOME} to some extend. In particular, site-wide
- defaults may be overridden by a private
- \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
+ \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
+ Isabelle distribution directory. This is automatically determined from the
+ Isabelle executable that has been invoked. Do not attempt to set @{setting
+ ISABELLE_HOME} yourself from the shell!
- \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is
- automatically set to the general platform family: \<^verbatim>\<open>linux\<close>,
- \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
+ \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
+ @{setting ISABELLE_HOME}. The default value is relative to @{file_unchecked
+ "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
+ global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
+ mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
+ defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
+
+ \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
+ general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
platform-dependent tools usually need to refer to the more specific
identification according to @{setting ISABELLE_PLATFORM}, @{setting
ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
- \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically
- set to a symbolic identifier for the underlying hardware and
- operating system. The Isabelle platform identification always
- refers to the 32 bit variant, even this is a 64 bit machine. Note
- that the ML or Java runtime may have a different idea, depending on
- which binaries are actually run.
+ \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
+ identifier for the underlying hardware and operating system. The Isabelle
+ platform identification always refers to the 32 bit variant, even this is a
+ 64 bit machine. Note that the ML or Java runtime may have a different idea,
+ depending on which binaries are actually run.
- \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to
- @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
- on a platform that supports this; the value is empty for 32 bit.
- Note that the following bash expression (including the quotes)
- prefers the 64 bit platform, if that is available:
+ \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
+ ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
+ that supports this; the value is empty for 32 bit. Note that the following
+ bash expression (including the quotes) prefers the 64 bit platform, if that
+ is available:
@{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
- \<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting
- ISABELLE_TOOL}\<open>\<^sup>*\<close>] are automatically set to the full path
- names of the @{executable "isabelle_process"} and @{executable
- isabelle} executables, respectively. Thus other tools and scripts
- need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
- on the current search path of the shell.
-
- \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers
- to the name of this Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
+ \<^descr>[@{setting_def ISABELLE_PROCESS}\<open>\<^sup>*\<close>, @{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] are
+ automatically set to the full path names of the @{executable
+ "isabelle_process"} and @{executable isabelle} executables, respectively.
+ Thus other tools and scripts need not assume that the @{file
+ "$ISABELLE_HOME/bin"} directory is on the current search path of the shell.
- \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
- @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
- ML_IDENTIFIER}\<open>\<^sup>*\<close>] specify the underlying ML system
- to be used for Isabelle. There is only a fixed set of admissable
- @{setting ML_SYSTEM} names (see the @{file
+ \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012\<close>''.
+
+ \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
+ ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
+ specify the underlying ML system to be used for Isabelle. There is only a
+ fixed set of admissable @{setting ML_SYSTEM} names (see the @{file
"$ISABELLE_HOME/etc/settings"} file of the distribution).
-
+
The actual compiler binary will be run from the directory @{setting
- ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
- command line. The optional @{setting ML_PLATFORM} may specify the
- binary format of ML heap images, which is useful for cross-platform
- installations. The value of @{setting ML_IDENTIFIER} is
- automatically obtained by composing the values of @{setting
- ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
+ ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
+ The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
+ images, which is useful for cross-platform installations. The value of
+ @{setting ML_IDENTIFIER} is automatically obtained by composing the values
+ of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
+ values.
- \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close>
- for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to
- SML/NJ where it is empty. This is particularly useful with the
- build option @{system_option condition}
- (\secref{sec:system-options}) to restrict big sessions to something
- that SML/NJ can still handle.
+ \<^descr>[@{setting_def ML_SYSTEM_POLYML}\<open>\<^sup>*\<close>] is \<^verbatim>\<open>true\<close> for @{setting ML_SYSTEM}
+ values derived from Poly/ML, as opposed to SML/NJ where it is empty. This is
+ particularly useful with the build option @{system_option condition}
+ (\secref{sec:system-options}) to restrict big sessions to something that
+ SML/NJ can still handle.
- \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
- (Java Development Kit) installation with \<^verbatim>\<open>javac\<close> and
- \<^verbatim>\<open>jar\<close> executables. This is essential for Isabelle/Scala
- and other JVM-based tools to work properly. Note that conventional
- \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
+ \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
+ Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
+ essential for Isabelle/Scala and other JVM-based tools to work properly.
+ Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
Environment), not JDK.
-
- \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories
- (separated by colons) where Isabelle logic images may reside. When
- looking up heaps files, the value of @{setting ML_IDENTIFIER} is
- appended to each component internally.
-
- \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a
- directory where output heap files should be stored by default. The
- ML system and Isabelle version identifier is appended here, too.
-
- \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
- theory browser information (HTML text, graph data, and printable
- documents) is stored (see also \secref{sec:info}). The default
- value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
-
- \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
- load if none is given explicitely by the user. The default value is
- \<^verbatim>\<open>HOL\<close>.
-
- \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the
- line editor for the @{tool_ref console} interface.
+
+ \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
+ colons) where Isabelle logic images may reside. When looking up heaps files,
+ the value of @{setting ML_IDENTIFIER} is appended to each component
+ internally.
+
+ \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
+ should be stored by default. The ML system and Isabelle version identifier
+ is appended here, too.
+
+ \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
+ browser information (HTML text, graph data, and printable documents) is
+ stored (see also \secref{sec:info}). The default value is @{file_unchecked
+ "$ISABELLE_HOME_USER/browser_info"}.
+
+ \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
+ is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
+
+ \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
+ @{tool_ref console} interface.
- \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def
- ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}
- related tools for Isabelle document preparation (see also
- \secref{sec:tool-latex}).
-
- \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
- directories that are scanned by @{executable isabelle} for external
- utility programs (see also \secref{sec:isabelle-tool}).
-
- \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of
- directories with documentation files.
+ \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
+ @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
+ document preparation (see also \secref{sec:tool-latex}).
+
+ \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
+ that are scanned by @{executable isabelle} for external utility programs
+ (see also \secref{sec:isabelle-tool}).
- \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used
- for displaying \<^verbatim>\<open>pdf\<close> files.
+ \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
+ with documentation files.
+
+ \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
+ \<^verbatim>\<open>pdf\<close> files.
- \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used
- for displaying \<^verbatim>\<open>dvi\<close> files.
-
- \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the
- prefix from which any running @{executable "isabelle_process"}
- derives an individual directory for temporary files.
+ \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
+ \<^verbatim>\<open>dvi\<close> files.
+
+ \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
+ running @{executable "isabelle_process"} derives an individual directory for
+ temporary files.
\<close>
subsection \<open>Additional components \label{sec:components}\<close>
-text \<open>Any directory may be registered as an explicit \<^emph>\<open>Isabelle
- component\<close>. The general layout conventions are that of the main
- Isabelle distribution itself, and the following two files (both
- optional) have a special meaning:
+text \<open>
+ Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
+ general layout conventions are that of the main Isabelle distribution
+ itself, and the following two files (both optional) have a special meaning:
- \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are
- initialized when bootstrapping the overall Isabelle environment,
- cf.\ \secref{sec:boot}. As usual, the content is interpreted as a
- \<^verbatim>\<open>bash\<close> script. It may refer to the component's enclosing
- directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
+ \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
+ bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
+ usual, the content is interpreted as a \<^verbatim>\<open>bash\<close> script. It may refer to the
+ component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
- For example, the following setting allows to refer to files within
- the component later on, without having to hardwire absolute paths:
- @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
+ For example, the following setting allows to refer to files within the
+ component later on, without having to hardwire absolute paths:
+ @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
- Components can also add to existing Isabelle settings such as
- @{setting_def ISABELLE_TOOLS}, in order to provide
- component-specific tools that can be invoked by end-users. For
- example:
- @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
+ Components can also add to existing Isabelle settings such as
+ @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
+ tools that can be invoked by end-users. For example:
+ @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
- \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further
- sub-components of the same structure. The directory specifications
- given here can be either absolute (with leading \<^verbatim>\<open>/\<close>) or
- relative to the component's main directory.
+ \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
+ structure. The directory specifications given here can be either absolute
+ (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
-
- The root of component initialization is @{setting ISABELLE_HOME}
- itself. After initializing all of its sub-components recursively,
- @{setting ISABELLE_HOME_USER} is included in the same manner (if
- that directory exists). This allows to install private components
- via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
- often more convenient to do that programmatically via the
- \<^verbatim>\<open>init_component\<close> shell function in the \<^verbatim>\<open>etc/settings\<close>
- script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
- directory). For example:
+ The root of component initialization is @{setting ISABELLE_HOME} itself.
+ After initializing all of its sub-components recursively, @{setting
+ ISABELLE_HOME_USER} is included in the same manner (if that directory
+ exists). This allows to install private components via @{file_unchecked
+ "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
+ to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
+ \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
+ directory). For example:
@{verbatim [display] \<open>init_component "$HOME/screwdriver-2.0"\<close>}
- This is tolerant wrt.\ missing component directories, but might
- produce a warning.
+ This is tolerant wrt.\ missing component directories, but might produce a
+ warning.
\<^medskip>
- More complex situations may be addressed by initializing
- components listed in a given catalog file, relatively to some base
- directory:
+ More complex situations may be addressed by initializing components listed
+ in a given catalog file, relatively to some base directory:
@{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
- The component directories listed in the catalog file are treated as
- relative to the given base directory.
+ The component directories listed in the catalog file are treated as relative
+ to the given base directory.
- See also \secref{sec:tool-components} for some tool-support for
- resolving components that are formally initialized but not installed
- yet.
+ See also \secref{sec:tool-components} for some tool-support for resolving
+ components that are formally initialized but not installed yet.
\<close>
section \<open>The raw Isabelle process \label{sec:isabelle-process}\<close>
text \<open>
- The @{executable_def "isabelle_process"} executable runs bare-bones
- Isabelle logic sessions --- either interactively or in batch mode.
- It provides an abstraction over the underlying ML system, and over
- the actual heap file locations. Its usage is:
+ The @{executable_def "isabelle_process"} executable runs bare-bones Isabelle
+ logic sessions --- either interactively or in batch mode. It provides an
+ abstraction over the underlying ML system, and over the actual heap file
+ locations. Its usage is:
@{verbatim [display]
\<open>Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
@@ -349,123 +319,111 @@
actual file names (containing at least one /).
If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.\<close>}
- Input files without path specifications are looked up in the
- @{setting ISABELLE_PATH} setting, which may consist of multiple
- components separated by colons --- these are tried in the given
- order with the value of @{setting ML_IDENTIFIER} appended
- internally. In a similar way, base names are relative to the
- directory specified by @{setting ISABELLE_OUTPUT}. In any case,
- actual file locations may also be given by including at least one
- slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to
- refer to the current directory).
+ Input files without path specifications are looked up in the @{setting
+ ISABELLE_PATH} setting, which may consist of multiple components separated
+ by colons --- these are tried in the given order with the value of @{setting
+ ML_IDENTIFIER} appended internally. In a similar way, base names are
+ relative to the directory specified by @{setting ISABELLE_OUTPUT}. In any
+ case, actual file locations may also be given by including at least one
+ slash (\<^verbatim>\<open>/\<close>) in the name (hint: use \<^verbatim>\<open>./\<close> to refer to the current
+ directory).
\<close>
subsubsection \<open>Options\<close>
text \<open>
- If the input heap file does not have write permission bits set, or
- the \<^verbatim>\<open>-r\<close> option is given explicitly, then the session
- started will be read-only. That is, the ML world cannot be
- committed back into the image file. Otherwise, a writable session
- enables commits into either the input file, or into another output
- heap file (if that is given as the second argument on the command
+ If the input heap file does not have write permission bits set, or the \<^verbatim>\<open>-r\<close>
+ option is given explicitly, then the session started will be read-only. That
+ is, the ML world cannot be committed back into the image file. Otherwise, a
+ writable session enables commits into either the input file, or into another
+ output heap file (if that is given as the second argument on the command
line).
- The read-write state of sessions is determined at startup only, it
- cannot be changed intermediately. Also note that heap images may
- require considerable amounts of disk space (hundreds of MB or some GB).
- Users are responsible for themselves to dispose their heap files
- when they are no longer needed.
+ The read-write state of sessions is determined at startup only, it cannot be
+ changed intermediately. Also note that heap images may require considerable
+ amounts of disk space (hundreds of MB or some GB). Users are responsible for
+ themselves to dispose their heap files when they are no longer needed.
\<^medskip>
- The \<^verbatim>\<open>-w\<close> option makes the output heap file
- read-only after terminating. Thus subsequent invocations cause the
- logic image to be read-only automatically.
+ The \<^verbatim>\<open>-w\<close> option makes the output heap file read-only after terminating.
+ Thus subsequent invocations cause the logic image to be read-only
+ automatically.
\<^medskip>
- Using the \<^verbatim>\<open>-e\<close> option, arbitrary ML code may be
- passed to the Isabelle session from the command line. Multiple
- \<^verbatim>\<open>-e\<close> options are evaluated in the given order. Strange things
- may happen when erroneous ML code is provided. Also make sure that
- the ML commands are terminated properly by semicolon.
+ Using the \<^verbatim>\<open>-e\<close> option, arbitrary ML code may be passed to the Isabelle
+ session from the command line. Multiple \<^verbatim>\<open>-e\<close> options are evaluated in the
+ given order. Strange things may happen when erroneous ML code is provided.
+ Also make sure that the ML commands are terminated properly by semicolon.
\<^medskip>
- The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes
- to be made active for this session. Typically, this is used by some
- user interface, e.g.\ to enable output of proper mathematical
- symbols.
+ The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
+ session. Typically, this is used by some user interface, e.g.\ to enable
+ output of proper mathematical symbols.
\<^medskip>
- Isabelle normally enters an interactive top-level loop
- (after processing the \<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close>
- option inhibits interaction, thus providing a pure batch mode
- facility.
+ Isabelle normally enters an interactive top-level loop (after processing the
+ \<^verbatim>\<open>-e\<close> texts). The \<^verbatim>\<open>-q\<close> option inhibits interaction, thus providing a pure
+ batch mode facility.
\<^medskip>
- Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system
- options for this process, see also \secref{sec:system-options}.
- Alternatively, option \<^verbatim>\<open>-O\<close> specifies the full environment of
- system options as a file in YXML format (according to the Isabelle/Scala
- function \<^verbatim>\<open>isabelle.Options.encode\<close>).
+ Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
+ see also \secref{sec:system-options}. Alternatively, option \<^verbatim>\<open>-O\<close> specifies
+ the full environment of system options as a file in YXML format (according
+ to the Isabelle/Scala function \<^verbatim>\<open>isabelle.Options.encode\<close>).
\<^medskip>
- The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper
- for Isabelle/Scala, with a private protocol running over the specified TCP
- socket. Isabelle/ML and Isabelle/Scala provide various programming
- interfaces to invoke protocol functions over untyped strings and XML
- trees.
+ The \<^verbatim>\<open>-P\<close> option starts the Isabelle process wrapper for Isabelle/Scala,
+ with a private protocol running over the specified TCP socket. Isabelle/ML
+ and Isabelle/Scala provide various programming interfaces to invoke protocol
+ functions over untyped strings and XML trees.
\<^medskip>
- The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more
- secure by disabling some critical operations, notably runtime
- compilation and evaluation of ML source code.
+ The \<^verbatim>\<open>-S\<close> option makes the Isabelle process more secure by disabling some
+ critical operations, notably runtime compilation and evaluation of ML source
+ code.
\<close>
subsubsection \<open>Examples\<close>
text \<open>
- Run an interactive session of the default object-logic (as specified
- by the @{setting ISABELLE_LOGIC} setting) like this:
+ Run an interactive session of the default object-logic (as specified by the
+ @{setting ISABELLE_LOGIC} setting) like this:
@{verbatim [display] \<open>isabelle_process\<close>}
- Usually @{setting ISABELLE_LOGIC} refers to one of the standard
- logic images, which are read-only by default. A writable session
- --- based on \<^verbatim>\<open>HOL\<close>, but output to \<^verbatim>\<open>Test\<close> (in the
- directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
- may be invoked as follows:
+ Usually @{setting ISABELLE_LOGIC} refers to one of the standard logic
+ images, which are read-only by default. A writable session --- based on
+ \<^verbatim>\<open>HOL\<close>, but output to \<^verbatim>\<open>Test\<close> (in the directory specified by the @{setting
+ ISABELLE_OUTPUT} setting) --- may be invoked as follows:
@{verbatim [display] \<open>isabelle_process HOL Test\<close>}
- Ending this session normally (e.g.\ by typing control-D) dumps the
- whole ML system state into \<^verbatim>\<open>Test\<close> (be prepared for more
- than 100\,MB):
+ Ending this session normally (e.g.\ by typing control-D) dumps the whole ML
+ system state into \<^verbatim>\<open>Test\<close> (be prepared for more than 100\,MB):
- The \<^verbatim>\<open>Test\<close> session may be continued later (still in
- writable state) by: @{verbatim [display] \<open>isabelle_process Test\<close>}
+ The \<^verbatim>\<open>Test\<close> session may be continued later (still in writable state) by:
+ @{verbatim [display] \<open>isabelle_process Test\<close>}
A read-only \<^verbatim>\<open>Test\<close> session may be started by:
@{verbatim [display] \<open>isabelle_process -r Test\<close>}
\<^bigskip>
- The next example demonstrates batch execution of Isabelle.
- We retrieve the \<^verbatim>\<open>Main\<close> theory value from the theory loader
- within ML (observe the delicate quoting rules for the Bash shell
- vs.\ ML):
+ The next example demonstrates batch execution of Isabelle. We retrieve the
+ \<^verbatim>\<open>Main\<close> theory value from the theory loader within ML (observe the delicate
+ quoting rules for the Bash shell vs.\ ML):
@{verbatim [display] \<open>isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL\<close>}
- Note that the output text will be interspersed with additional junk
- messages by the ML runtime environment. The \<^verbatim>\<open>-W\<close> option
- allows to communicate with the Isabelle process via an external
- program in a more robust fashion.
+ Note that the output text will be interspersed with additional junk messages
+ by the ML runtime environment. The \<^verbatim>\<open>-W\<close> option allows to communicate with
+ the Isabelle process via an external program in a more robust fashion.
\<close>
section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
text \<open>
- All Isabelle related tools and interfaces are called via a common
- wrapper --- @{executable isabelle}:
+ All Isabelle related tools and interfaces are called via a common wrapper
+ --- @{executable isabelle}:
@{verbatim [display]
\<open>Usage: isabelle TOOL [ARGS ...]
@@ -474,20 +432,19 @@
Available tools:
...\<close>}
- In principle, Isabelle tools are ordinary executable scripts that
- are run within the Isabelle settings environment, see
- \secref{sec:settings}. The set of available tools is collected by
- @{executable isabelle} from the directories listed in the @{setting
- ISABELLE_TOOLS} setting. Do not try to call the scripts directly
- from the shell. Neither should you add the tool directories to your
- shell's search path!
+ In principle, Isabelle tools are ordinary executable scripts that are run
+ within the Isabelle settings environment, see \secref{sec:settings}. The set
+ of available tools is collected by @{executable isabelle} from the
+ directories listed in the @{setting ISABELLE_TOOLS} setting. Do not try to
+ call the scripts directly from the shell. Neither should you add the tool
+ directories to your shell's search path!
\<close>
subsubsection \<open>Examples\<close>
-text \<open>Show the list of available documentation of the Isabelle
- distribution:
+text \<open>
+ Show the list of available documentation of the Isabelle distribution:
@{verbatim [display] \<open>isabelle doc\<close>}
View a certain document as follows:
--- a/src/Doc/System/Misc.thy Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Misc.thy Wed Nov 04 20:18:46 2015 +0100
@@ -1,3 +1,5 @@
+(*:wrap=hard:maxLineLen=78:*)
+
theory Misc
imports Base
begin
@@ -5,25 +7,27 @@
chapter \<open>Miscellaneous tools \label{ch:tools}\<close>
text \<open>
- Subsequently we describe various Isabelle related utilities, given
- in alphabetical order.
+ Subsequently we describe various Isabelle related utilities, given in
+ alphabetical order.
\<close>
section \<open>Theory graph browser \label{sec:browse}\<close>
-text \<open>The Isabelle graph browser is a general tool for visualizing
- dependency graphs. Certain nodes of the graph (i.e.\ theories) can
- be grouped together in ``directories'', whose contents may be
- hidden, thus enabling the user to collapse irrelevant portions of
- information. The browser is written in Java, it can be used both as
- a stand-alone application and as an applet.\<close>
+text \<open>
+ The Isabelle graph browser is a general tool for visualizing dependency
+ graphs. Certain nodes of the graph (i.e.\ theories) can be grouped together
+ in ``directories'', whose contents may be hidden, thus enabling the user to
+ collapse irrelevant portions of information. The browser is written in Java,
+ it can be used both as a stand-alone application and as an applet.
+\<close>
subsection \<open>Invoking the graph browser\<close>
-text \<open>The stand-alone version of the graph browser is wrapped up as
- @{tool_def browser}:
+text \<open>
+ The stand-alone version of the graph browser is wrapped up as @{tool_def
+ browser}:
@{verbatim [display]
\<open>Usage: isabelle browser [OPTIONS] [GRAPHFILE]
@@ -32,35 +36,31 @@
-c cleanup -- remove GRAPHFILE after use
-o FILE output to FILE (ps, eps, pdf)\<close>}
- When no file name is specified, the browser automatically changes to
- the directory @{setting ISABELLE_BROWSER_INFO}.
+ When no file name is specified, the browser automatically changes to the
+ directory @{setting ISABELLE_BROWSER_INFO}.
\<^medskip>
- The \<^verbatim>\<open>-b\<close> option indicates that this is for
- administrative build only, i.e.\ no browser popup if no files are
- given.
+ The \<^verbatim>\<open>-b\<close> option indicates that this is for administrative build only, i.e.\
+ no browser popup if no files are given.
- The \<^verbatim>\<open>-c\<close> option causes the input file to be removed
- after use.
+ The \<^verbatim>\<open>-c\<close> option causes the input file to be removed after use.
- The \<^verbatim>\<open>-o\<close> option indicates batch-mode operation, with the
- output written to the indicated file; note that \<^verbatim>\<open>pdf\<close>
- produces an \<^verbatim>\<open>eps\<close> copy as well.
+ The \<^verbatim>\<open>-o\<close> option indicates batch-mode operation, with the output written to
+ the indicated file; note that \<^verbatim>\<open>pdf\<close> produces an \<^verbatim>\<open>eps\<close> copy as well.
\<^medskip>
- The applet version of the browser is part of the standard
- WWW theory presentation, see the link ``theory dependencies'' within
- each session index.
+ The applet version of the browser is part of the standard WWW theory
+ presentation, see the link ``theory dependencies'' within each session
+ index.
\<close>
subsection \<open>Using the graph browser\<close>
text \<open>
- The browser's main window, which is shown in
- \figref{fig:browserwindow}, consists of two sub-windows. In the
- left sub-window, the directory tree is displayed. The graph itself
- is displayed in the right sub-window.
+ The browser's main window, which is shown in \figref{fig:browserwindow},
+ consists of two sub-windows. In the left sub-window, the directory tree is
+ displayed. The graph itself is displayed in the right sub-window.
\begin{figure}[ht]
\includegraphics[width=\textwidth]{browser_screenshot}
@@ -72,63 +72,57 @@
subsubsection \<open>The directory tree window\<close>
text \<open>
- We describe the usage of the directory browser and the meaning of
- the different items in the browser window.
+ We describe the usage of the directory browser and the meaning of the
+ different items in the browser window.
- \<^item> A red arrow before a directory name indicates that the
- directory is currently ``folded'', i.e.~the nodes in this directory
- are collapsed to one single node. In the right sub-window, the names
- of nodes corresponding to folded directories are enclosed in square
- brackets and displayed in red color.
+ \<^item> A red arrow before a directory name indicates that the directory is
+ currently ``folded'', i.e.~the nodes in this directory are collapsed to one
+ single node. In the right sub-window, the names of nodes corresponding to
+ folded directories are enclosed in square brackets and displayed in red
+ color.
- \<^item> A green downward arrow before a directory name indicates that
- the directory is currently ``unfolded''. It can be folded by
- clicking on the directory name. Clicking on the name for a second
- time unfolds the directory again. Alternatively, a directory can
- also be unfolded by clicking on the corresponding node in the right
- sub-window.
+ \<^item> A green downward arrow before a directory name indicates that the
+ directory is currently ``unfolded''. It can be folded by clicking on the
+ directory name. Clicking on the name for a second time unfolds the directory
+ again. Alternatively, a directory can also be unfolded by clicking on the
+ corresponding node in the right sub-window.
- \<^item> Blue arrows stand before ordinary node names. When clicking on
- such a name (i.e.\ that of a theory), the graph display window
- focuses to the corresponding node. Double clicking invokes a text
- viewer window in which the contents of the theory file are
- displayed.
+ \<^item> Blue arrows stand before ordinary node names. When clicking on such a name
+ (i.e.\ that of a theory), the graph display window focuses to the
+ corresponding node. Double clicking invokes a text viewer window in which
+ the contents of the theory file are displayed.
\<close>
subsubsection \<open>The graph display window\<close>
text \<open>
- When pointing on an ordinary node, an upward and a downward arrow is
- shown. Initially, both of these arrows are green. Clicking on the
- upward or downward arrow collapses all predecessor or successor
- nodes, respectively. The arrow's color then changes to red,
- indicating that the predecessor or successor nodes are currently
- collapsed. The node corresponding to the collapsed nodes has the
- name ``\<^verbatim>\<open>[....]\<close>''. To uncollapse the nodes again, simply
- click on the red arrow or on the node with the name ``\<^verbatim>\<open>[....]\<close>''.
- Similar to the directory browser, the contents of
- theory files can be displayed by double clicking on the
- corresponding node.
+ When pointing on an ordinary node, an upward and a downward arrow is shown.
+ Initially, both of these arrows are green. Clicking on the upward or
+ downward arrow collapses all predecessor or successor nodes, respectively.
+ The arrow's color then changes to red, indicating that the predecessor or
+ successor nodes are currently collapsed. The node corresponding to the
+ collapsed nodes has the name ``\<^verbatim>\<open>[....]\<close>''. To uncollapse the nodes again,
+ simply click on the red arrow or on the node with the name ``\<^verbatim>\<open>[....]\<close>''.
+ Similar to the directory browser, the contents of theory files can be
+ displayed by double clicking on the corresponding node.
\<close>
subsubsection \<open>The ``File'' menu\<close>
text \<open>
- Due to Java Applet security restrictions this menu is only available
- in the full application version. The meaning of the menu items is as
- follows:
+ Due to Java Applet security restrictions this menu is only available in the
+ full application version. The meaning of the menu items is as follows:
\<^descr>[Open \dots] Open a new graph file.
- \<^descr>[Export to PostScript] Outputs the current graph in Postscript
- format, appropriately scaled to fit on one single sheet of A4 paper.
- The resulting file can be printed directly.
+ \<^descr>[Export to PostScript] Outputs the current graph in Postscript format,
+ appropriately scaled to fit on one single sheet of A4 paper. The resulting
+ file can be printed directly.
- \<^descr>[Export to EPS] Outputs the current graph in Encapsulated
- Postscript format. The resulting file can be included in other
- documents.
+ \<^descr>[Export to EPS] Outputs the current graph in Encapsulated Postscript
+ format. The resulting file can be included in other documents.
\<^descr>[Quit] Quit the graph browser.
\<close>
@@ -150,22 +144,20 @@
\<^descr>[\<open>vertex_name\<close>] The name of the vertex.
- \<^descr>[\<open>vertex_ID\<close>] The vertex identifier. Note that there may
- be several vertices with equal names, whereas identifiers must be
- unique.
+ \<^descr>[\<open>vertex_ID\<close>] The vertex identifier. Note that there may be several
+ vertices with equal names, whereas identifiers must be unique.
- \<^descr>[\<open>dir_name\<close>] The name of the ``directory'' the vertex
- should be placed in. A ``\<^verbatim>\<open>+\<close>'' sign after \<open>dir_name\<close> indicates that the nodes in the directory are initially
- visible. Directories are initially invisible by default.
+ \<^descr>[\<open>dir_name\<close>] The name of the ``directory'' the vertex should be placed in.
+ A ``\<^verbatim>\<open>+\<close>'' sign after \<open>dir_name\<close> indicates that the nodes in the directory
+ are initially visible. Directories are initially invisible by default.
- \<^descr>[\<open>path\<close>] The path of the corresponding theory file. This
- is specified relatively to the path of the graph definition file.
+ \<^descr>[\<open>path\<close>] The path of the corresponding theory file. This is specified
+ relatively to the path of the graph definition file.
- \<^descr>[List of successor/predecessor nodes] A ``\<^verbatim>\<open><\<close>''
- sign before the list means that successor nodes are listed, a
- ``\<^verbatim>\<open>>\<close>'' sign means that predecessor nodes are listed. If
- neither ``\<^verbatim>\<open><\<close>'' nor ``\<^verbatim>\<open>>\<close>'' is found, the
- browser assumes that successor nodes are listed.
+ \<^descr>[List of successor/predecessor nodes] A ``\<^verbatim>\<open><\<close>'' sign before the list means
+ that successor nodes are listed, a ``\<^verbatim>\<open>>\<close>'' sign means that predecessor
+ nodes are listed. If neither ``\<^verbatim>\<open><\<close>'' nor ``\<^verbatim>\<open>>\<close>'' is found, the browser
+ assumes that successor nodes are listed.
\<close>
@@ -188,33 +180,28 @@
ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"\<close>}
- Components are initialized as described in \secref{sec:components}
- in a permissive manner, which can mark components as ``missing''.
- This state is amended by letting @{tool "components"} download and
- unpack components that are published on the default component
- repository @{url "http://isabelle.in.tum.de/components/"} in
- particular.
+ Components are initialized as described in \secref{sec:components} in a
+ permissive manner, which can mark components as ``missing''. This state is
+ amended by letting @{tool "components"} download and unpack components that
+ are published on the default component repository @{url
+ "http://isabelle.in.tum.de/components/"} in particular.
- Option \<^verbatim>\<open>-R\<close> specifies an alternative component
- repository. Note that \<^verbatim>\<open>file:///\<close> URLs can be used for
- local directories.
+ Option \<^verbatim>\<open>-R\<close> specifies an alternative component repository. Note that
+ \<^verbatim>\<open>file:///\<close> URLs can be used for local directories.
- Option \<^verbatim>\<open>-a\<close> selects all missing components to be
- resolved. Explicit components may be named as command
- line-arguments as well. Note that components are uniquely
- identified by their base name, while the installation takes place in
- the location that was specified in the attempt to initialize the
- component before.
+ Option \<^verbatim>\<open>-a\<close> selects all missing components to be resolved. Explicit
+ components may be named as command line-arguments as well. Note that
+ components are uniquely identified by their base name, while the
+ installation takes place in the location that was specified in the attempt
+ to initialize the component before.
- Option \<^verbatim>\<open>-l\<close> lists the current state of available and
- missing components with their location (full name) within the
- file-system.
+ Option \<^verbatim>\<open>-l\<close> lists the current state of available and missing components
+ with their location (full name) within the file-system.
- Option \<^verbatim>\<open>-I\<close> initializes the user settings file to
- subscribe to the standard components specified in the Isabelle
- repository clone --- this does not make any sense for regular
- Isabelle releases. If the file already exists, it needs to be
- edited manually according to the printed explanation.
+ Option \<^verbatim>\<open>-I\<close> initializes the user settings file to subscribe to the standard
+ components specified in the Isabelle repository clone --- this does not make
+ any sense for regular Isabelle releases. If the file already exists, it
+ needs to be edited manually according to the printed explanation.
\<close>
@@ -236,14 +223,14 @@
Run Isabelle process with raw ML console and line editor
(default ISABELLE_LINE_EDITOR).\<close>}
- The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default,
- its heap image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
+ The \<^verbatim>\<open>-l\<close> option specifies the logic session name. By default, its heap
+ image is checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
- Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed
- directly to @{tool build} (\secref{sec:tool-build}).
+ Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-o\<close>, \<^verbatim>\<open>-s\<close> are passed directly to @{tool build}
+ (\secref{sec:tool-build}).
- Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the
- underlying Isabelle process (\secref{sec:isabelle-process}).
+ Options \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> are passed directly to the underlying Isabelle process
+ (\secref{sec:isabelle-process}).
The Isabelle process is run through the line editor that is specified via
the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
@@ -259,19 +246,18 @@
section \<open>Displaying documents \label{sec:tool-display}\<close>
-text \<open>The @{tool_def display} tool displays documents in DVI or PDF
- format:
+text \<open>
+ The @{tool_def display} tool displays documents in DVI or PDF format:
@{verbatim [display]
\<open>Usage: isabelle display DOCUMENT
Display DOCUMENT (in DVI or PDF format).\<close>}
\<^medskip>
- The settings @{setting DVI_VIEWER} and @{setting
- PDF_VIEWER} determine the programs for viewing the corresponding
- file formats. Normally this opens the document via the desktop
- environment, potentially in an asynchronous manner with re-use of
- previews views.
+ The settings @{setting DVI_VIEWER} and @{setting PDF_VIEWER} determine the
+ programs for viewing the corresponding file formats. Normally this opens the
+ document via the desktop environment, potentially in an asynchronous manner
+ with re-use of previews views.
\<close>
@@ -284,27 +270,27 @@
View Isabelle documentation.\<close>}
- If called without arguments, it lists all available documents. Each
- line starts with an identifier, followed by a short description. Any
- of these identifiers may be specified as arguments, in order to
- display the corresponding document (see also
- \secref{sec:tool-display}).
+ If called without arguments, it lists all available documents. Each line
+ starts with an identifier, followed by a short description. Any of these
+ identifiers may be specified as arguments, in order to display the
+ corresponding document (see also \secref{sec:tool-display}).
\<^medskip>
- The @{setting ISABELLE_DOCS} setting specifies the list of
- directories (separated by colons) to be scanned for documentations.
+ The @{setting ISABELLE_DOCS} setting specifies the list of directories
+ (separated by colons) to be scanned for documentations.
\<close>
section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close>
-text \<open>The @{tool_def env} tool is a direct wrapper for the standard
- \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within
- the Isabelle settings environment (\secref{sec:settings}).
+text \<open>
+ The @{tool_def env} tool is a direct wrapper for the standard
+ \<^verbatim>\<open>/usr/bin/env\<close> command on POSIX systems, running within the Isabelle
+ settings environment (\secref{sec:settings}).
- The command-line arguments are that of the underlying version of
- \<^verbatim>\<open>env\<close>. For example, the following invokes an instance of
- the GNU Bash shell within the Isabelle environment:
+ The command-line arguments are that of the underlying version of \<^verbatim>\<open>env\<close>. For
+ example, the following invokes an instance of the GNU Bash shell within the
+ Isabelle environment:
@{verbatim [display] \<open>isabelle env bash\<close>}
\<close>
@@ -325,38 +311,39 @@
Get value of VARNAMES from the Isabelle settings.\<close>}
- With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process
- environment that Isabelle related programs are run in. This usually
- contains much more variables than are actually Isabelle settings.
- Normally, output is a list of lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option
- causes only the values to be printed.
+ With the \<^verbatim>\<open>-a\<close> option, one may inspect the full process environment that
+ Isabelle related programs are run in. This usually contains much more
+ variables than are actually Isabelle settings. Normally, output is a list of
+ lines of the form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close>. The \<^verbatim>\<open>-b\<close> option causes only the values
+ to be printed.
- Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment
- to the specified file. Entries are terminated by the ASCII null
- character, i.e.\ the C string terminator.
+ Option \<^verbatim>\<open>-d\<close> produces a dump of the complete environment to the specified
+ file. Entries are terminated by the ASCII null character, i.e.\ the C string
+ terminator.
\<close>
subsubsection \<open>Examples\<close>
-text \<open>Get the location of @{setting ISABELLE_HOME_USER} where
- user-specific information is stored:
+text \<open>
+ Get the location of @{setting ISABELLE_HOME_USER} where user-specific
+ information is stored:
@{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
\<^medskip>
- Get the value only of the same settings variable, which is
- particularly useful in shell scripts:
+ Get the value only of the same settings variable, which is particularly
+ useful in shell scripts:
@{verbatim [display] \<open>isabelle getenv -b ISABELLE_OUTPUT\<close>}
\<close>
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
-text \<open>By default, the main Isabelle binaries (@{executable
- "isabelle"} etc.) are just run from their location within the
- distribution directory, probably indirectly by the shell through its
- @{setting PATH}. Other schemes of installation are supported by the
- @{tool_def install} tool:
+text \<open>
+ By default, the main Isabelle binaries (@{executable "isabelle"} etc.) are
+ just run from their location within the distribution directory, probably
+ indirectly by the shell through its @{setting PATH}. Other schemes of
+ installation are supported by the @{tool_def install} tool:
@{verbatim [display]
\<open>Usage: isabelle install [OPTIONS] BINDIR
@@ -367,24 +354,26 @@
Install Isabelle executables with absolute references to the
distribution directory.\<close>}
- The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle
- distribution directory as determined by @{setting ISABELLE_HOME}.
+ The \<^verbatim>\<open>-d\<close> option overrides the current Isabelle distribution directory as
+ determined by @{setting ISABELLE_HOME}.
- The \<open>BINDIR\<close> argument tells where executable wrapper scripts
- for @{executable "isabelle_process"} and @{executable isabelle}
- should be placed, which is typically a directory in the shell's
- @{setting PATH}, such as \<^verbatim>\<open>$HOME/bin\<close>.
+ The \<open>BINDIR\<close> argument tells where executable wrapper scripts for
+ @{executable "isabelle_process"} and @{executable isabelle} should be
+ placed, which is typically a directory in the shell's @{setting PATH}, such
+ as \<^verbatim>\<open>$HOME/bin\<close>.
\<^medskip>
- It is also possible to make symbolic links of the main
- Isabelle executables manually, but making separate copies outside
- the Isabelle distribution directory will not work!\<close>
+ It is also possible to make symbolic links of the main Isabelle executables
+ manually, but making separate copies outside the Isabelle distribution
+ directory will not work!
+\<close>
section \<open>Creating instances of the Isabelle logo\<close>
-text \<open>The @{tool_def logo} tool creates instances of the generic
- Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
+text \<open>
+ The @{tool_def logo} tool creates instances of the generic Isabelle logo as
+ EPS and PDF, for inclusion in {\LaTeX} documents.
@{verbatim [display]
\<open>Usage: isabelle logo [OPTIONS] XYZ
@@ -394,16 +383,15 @@
-n NAME alternative output base name (default "isabelle_xyx")
-q quiet mode\<close>}
- Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the
- generated files. The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close>
- in lower-case.
+ Option \<^verbatim>\<open>-n\<close> specifies an alternative (base) name for the generated files.
+ The default is \<^verbatim>\<open>isabelle_\<close>\<open>xyz\<close> in lower-case.
Option \<^verbatim>\<open>-q\<close> omits printing of the result file name.
\<^medskip>
- Implementors of Isabelle tools and applications are
- encouraged to make derived Isabelle logos for their own projects
- using this template.\<close>
+ Implementors of Isabelle tools and applications are encouraged to make
+ derived Isabelle logos for their own projects using this template.
+\<close>
section \<open>Output the version identifier of the Isabelle distribution\<close>
@@ -419,53 +407,49 @@
Display Isabelle version information.\<close>}
\<^medskip>
- The default is to output the full version string of the
- Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012: May 2012\<close>.
+ The default is to output the full version string of the Isabelle
+ distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2012: May 2012\<close>.
- The \<^verbatim>\<open>-i\<close> option produces a short identification derived
- from the Mercurial id of the @{setting ISABELLE_HOME} directory.
+ The \<^verbatim>\<open>-i\<close> option produces a short identification derived from the Mercurial
+ id of the @{setting ISABELLE_HOME} directory.
\<close>
section \<open>Convert XML to YXML\<close>
text \<open>
- The @{tool_def yxml} tool converts a standard XML document (stdin)
- to the much simpler and more efficient YXML format of Isabelle
- (stdout). The YXML format is defined as follows.
-
- \<^enum> The encoding is always UTF-8.
+ The @{tool_def yxml} tool converts a standard XML document (stdin) to the
+ much simpler and more efficient YXML format of Isabelle (stdout). The YXML
+ format is defined as follows.
- \<^enum> Body text is represented verbatim (no escaping, no special
- treatment of white space, no named entities, no CDATA chunks, no
- comments).
+ \<^enum> The encoding is always UTF-8.
- \<^enum> Markup elements are represented via ASCII control characters
- \<open>\<^bold>X = 5\<close> and \<open>\<^bold>Y = 6\<close> as follows:
+ \<^enum> Body text is represented verbatim (no escaping, no special treatment of
+ white space, no named entities, no CDATA chunks, no comments).
- \begin{tabular}{ll}
- XML & YXML \\\hline
- \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
- \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
- \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
- \end{tabular}
+ \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
+ and \<open>\<^bold>Y = 6\<close> as follows:
- There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close>
- is treated like \<^verbatim>\<open><foo></foo>\<close>. Also note that
- \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
- well-formed XML documents.
+ \begin{tabular}{ll}
+ XML & YXML \\\hline
+ \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
+ \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
+ \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
+ \end{tabular}
+ There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
+ like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
+ well-formed XML documents.
Parsing YXML is pretty straight-forward: split the text into chunks
- separated by \<open>\<^bold>X\<close>, then split each chunk into
- sub-chunks separated by \<open>\<^bold>Y\<close>. Markup chunks start
- with an empty sub-chunk, and a second empty sub-chunk indicates
- close of an element. Any other non-empty chunk consists of plain
- text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
- @{file "~~/src/Pure/PIDE/yxml.scala"}.
+ separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
+ Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
+ indicates close of an element. Any other non-empty chunk consists of plain
+ text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or @{file
+ "~~/src/Pure/PIDE/yxml.scala"}.
- YXML documents may be detected quickly by checking that the first
- two characters are \<open>\<^bold>X\<^bold>Y\<close>.
+ YXML documents may be detected quickly by checking that the first two
+ characters are \<open>\<^bold>X\<^bold>Y\<close>.
\<close>
end
\ No newline at end of file
--- a/src/Doc/System/Presentation.thy Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Presentation.thy Wed Nov 04 20:18:46 2015 +0100
@@ -1,24 +1,27 @@
+(*:wrap=hard:maxLineLen=78:*)
+
theory Presentation
imports Base
begin
chapter \<open>Presenting theories \label{ch:present}\<close>
-text \<open>Isabelle provides several ways to present the outcome of
- formal developments, including WWW-based browsable libraries or
- actual printable documents. Presentation is centered around the
- concept of \<^emph>\<open>sessions\<close> (\chref{ch:session}). The global session
- structure is that of a tree, with Isabelle Pure at its root, further
- object-logics derived (e.g.\ HOLCF from HOL, and HOL from Pure), and
- application sessions further on in the hierarchy.
+text \<open>
+ Isabelle provides several ways to present the outcome of formal
+ developments, including WWW-based browsable libraries or actual printable
+ documents. Presentation is centered around the concept of \<^emph>\<open>sessions\<close>
+ (\chref{ch:session}). The global session structure is that of a tree, with
+ Isabelle Pure at its root, further object-logics derived (e.g.\ HOLCF from
+ HOL, and HOL from Pure), and application sessions further on in the
+ hierarchy.
- The tools @{tool_ref mkroot} and @{tool_ref build} provide the
- primary means for managing Isabelle sessions, including proper setup
- for presentation; @{tool build} takes care to have @{executable_ref
- "isabelle_process"} run any additional stages required for document
- preparation, notably the @{tool_ref document} and @{tool_ref latex}.
- The complete tool chain for managing batch-mode Isabelle sessions is
- illustrated in \figref{fig:session-tools}.
+ The tools @{tool_ref mkroot} and @{tool_ref build} provide the primary means
+ for managing Isabelle sessions, including proper setup for presentation;
+ @{tool build} takes care to have @{executable_ref "isabelle_process"} run
+ any additional stages required for document preparation, notably the
+ @{tool_ref document} and @{tool_ref latex}. The complete tool chain for
+ managing batch-mode Isabelle sessions is illustrated in
+ \figref{fig:session-tools}.
\begin{figure}[htbp]
\begin{center}
@@ -53,58 +56,55 @@
text \<open>
\index{theory browsing information|bold}
- As a side-effect of building sessions, Isabelle is able to generate
- theory browsing information, including HTML documents that show the
- theory sources and the relationship with its ancestors and
- descendants. Besides the HTML file that is generated for every
- theory, Isabelle stores links to all theories of a session in an
- index file. As a second hierarchy, groups of sessions are organized
- as \<^emph>\<open>chapters\<close>, with a separate index. Note that the implicit
- tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant
+ As a side-effect of building sessions, Isabelle is able to generate theory
+ browsing information, including HTML documents that show the theory sources
+ and the relationship with its ancestors and descendants. Besides the HTML
+ file that is generated for every theory, Isabelle stores links to all
+ theories of a session in an index file. As a second hierarchy, groups of
+ sessions are organized as \<^emph>\<open>chapters\<close>, with a separate index. Note that the
+ implicit tree structure of the session build hierarchy is \<^emph>\<open>not\<close> relevant
for the presentation.
- Isabelle also generates graph files that represent the theory
- dependencies within a session. There is a graph browser Java applet
- embedded in the generated HTML pages, and also a stand-alone
- application that allows browsing theory graphs without having to
- start a WWW client first. The latter version also includes features
- such as generating Postscript files, which are not available in the
- applet version. See \secref{sec:browse} for further information.
+ Isabelle also generates graph files that represent the theory dependencies
+ within a session. There is a graph browser Java applet embedded in the
+ generated HTML pages, and also a stand-alone application that allows
+ browsing theory graphs without having to start a WWW client first. The
+ latter version also includes features such as generating Postscript files,
+ which are not available in the applet version. See \secref{sec:browse} for
+ further information.
\<^medskip>
- The easiest way to let Isabelle generate theory browsing information
- for existing sessions is to invoke @{tool build} with suitable
- options:
+ The easiest way to let Isabelle generate theory browsing information for
+ existing sessions is to invoke @{tool build} with suitable options:
@{verbatim [display] \<open>isabelle build -o browser_info -v -c FOL\<close>}
- The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close>
- as reported by the above verbose invocation of the build process.
+ The presentation output will appear in \<^verbatim>\<open>$ISABELLE_BROWSER_INFO/FOL/FOL\<close> as
+ reported by the above verbose invocation of the build process.
Many Isabelle sessions (such as \<^verbatim>\<open>HOL-Library\<close> in @{file
- "~~/src/HOL/Library"}) also provide actual printable documents.
- These are prepared automatically as well if enabled like this:
+ "~~/src/HOL/Library"}) also provide actual printable documents. These are
+ prepared automatically as well if enabled like this:
@{verbatim [display] \<open>isabelle build -o browser_info -o document=pdf -v -c HOL-Library\<close>}
- Enabling both browser info and document preparation simultaneously
- causes an appropriate ``document'' link to be included in the HTML
- index. Documents may be generated independently of browser
- information as well, see \secref{sec:tool-document} for further
- details.
+ Enabling both browser info and document preparation simultaneously causes an
+ appropriate ``document'' link to be included in the HTML index. Documents
+ may be generated independently of browser information as well, see
+ \secref{sec:tool-document} for further details.
\<^bigskip>
- The theory browsing information is stored in a
- sub-directory directory determined by the @{setting_ref
- ISABELLE_BROWSER_INFO} setting plus a prefix corresponding to the
- session chapter and identifier. In order to present Isabelle
- applications on the web, the corresponding subdirectory from
- @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.\<close>
+ The theory browsing information is stored in a sub-directory directory
+ determined by the @{setting_ref ISABELLE_BROWSER_INFO} setting plus a prefix
+ corresponding to the session chapter and identifier. In order to present
+ Isabelle applications on the web, the corresponding subdirectory from
+ @{setting ISABELLE_BROWSER_INFO} can be put on a WWW server.
+\<close>
section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
-text \<open>The @{tool_def mkroot} tool configures a given directory as
- session root, with some \<^verbatim>\<open>ROOT\<close> file and optional document
- source directory. Its usage is:
+text \<open>
+ The @{tool_def mkroot} tool configures a given directory as session root,
+ with some \<^verbatim>\<open>ROOT\<close> file and optional document source directory. Its usage is:
@{verbatim [display]
\<open>Usage: isabelle mkroot [OPTIONS] [DIR]
@@ -114,46 +114,45 @@
Prepare session root DIR (default: current directory).\<close>}
- The results are placed in the given directory \<open>dir\<close>, which
- refers to the current directory by default. The @{tool mkroot} tool
- is conservative in the sense that it does not overwrite existing
- files or directories. Earlier attempts to generate a session root
- need to be deleted manually.
+ The results are placed in the given directory \<open>dir\<close>, which refers to the
+ current directory by default. The @{tool mkroot} tool is conservative in the
+ sense that it does not overwrite existing files or directories. Earlier
+ attempts to generate a session root need to be deleted manually.
\<^medskip>
- Option \<^verbatim>\<open>-d\<close> indicates that the session shall be
- accompanied by a formal document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close>
- as its {\LaTeX} entry point (see also \chref{ch:present}).
+ Option \<^verbatim>\<open>-d\<close> indicates that the session shall be accompanied by a formal
+ document, with \<open>DIR\<close>\<^verbatim>\<open>/document/root.tex\<close> as its {\LaTeX} entry point (see
+ also \chref{ch:present}).
- Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session
- name; otherwise the base name of the given directory is used.
+ Option \<^verbatim>\<open>-n\<close> allows to specify an alternative session name; otherwise the
+ base name of the given directory is used.
\<^medskip>
- The implicit Isabelle settings variable @{setting
- ISABELLE_LOGIC} specifies the parent session, and @{setting
- ISABELLE_DOCUMENT_FORMAT} the document format to be filled filled
- into the generated \<^verbatim>\<open>ROOT\<close> file.
+ The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
+ the parent session, and @{setting ISABELLE_DOCUMENT_FORMAT} the document
+ format to be filled filled into the generated \<^verbatim>\<open>ROOT\<close> file.
\<close>
subsubsection \<open>Examples\<close>
-text \<open>Produce session \<^verbatim>\<open>Test\<close> (with document preparation)
- within a separate directory of the same name:
+text \<open>
+ Produce session \<^verbatim>\<open>Test\<close> (with document preparation) within a separate
+ directory of the same name:
@{verbatim [display] \<open>isabelle mkroot -d Test && isabelle build -D Test\<close>}
\<^medskip>
- Upgrade the current directory into a session ROOT with
- document preparation, and build it:
+ Upgrade the current directory into a session ROOT with document preparation,
+ and build it:
@{verbatim [display] \<open>isabelle mkroot -d && isabelle build -D .\<close>}
\<close>
section \<open>Preparing Isabelle session documents \label{sec:tool-document}\<close>
-text \<open>The @{tool_def document} tool prepares logic session
- documents, processing the sources as provided by the user and
- generated by Isabelle. Its usage is:
+text \<open>
+ The @{tool_def document} tool prepares logic session documents, processing
+ the sources as provided by the user and generated by Isabelle. Its usage is:
@{verbatim [display]
\<open>Usage: isabelle document [OPTIONS] [DIR]
@@ -168,90 +167,83 @@
This tool is usually run automatically as part of the Isabelle build
process, provided document preparation has been enabled via suitable
- options. It may be manually invoked on the generated browser
- information document output as well, e.g.\ in case of errors
- encountered in the batch run.
+ options. It may be manually invoked on the generated browser information
+ document output as well, e.g.\ in case of errors encountered in the batch
+ run.
\<^medskip>
- The \<^verbatim>\<open>-c\<close> option tells @{tool document} to
- dispose the document sources after successful operation! This is
- the right thing to do for sources generated by an Isabelle process,
- but take care of your files in manual document preparation!
+ The \<^verbatim>\<open>-c\<close> option tells @{tool document} to dispose the document sources
+ after successful operation! This is the right thing to do for sources
+ generated by an Isabelle process, but take care of your files in manual
+ document preparation!
\<^medskip>
- The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify
- the final output file name and format, the default is ``\<^verbatim>\<open>document.dvi\<close>''.
- Note that the result will appear in the parent of the target \<^verbatim>\<open>DIR\<close>.
+ The \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-o\<close> option specify the final output file name and format,
+ the default is ``\<^verbatim>\<open>document.dvi\<close>''. Note that the result will appear in the
+ parent of the target \<^verbatim>\<open>DIR\<close>.
\<^medskip>
- The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret
- tagged Isabelle command regions. Tags are specified as a comma
- separated list of modifier/name pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'')
- means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to
- fold text tagged as \<open>foo\<close>. The builtin default is equivalent
- to the tag specification ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>'';
- see also the {\LaTeX} macros \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and
- \<^verbatim>\<open>\isafoldtag\<close>, in @{file "~~/lib/texinputs/isabelle.sty"}.
+ The \<^verbatim>\<open>-t\<close> option tells {\LaTeX} how to interpret tagged Isabelle command
+ regions. Tags are specified as a comma separated list of modifier/name
+ pairs: ``\<^verbatim>\<open>+\<close>\<open>foo\<close>'' (or just ``\<open>foo\<close>'') means to keep, ``\<^verbatim>\<open>-\<close>\<open>foo\<close>'' to
+ drop, and ``\<^verbatim>\<open>/\<close>\<open>foo\<close>'' to fold text tagged as \<open>foo\<close>. The builtin default is
+ equivalent to the tag specification
+ ``\<^verbatim>\<open>+theory,+proof,+ML,+visible,-invisible\<close>''; see also the {\LaTeX} macros
+ \<^verbatim>\<open>\isakeeptag\<close>, \<^verbatim>\<open>\isadroptag\<close>, and \<^verbatim>\<open>\isafoldtag\<close>, in @{file
+ "~~/lib/texinputs/isabelle.sty"}.
\<^medskip>
- Document preparation requires a \<^verbatim>\<open>document\<close>
- directory within the session sources. This directory is supposed to
- contain all the files needed to produce the final document --- apart
- from the actual theories which are generated by Isabelle.
+ Document preparation requires a \<^verbatim>\<open>document\<close> directory within the session
+ sources. This directory is supposed to contain all the files needed to
+ produce the final document --- apart from the actual theories which are
+ generated by Isabelle.
\<^medskip>
- For most practical purposes, @{tool document} is smart
- enough to create any of the specified output formats, taking
- \<^verbatim>\<open>root.tex\<close> supplied by the user as a starting point. This
- even includes multiple runs of {\LaTeX} to accommodate references
- and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close> within
- the same directory).
+ For most practical purposes, @{tool document} is smart enough to create any
+ of the specified output formats, taking \<^verbatim>\<open>root.tex\<close> supplied by the user as
+ a starting point. This even includes multiple runs of {\LaTeX} to
+ accommodate references and bibliographies (the latter assumes \<^verbatim>\<open>root.bib\<close>
+ within the same directory).
- In more complex situations, a separate \<^verbatim>\<open>build\<close> script for
- the document sources may be given. It is invoked with command-line
- arguments for the document format and the document variant name.
- The script needs to produce corresponding output files, e.g.\
- \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and default
- variants). The main work can be again delegated to @{tool latex},
- but it is also possible to harvest generated {\LaTeX} sources and
- copy them elsewhere.
+ In more complex situations, a separate \<^verbatim>\<open>build\<close> script for the document
+ sources may be given. It is invoked with command-line arguments for the
+ document format and the document variant name. The script needs to produce
+ corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for target format \<^verbatim>\<open>pdf\<close> (and
+ default variants). The main work can be again delegated to @{tool latex},
+ but it is also possible to harvest generated {\LaTeX} sources and copy them
+ elsewhere.
\<^medskip>
- When running the session, Isabelle copies the content of
- the original \<^verbatim>\<open>document\<close> directory into its proper place
- within @{setting ISABELLE_BROWSER_INFO}, according to the session
- path and document variant. Then, for any processed theory \<open>A\<close>
- some {\LaTeX} source is generated and put there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>.
- Furthermore, a list of all generated theory
- files is put into \<^verbatim>\<open>session.tex\<close>. Typically, the root
- {\LaTeX} file provided by the user would include \<^verbatim>\<open>session.tex\<close>
- to get a document containing all the theories.
+ When running the session, Isabelle copies the content of the original
+ \<^verbatim>\<open>document\<close> directory into its proper place within @{setting
+ ISABELLE_BROWSER_INFO}, according to the session path and document variant.
+ Then, for any processed theory \<open>A\<close> some {\LaTeX} source is generated and put
+ there as \<open>A\<close>\<^verbatim>\<open>.tex\<close>. Furthermore, a list of all generated theory files is
+ put into \<^verbatim>\<open>session.tex\<close>. Typically, the root {\LaTeX} file provided by the
+ user would include \<^verbatim>\<open>session.tex\<close> to get a document containing all the
+ theories.
- The {\LaTeX} versions of the theories require some macros defined in
- @{file "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close>
- in \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already
- includes an appropriate path specification for {\TeX} inputs.
+ The {\LaTeX} versions of the theories require some macros defined in @{file
+ "~~/lib/texinputs/isabelle.sty"}. Doing \<^verbatim>\<open>\usepackage{isabelle}\<close> in
+ \<^verbatim>\<open>root.tex\<close> should be fine; the underlying @{tool latex} already includes an
+ appropriate path specification for {\TeX} inputs.
- If the text contains any references to Isabelle symbols (such as
- \<^verbatim>\<open>\<forall>\<close>) then \<^verbatim>\<open>isabellesym.sty\<close> should be included as well.
- This package contains a standard set of {\LaTeX} macro definitions
- \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>,
- see @{cite "isabelle-implementation"} for a
- complete list of predefined Isabelle symbols. Users may invent
- further symbols as well, just by providing {\LaTeX} macros in a
- similar fashion as in @{file "~~/lib/texinputs/isabellesym.sty"} of
- the Isabelle distribution.
+ If the text contains any references to Isabelle symbols (such as \<^verbatim>\<open>\<forall>\<close>) then
+ \<^verbatim>\<open>isabellesym.sty\<close> should be included as well. This package contains a
+ standard set of {\LaTeX} macro definitions \<^verbatim>\<open>\isasym\<close>\<open>foo\<close> corresponding to
+ \<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>foo\<close>\<^verbatim>\<open>>\<close>, see @{cite "isabelle-implementation"} for a complete list
+ of predefined Isabelle symbols. Users may invent further symbols as well,
+ just by providing {\LaTeX} macros in a similar fashion as in @{file
+ "~~/lib/texinputs/isabellesym.sty"} of the Isabelle distribution.
- For proper setup of DVI and PDF documents (with hyperlinks and
- bookmarks), we recommend to include @{file
- "~~/lib/texinputs/pdfsetup.sty"} as well.
+ For proper setup of DVI and PDF documents (with hyperlinks and bookmarks),
+ we recommend to include @{file "~~/lib/texinputs/pdfsetup.sty"} as well.
\<^medskip>
- As a final step of Isabelle document preparation, @{tool
- document}~\<^verbatim>\<open>-c\<close> is run on the resulting copy of the
- \<^verbatim>\<open>document\<close> directory. Thus the actual output document is
- built and installed in its proper place. The generated sources are
- deleted after successful run of {\LaTeX} and friends.
+ As a final step of Isabelle document preparation, @{tool document}~\<^verbatim>\<open>-c\<close> is
+ run on the resulting copy of the \<^verbatim>\<open>document\<close> directory. Thus the actual
+ output document is built and installed in its proper place. The generated
+ sources are deleted after successful run of {\LaTeX} and friends.
Some care is needed if the document output location is configured
differently, say within a directory whose content is still required
@@ -262,8 +254,9 @@
section \<open>Running {\LaTeX} within the Isabelle environment
\label{sec:tool-latex}\<close>
-text \<open>The @{tool_def latex} tool provides the basic interface for
- Isabelle document preparation. Its usage is:
+text \<open>
+ The @{tool_def latex} tool provides the basic interface for Isabelle
+ document preparation. Its usage is:
@{verbatim [display]
\<open>Usage: isabelle latex [OPTIONS] [FILE]
@@ -274,32 +267,30 @@
Run LaTeX (and related tools) on FILE (default root.tex),
producing the specified output format.\<close>}
- Appropriate {\LaTeX}-related programs are run on the input file,
- according to the given output format: @{executable latex},
- @{executable pdflatex}, @{executable dvips}, @{executable bibtex}
- (for \<^verbatim>\<open>bbl\<close>), and @{executable makeindex} (for \<^verbatim>\<open>idx\<close>).
- The actual commands are determined from the settings
- environment (@{setting ISABELLE_PDFLATEX} etc.).
+ Appropriate {\LaTeX}-related programs are run on the input file, according
+ to the given output format: @{executable latex}, @{executable pdflatex},
+ @{executable dvips}, @{executable bibtex} (for \<^verbatim>\<open>bbl\<close>), and @{executable
+ makeindex} (for \<^verbatim>\<open>idx\<close>). The actual commands are determined from the
+ settings environment (@{setting ISABELLE_PDFLATEX} etc.).
- The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to
- be updated from the distribution. This is useful in special
- situations where the document sources are to be processed another
- time by separate tools.
+ The \<^verbatim>\<open>sty\<close> output format causes the Isabelle style files to be updated from
+ the distribution. This is useful in special situations where the document
+ sources are to be processed another time by separate tools.
- The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists
- of symbols that are available without loading additional {\LaTeX}
- packages.
+ The \<^verbatim>\<open>syms\<close> output is for internal use; it generates lists of symbols that
+ are available without loading additional {\LaTeX} packages.
\<close>
subsubsection \<open>Examples\<close>
-text \<open>Invoking @{tool latex} by hand may be occasionally useful when
- debugging failed attempts of the automatic document preparation
- stage of batch-mode Isabelle. The abortive process leaves the
- sources at a certain place within @{setting ISABELLE_BROWSER_INFO},
- see the runtime error message for details. This enables users to
- inspect {\LaTeX} runs in further detail, e.g.\ like this:
+text \<open>
+ Invoking @{tool latex} by hand may be occasionally useful when debugging
+ failed attempts of the automatic document preparation stage of batch-mode
+ Isabelle. The abortive process leaves the sources at a certain place within
+ @{setting ISABELLE_BROWSER_INFO}, see the runtime error message for details.
+ This enables users to inspect {\LaTeX} runs in further detail, e.g.\ like
+ this:
@{verbatim [display]
\<open>cd "$(isabelle getenv -b ISABELLE_BROWSER_INFO)/Unsorted/Test/document"
--- a/src/Doc/System/Scala.thy Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Scala.thy Wed Nov 04 20:18:46 2015 +0100
@@ -1,43 +1,47 @@
+(*:wrap=hard:maxLineLen=78:*)
+
theory Scala
imports Base
begin
chapter \<open>Isabelle/Scala development tools\<close>
-text \<open>Isabelle/ML and Isabelle/Scala are the two main language
-environments for Isabelle tool implementations. There are some basic
-command-line tools to work with the underlying Java Virtual Machine,
-the Scala toplevel and compiler. Note that Isabelle/jEdit
-@{cite "isabelle-jedit"} provides a Scala Console for interactive
-experimentation within the running application.\<close>
+text \<open>
+ Isabelle/ML and Isabelle/Scala are the two main language environments for
+ Isabelle tool implementations. There are some basic command-line tools to
+ work with the underlying Java Virtual Machine, the Scala toplevel and
+ compiler. Note that Isabelle/jEdit @{cite "isabelle-jedit"} provides a Scala
+ Console for interactive experimentation within the running application.
+\<close>
section \<open>Java Runtime Environment within Isabelle \label{sec:tool-java}\<close>
-text \<open>The @{tool_def java} tool is a direct wrapper for the Java
- Runtime Environment, within the regular Isabelle settings
- environment (\secref{sec:settings}). The command line arguments are
- that of the underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode
- if possible, to improve performance (at the cost of extra startup time).
+text \<open>
+ The @{tool_def java} tool is a direct wrapper for the Java Runtime
+ Environment, within the regular Isabelle settings environment
+ (\secref{sec:settings}). The command line arguments are that of the
+ underlying Java version. It is run in \<^verbatim>\<open>-server\<close> mode if possible, to
+ improve performance (at the cost of extra startup time).
- The \<^verbatim>\<open>java\<close> executable is the one within @{setting
- ISABELLE_JDK_HOME}, according to the standard directory layout for
- official JDK distributions. The class loader is augmented such that
- the name space of \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available,
- which is the main Isabelle/Scala module.
+ The \<^verbatim>\<open>java\<close> executable is the one within @{setting ISABELLE_JDK_HOME},
+ according to the standard directory layout for official JDK distributions.
+ The class loader is augmented such that the name space of
+ \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available, which is the main Isabelle/Scala module.
- For example, the following command-line invokes the main method of
- class \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with
- some diagnostic information about the Isabelle environment:
+ For example, the following command-line invokes the main method of class
+ \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with some diagnostic
+ information about the Isabelle environment:
@{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
\<close>
section \<open>Scala toplevel \label{sec:tool-scala}\<close>
-text \<open>The @{tool_def scala} tool is a direct wrapper for the Scala
- toplevel; see also @{tool java} above. The command line arguments
- are that of the underlying Scala version.
+text \<open>
+ The @{tool_def scala} tool is a direct wrapper for the Scala toplevel; see
+ also @{tool java} above. The command line arguments are that of the
+ underlying Scala version.
This allows to interact with Isabelle/Scala in TTY mode like this:
@{verbatim [display]
@@ -51,32 +55,33 @@
section \<open>Scala compiler \label{sec:tool-scalac}\<close>
-text \<open>The @{tool_def scalac} tool is a direct wrapper for the Scala
- compiler; see also @{tool scala} above. The command line arguments
- are that of the underlying Scala version.
+text \<open>
+ The @{tool_def scalac} tool is a direct wrapper for the Scala compiler; see
+ also @{tool scala} above. The command line arguments are that of the
+ underlying Scala version.
This allows to compile further Scala modules, depending on existing
- Isabelle/Scala functionality. The resulting class or jar files can
- be added to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash
- function that is provided by the Isabelle process environment. Thus
- add-on components can register themselves in a modular manner, see
- also \secref{sec:components}.
+ Isabelle/Scala functionality. The resulting class or jar files can be added
+ to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash function that is provided
+ by the Isabelle process environment. Thus add-on components can register
+ themselves in a modular manner, see also \secref{sec:components}.
- Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for
- adding plugin components, which needs special attention since
- it overrides the standard Java class loader.\<close>
+ Note that jEdit @{cite "isabelle-jedit"} has its own mechanisms for adding
+ plugin components, which needs special attention since it overrides the
+ standard Java class loader.
+\<close>
section \<open>Scala script wrapper\<close>
-text \<open>The executable @{executable
- "$ISABELLE_HOME/bin/isabelle_scala_script"} allows to run
- Isabelle/Scala source files stand-alone programs, by using a
+text \<open>
+ The executable @{executable "$ISABELLE_HOME/bin/isabelle_scala_script"}
+ allows to run Isabelle/Scala source files stand-alone programs, by using a
suitable ``hash-bang'' line and executable file permissions.
- The subsequent example assumes that the main Isabelle binaries have
- been installed in some directory that is included in @{setting PATH}
- (see also @{tool "install"}):
+ The subsequent example assumes that the main Isabelle binaries have been
+ installed in some directory that is included in @{setting PATH} (see also
+ @{tool "install"}):
@{verbatim [display]
\<open>#!/usr/bin/env isabelle_scala_script
@@ -84,8 +89,8 @@
Console.println("browser_info = " + options.bool("browser_info"))
Console.println("document = " + options.string("document"))\<close>}
- Alternatively the full @{file
- "$ISABELLE_HOME/bin/isabelle_scala_script"} may be specified in
- expanded form.\<close>
+ Alternatively the full @{file "$ISABELLE_HOME/bin/isabelle_scala_script"}
+ may be specified in expanded form.
+\<close>
end
--- a/src/Doc/System/Sessions.thy Wed Nov 04 19:52:38 2015 +0100
+++ b/src/Doc/System/Sessions.thy Wed Nov 04 20:18:46 2015 +0100
@@ -1,52 +1,52 @@
+(*:wrap=hard:maxLineLen=78:*)
+
theory Sessions
imports Base
begin
chapter \<open>Isabelle sessions and build management \label{ch:session}\<close>
-text \<open>An Isabelle \<^emph>\<open>session\<close> consists of a collection of related
- theories that may be associated with formal documents
- (\chref{ch:present}). There is also a notion of \<^emph>\<open>persistent
- heap\<close> image to capture the state of a session, similar to
- object-code in compiled programming languages. Thus the concept of
- session resembles that of a ``project'' in common IDE environments,
- but the specific name emphasizes the connection to interactive
- theorem proving: the session wraps-up the results of
- user-interaction with the prover in a persistent form.
+text \<open>
+ An Isabelle \<^emph>\<open>session\<close> consists of a collection of related theories that may
+ be associated with formal documents (\chref{ch:present}). There is also a
+ notion of \<^emph>\<open>persistent heap\<close> image to capture the state of a session,
+ similar to object-code in compiled programming languages. Thus the concept
+ of session resembles that of a ``project'' in common IDE environments, but
+ the specific name emphasizes the connection to interactive theorem proving:
+ the session wraps-up the results of user-interaction with the prover in a
+ persistent form.
- Application sessions are built on a given parent session, which may
- be built recursively on other parents. Following this path in the
- hierarchy eventually leads to some major object-logic session like
- \<open>HOL\<close>, which itself is based on \<open>Pure\<close> as the common
- root of all sessions.
+ Application sessions are built on a given parent session, which may be built
+ recursively on other parents. Following this path in the hierarchy
+ eventually leads to some major object-logic session like \<open>HOL\<close>, which itself
+ is based on \<open>Pure\<close> as the common root of all sessions.
- Processing sessions may take considerable time. Isabelle build
- management helps to organize this efficiently. This includes
- support for parallel build jobs, in addition to the multithreaded
- theory and proof checking that is already provided by the prover
- process itself.\<close>
+ Processing sessions may take considerable time. Isabelle build management
+ helps to organize this efficiently. This includes support for parallel build
+ jobs, in addition to the multithreaded theory and proof checking that is
+ already provided by the prover process itself.
+\<close>
section \<open>Session ROOT specifications \label{sec:session-root}\<close>
-text \<open>Session specifications reside in files called \<^verbatim>\<open>ROOT\<close>
- within certain directories, such as the home locations of registered
- Isabelle components or additional project directories given by the
- user.
+text \<open>
+ Session specifications reside in files called \<^verbatim>\<open>ROOT\<close> within certain
+ directories, such as the home locations of registered Isabelle components or
+ additional project directories given by the user.
- The ROOT file format follows the lexical conventions of the
- \<^emph>\<open>outer syntax\<close> of Isabelle/Isar, see also
- @{cite "isabelle-isar-ref"}. This defines common forms like
- identifiers, names, quoted strings, verbatim text, nested comments
- etc. The grammar for @{syntax session_chapter} and @{syntax
- session_entry} is given as syntax diagram below; each ROOT file may
- contain multiple specifications like this. Chapters help to
- organize browser info (\secref{sec:info}), but have no formal
- meaning. The default chapter is ``\<open>Unsorted\<close>''.
+ The ROOT file format follows the lexical conventions of the \<^emph>\<open>outer syntax\<close>
+ of Isabelle/Isar, see also @{cite "isabelle-isar-ref"}. This defines common
+ forms like identifiers, names, quoted strings, verbatim text, nested
+ comments etc. The grammar for @{syntax session_chapter} and @{syntax
+ session_entry} is given as syntax diagram below; each ROOT file may contain
+ multiple specifications like this. Chapters help to organize browser info
+ (\secref{sec:info}), but have no formal meaning. The default chapter is
+ ``\<open>Unsorted\<close>''.
- Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing
- mode \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is
- enabled by default for any file of that name.
+ Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple editing mode
+ \<^verbatim>\<open>isabelle-root\<close> for session ROOT files, which is enabled by default for any
+ file of that name.
@{rail \<open>
@{syntax_def session_chapter}: @'chapter' @{syntax name}
@@ -77,151 +77,138 @@
document_files: @'document_files' ('(' dir ')')? (@{syntax name}+)
\<close>}
- \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new
- session \<open>A\<close> based on parent session \<open>B\<close>, with its
- content given in \<open>body\<close> (theories and auxiliary source files).
- Note that a parent (like \<open>HOL\<close>) is mandatory in practical
+ \<^descr> \isakeyword{session}~\<open>A = B + body\<close> defines a new session \<open>A\<close> based on
+ parent session \<open>B\<close>, with its content given in \<open>body\<close> (theories and auxiliary
+ source files). Note that a parent (like \<open>HOL\<close>) is mandatory in practical
applications: only Isabelle/Pure can bootstrap itself from nothing.
- All such session specifications together describe a hierarchy (tree)
- of sessions, with globally unique names. The new session name
- \<open>A\<close> should be sufficiently long and descriptive to stand on
- its own in a potentially large library.
+ All such session specifications together describe a hierarchy (tree) of
+ sessions, with globally unique names. The new session name \<open>A\<close> should be
+ sufficiently long and descriptive to stand on its own in a potentially large
+ library.
- \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a
- collection of groups where the new session is a member. Group names
- are uninterpreted and merely follow certain conventions. For
- example, the Isabelle distribution tags some important sessions by
- the group name called ``\<open>main\<close>''. Other projects may invent
- their own conventions, but this requires some care to avoid clashes
+ \<^descr> \isakeyword{session}~\<open>A (groups)\<close> indicates a collection of groups where
+ the new session is a member. Group names are uninterpreted and merely follow
+ certain conventions. For example, the Isabelle distribution tags some
+ important sessions by the group name called ``\<open>main\<close>''. Other projects may
+ invent their own conventions, but this requires some care to avoid clashes
within this unchecked name space.
- \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close>
- specifies an explicit directory for this session; by default this is
- the current directory of the \<^verbatim>\<open>ROOT\<close> file.
+ \<^descr> \isakeyword{session}~\<open>A\<close>~\isakeyword{in}~\<open>dir\<close> specifies an explicit
+ directory for this session; by default this is the current directory of the
+ \<^verbatim>\<open>ROOT\<close> file.
- All theories and auxiliary source files are located relatively to
- the session directory. The prover process is run within the same as
- its current working directory.
-
- \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form
- annotation for this session.
+ All theories and auxiliary source files are located relatively to the
+ session directory. The prover process is run within the same as its current
+ working directory.
- \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines
- separate options (\secref{sec:system-options}) that are used when
- processing this session, but \<^emph>\<open>without\<close> propagation to child
- sessions. Note that \<open>z\<close> abbreviates \<open>z = true\<close> for
- Boolean options.
+ \<^descr> \isakeyword{description}~\<open>text\<close> is a free-form annotation for this
+ session.
- \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a
- block of theories that are processed within an environment that is
- augmented by the given options, in addition to the global session
- options given before. Any number of blocks of \isakeyword{theories}
- may be given. Options are only active for each
+ \<^descr> \isakeyword{options}~\<open>[x = a, y = b, z]\<close> defines separate options
+ (\secref{sec:system-options}) that are used when processing this session,
+ but \<^emph>\<open>without\<close> propagation to child sessions. Note that \<open>z\<close> abbreviates \<open>z =
+ true\<close> for Boolean options.
+
+ \<^descr> \isakeyword{theories}~\<open>options names\<close> specifies a block of theories that
+ are processed within an environment that is augmented by the given options,
+ in addition to the global session options given before. Any number of blocks
+ of \isakeyword{theories} may be given. Options are only active for each
\isakeyword{theories} block separately.
- \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source
- files that are involved in the processing of this session. This
- should cover anything outside the formal content of the theory
- sources. In contrast, files that are loaded formally
- within a theory, e.g.\ via @{command "ML_file"}, need not be
+ \<^descr> \isakeyword{files}~\<open>files\<close> lists additional source files that are involved
+ in the processing of this session. This should cover anything outside the
+ formal content of the theory sources. In contrast, files that are loaded
+ formally within a theory, e.g.\ via @{command "ML_file"}, need not be
declared again.
- \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists source files for document preparation,
- typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for {\LaTeX}.
- Only these explicitly given files are copied from the base directory
- to the document output directory, before formal document processing
- is started (see also \secref{sec:tool-document}). The local path
- structure of the \<open>files\<close> is preserved, which allows to
- reconstruct the original directory hierarchy of \<open>base_dir\<close>.
+ \<^descr> \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>base_dir) files\<close> lists
+ source files for document preparation, typically \<^verbatim>\<open>.tex\<close> and \<^verbatim>\<open>.sty\<close> for
+ {\LaTeX}. Only these explicitly given files are copied from the base
+ directory to the document output directory, before formal document
+ processing is started (see also \secref{sec:tool-document}). The local path
+ structure of the \<open>files\<close> is preserved, which allows to reconstruct the
+ original directory hierarchy of \<open>base_dir\<close>.
\<^descr> \isakeyword{document_files}~\<open>files\<close> abbreviates
- \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\ document sources are taken from the base
- directory \<^verbatim>\<open>document\<close> within the session root directory.
+ \isakeyword{document_files}~\<open>(\<close>\isakeyword{in}~\<open>document) files\<close>, i.e.\
+ document sources are taken from the base directory \<^verbatim>\<open>document\<close> within the
+ session root directory.
\<close>
subsubsection \<open>Examples\<close>
-text \<open>See @{file "~~/src/HOL/ROOT"} for a diversity of practically
- relevant situations, although it uses relatively complex
- quasi-hierarchic naming conventions like \<^verbatim>\<open>HOL-SPARK\<close>,
- \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to use
- unqualified names that are relatively long and descriptive, as in
- the Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
- example.\<close>
+text \<open>
+ See @{file "~~/src/HOL/ROOT"} for a diversity of practically relevant
+ situations, although it uses relatively complex quasi-hierarchic naming
+ conventions like \<^verbatim>\<open>HOL-SPARK\<close>, \<^verbatim>\<open>HOL-SPARK-Examples\<close>. An alternative is to
+ use unqualified names that are relatively long and descriptive, as in the
+ Archive of Formal Proofs (@{url "http://afp.sourceforge.net"}), for
+ example.
+\<close>
section \<open>System build options \label{sec:system-options}\<close>
-text \<open>See @{file "~~/etc/options"} for the main defaults provided by
- the Isabelle distribution. Isabelle/jEdit @{cite "isabelle-jedit"}
- includes a simple editing mode \<^verbatim>\<open>isabelle-options\<close> for
- this file-format.
+text \<open>
+ See @{file "~~/etc/options"} for the main defaults provided by the Isabelle
+ distribution. Isabelle/jEdit @{cite "isabelle-jedit"} includes a simple
+ editing mode \<^verbatim>\<open>isabelle-options\<close> for this file-format.
- The following options are particularly relevant to build Isabelle
- sessions, in particular with document preparation
- (\chref{ch:present}).
+ The following options are particularly relevant to build Isabelle sessions,
+ in particular with document preparation (\chref{ch:present}).
- \<^item> @{system_option_def "browser_info"} controls output of HTML
- browser info, see also \secref{sec:info}.
+ \<^item> @{system_option_def "browser_info"} controls output of HTML browser
+ info, see also \secref{sec:info}.
- \<^item> @{system_option_def "document"} specifies the document output
- format, see @{tool document} option \<^verbatim>\<open>-o\<close> in
- \secref{sec:tool-document}. In practice, the most relevant values
- are \<^verbatim>\<open>document=false\<close> or \<^verbatim>\<open>document=pdf\<close>.
+ \<^item> @{system_option_def "document"} specifies the document output format,
+ see @{tool document} option \<^verbatim>\<open>-o\<close> in \secref{sec:tool-document}. In
+ practice, the most relevant values are \<^verbatim>\<open>document=false\<close> or
+ \<^verbatim>\<open>document=pdf\<close>.
- \<^item> @{system_option_def "document_output"} specifies an
- alternative directory for generated output of the document
- preparation system; the default is within the @{setting
- "ISABELLE_BROWSER_INFO"} hierarchy as explained in
- \secref{sec:info}. See also @{tool mkroot}, which generates a
- default configuration with output readily available to the author of
- the document.
+ \<^item> @{system_option_def "document_output"} specifies an alternative
+ directory for generated output of the document preparation system; the
+ default is within the @{setting "ISABELLE_BROWSER_INFO"} hierarchy as
+ explained in \secref{sec:info}. See also @{tool mkroot}, which generates a
+ default configuration with output readily available to the author of the
+ document.
- \<^item> @{system_option_def "document_variants"} specifies document
- variants as a colon-separated list of \<open>name=tags\<close> entries,
- corresponding to @{tool document} options \<^verbatim>\<open>-n\<close> and
- \<^verbatim>\<open>-t\<close>.
+ \<^item> @{system_option_def "document_variants"} specifies document variants as
+ a colon-separated list of \<open>name=tags\<close> entries, corresponding to @{tool
+ document} options \<^verbatim>\<open>-n\<close> and \<^verbatim>\<open>-t\<close>.
- For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
- two documents: the one called \<^verbatim>\<open>document\<close> with default tags,
- and the other called \<^verbatim>\<open>outline\<close> where proofs and ML
- sections are folded.
+ For example, \<^verbatim>\<open>document_variants=document:outline=/proof,/ML\<close> indicates
+ two documents: the one called \<^verbatim>\<open>document\<close> with default tags, and the other
+ called \<^verbatim>\<open>outline\<close> where proofs and ML sections are folded.
- Document variant names are just a matter of conventions. It is also
- possible to use different document variant names (without tags) for
- different document root entries, see also
- \secref{sec:tool-document}.
+ Document variant names are just a matter of conventions. It is also
+ possible to use different document variant names (without tags) for
+ different document root entries, see also \secref{sec:tool-document}.
- \<^item> @{system_option_def "threads"} determines the number of worker
- threads for parallel checking of theories and proofs. The default
- \<open>0\<close> means that a sensible maximum value is determined by the
- underlying hardware. For machines with many cores or with
- hyperthreading, this is often requires manual adjustment (on the
- command-line or within personal settings or preferences, not within
- a session \<^verbatim>\<open>ROOT\<close>).
+ \<^item> @{system_option_def "threads"} determines the number of worker threads
+ for parallel checking of theories and proofs. The default \<open>0\<close> means that a
+ sensible maximum value is determined by the underlying hardware. For
+ machines with many cores or with hyperthreading, this is often requires
+ manual adjustment (on the command-line or within personal settings or
+ preferences, not within a session \<^verbatim>\<open>ROOT\<close>).
- \<^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 ``true'' if the corresponding environment
- value is defined and non-empty.
+ \<^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
+ ``true'' if the corresponding environment value is defined and non-empty.
- For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be
- used to guard extraordinary theories, which are meant to be enabled
- explicitly via some shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close>
- before invoking @{tool build}.
+ For example, the \<^verbatim>\<open>condition=ISABELLE_FULL_TEST\<close> may be used to guard
+ extraordinary theories, which are meant to be enabled explicitly via some
+ shell prefix \<^verbatim>\<open>env ISABELLE_FULL_TEST=true\<close> before invoking @{tool build}.
- \<^item> @{system_option_def "timeout"} specifies a real wall-clock
- timeout (in seconds) for the session as a whole. The timer is
- controlled outside the ML process by the JVM that runs
- Isabelle/Scala. Thus it is relatively reliable in canceling
- processes that get out of control, even if there is a deadlock
- without CPU time usage.
+ \<^item> @{system_option_def "timeout"} specifies a real wall-clock timeout (in
+ seconds) for the session as a whole. The timer is controlled outside the
+ ML process by the JVM that runs Isabelle/Scala. Thus it is relatively
+ reliable in canceling processes that get out of control, even if there is
+ a deadlock without CPU time usage.
-
- The @{tool_def options} tool prints Isabelle system options. Its
+ The @{tool_def options} tool prints Isabelle system options. Its
command-line usage is:
@{verbatim [display]
\<open>Usage: isabelle options [OPTIONS] [MORE_OPTIONS ...]
@@ -235,31 +222,28 @@
Report Isabelle system options, augmented by MORE_OPTIONS given as
arguments NAME=VAL or NAME.\<close>}
- The command line arguments provide additional system options of the
- form \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close>
- for Boolean options.
+ The command line arguments provide additional system options of the form
+ \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> for Boolean options.
+
+ Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system options by the ones
+ of @{setting ISABELLE_BUILD_OPTIONS}, cf.\ \secref{sec:tool-build}.
- Option \<^verbatim>\<open>-b\<close> augments the implicit environment of system
- options by the ones of @{setting ISABELLE_BUILD_OPTIONS}, cf.\
- \secref{sec:tool-build}.
+ Option \<^verbatim>\<open>-g\<close> prints the value of the given option. Option \<^verbatim>\<open>-l\<close> lists all
+ options with their declaration and current value.
- Option \<^verbatim>\<open>-g\<close> prints the value of the given option.
- Option \<^verbatim>\<open>-l\<close> lists all options with their declaration and
- current value.
-
- Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in
- YXML format, instead of printing it in human-readable form.
+ Option \<^verbatim>\<open>-x\<close> specifies a file to export the result in YXML format, instead
+ of printing it in human-readable form.
\<close>
section \<open>Invoking the build process \label{sec:tool-build}\<close>
-text \<open>The @{tool_def build} tool invokes the build process for
- Isabelle sessions. It manages dependencies between sessions,
- related sources of theories and auxiliary files, and target heap
- images. Accordingly, it runs instances of the prover process with
- optional document preparation. Its command-line usage
- is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
+text \<open>
+ The @{tool_def build} tool invokes the build process for Isabelle sessions.
+ It manages dependencies between sessions, related sources of theories and
+ auxiliary files, and target heap images. Accordingly, it runs instances of
+ the prover process with optional document preparation. Its command-line
+ usage is:\<^footnote>\<open>Isabelle/Scala provides the same functionality via
\<^verbatim>\<open>isabelle.Build.build\<close>.\<close>
@{verbatim [display]
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
@@ -291,98 +275,87 @@
ML_OPTIONS="..."\<close>}
\<^medskip>
- Isabelle sessions are defined via session ROOT files as
- described in (\secref{sec:session-root}). The totality of sessions
- is determined by collecting such specifications from all Isabelle
- component directories (\secref{sec:components}), augmented by more
- directories given via options \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the
- command line. Each such directory may contain a session
+ Isabelle sessions are defined via session ROOT files as described in
+ (\secref{sec:session-root}). The totality of sessions is determined by
+ collecting such specifications from all Isabelle component directories
+ (\secref{sec:components}), augmented by more directories given via options
+ \<^verbatim>\<open>-d\<close>~\<open>DIR\<close> on the command line. Each such directory may contain a session
\<^verbatim>\<open>ROOT\<close> file with several session specifications.
- Any session root directory may refer recursively to further
- directories of the same kind, by listing them in a catalog file
- \<^verbatim>\<open>ROOTS\<close> line-by-line. This helps to organize large
- collections of session specifications, or to make \<^verbatim>\<open>-d\<close>
- command line options persistent (say within
+ Any session root directory may refer recursively to further directories of
+ the same kind, by listing them in a catalog file \<^verbatim>\<open>ROOTS\<close> line-by-line. This
+ helps to organize large collections of session specifications, or to make
+ \<^verbatim>\<open>-d\<close> command line options persistent (say within
\<^verbatim>\<open>$ISABELLE_HOME_USER/ROOTS\<close>).
\<^medskip>
- The subset of sessions to be managed is determined via
- individual \<open>SESSIONS\<close> given as command-line arguments, or
- session groups that are given via one or more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>.
- Option \<^verbatim>\<open>-a\<close> selects all sessions.
- The build tool takes session dependencies into account: the set of
- selected sessions is completed by including all ancestors.
+ The subset of sessions to be managed is determined via individual \<open>SESSIONS\<close>
+ given as command-line arguments, or session groups that are given via one or
+ more options \<^verbatim>\<open>-g\<close>~\<open>NAME\<close>. Option \<^verbatim>\<open>-a\<close> selects all sessions. The build tool
+ takes session dependencies into account: the set of selected sessions is
+ completed by including all ancestors.
\<^medskip>
- One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify
- sessions to be excluded. All descendents of excluded sessions are removed
- from the selection as specified above. Option \<^verbatim>\<open>-X\<close> is
- analogous to this, but excluded sessions are specified by session group
- membership.
+ One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
+ descendents of excluded sessions are removed from the selection as specified
+ above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
+ specified by session group membership.
\<^medskip>
- Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense
- that it refers to its requirements: all ancestor sessions excluding
- the original selection. This allows to prepare the stage for some
- build process with different options, before running the main build
- itself (without option \<^verbatim>\<open>-R\<close>).
+ Option \<^verbatim>\<open>-R\<close> reverses the selection in the sense that it refers to its
+ requirements: all ancestor sessions excluding the original selection. This
+ allows to prepare the stage for some build process with different options,
+ before running the main build itself (without option \<^verbatim>\<open>-R\<close>).
\<^medskip>
- Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but
- selects all sessions that are defined in the given directories.
+ Option \<^verbatim>\<open>-D\<close> is similar to \<^verbatim>\<open>-d\<close>, but selects all sessions that are defined
+ in the given directories.
\<^medskip>
The build process depends on additional options
- (\secref{sec:system-options}) that are passed to the prover
- eventually. The settings variable @{setting_ref
- ISABELLE_BUILD_OPTIONS} allows to provide additional defaults, e.g.\
- \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf threads=4"\<close>. Moreover,
- the environment of system build options may be 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>, which
- abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for
- Boolean options. Multiple occurrences of \<^verbatim>\<open>-o\<close> on the
- command-line are applied in the given order.
+ (\secref{sec:system-options}) that are passed to the prover eventually. The
+ settings variable @{setting_ref ISABELLE_BUILD_OPTIONS} allows to provide
+ additional defaults, e.g.\ \<^verbatim>\<open>ISABELLE_BUILD_OPTIONS="document=pdf
+ threads=4"\<close>. Moreover, the environment of system build options may be
+ 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>,
+ which abbreviates \<^verbatim>\<open>-o\<close>~\<open>name\<close>\<^verbatim>\<open>=true\<close> for Boolean options. Multiple
+ occurrences of \<^verbatim>\<open>-o\<close> on the command-line are applied in the given order.
\<^medskip>
- Option \<^verbatim>\<open>-b\<close> ensures that heap images are
- produced for all selected sessions. By default, images are only
- saved for inner nodes of the hierarchy of sessions, as required for
- other sessions to continue later on.
+ Option \<^verbatim>\<open>-b\<close> ensures that heap images are produced for all selected
+ sessions. By default, images are only saved for inner nodes of the hierarchy
+ of sessions, as required for other sessions to continue later on.
\<^medskip>
- Option \<^verbatim>\<open>-c\<close> cleans all descendants of the
- selected sessions before performing the specified build operation.
+ Option \<^verbatim>\<open>-c\<close> cleans all descendants of the selected sessions before
+ performing the specified build operation.
\<^medskip>
- Option \<^verbatim>\<open>-n\<close> omits the actual build process
- after the preparatory stage (including optional cleanup). Note that
- the return code always indicates the status of the set of selected
- sessions.
+ Option \<^verbatim>\<open>-n\<close> omits the actual build process after the preparatory stage
+ (including optional cleanup). Note that the return code always indicates the
+ status of the set of selected sessions.
\<^medskip>
- Option \<^verbatim>\<open>-j\<close> specifies the maximum number of
- parallel build jobs (prover processes). Each prover process is
- subject to a separate limit of parallel worker threads, cf.\ system
- option @{system_option_ref threads}.
+ Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
+ processes). Each prover process is subject to a separate limit of parallel
+ worker threads, cf.\ system option @{system_option_ref threads}.
\<^medskip>
- Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which
- means that resulting heap images and log files are stored in
- @{file_unchecked "$ISABELLE_HOME/heaps"} instead of the default location
- @{setting ISABELLE_OUTPUT} (which is normally in @{setting
- ISABELLE_HOME_USER}, i.e.\ the user's home directory).
+ Option \<^verbatim>\<open>-s\<close> enables \<^emph>\<open>system mode\<close>, which means that resulting heap images
+ and log files are stored in @{file_unchecked "$ISABELLE_HOME/heaps"} instead
+ of the default location @{setting ISABELLE_OUTPUT} (which is normally in
+ @{setting ISABELLE_HOME_USER}, i.e.\ the user's home directory).
\<^medskip>
- Option \<^verbatim>\<open>-v\<close> increases the general level of
- verbosity. Option \<^verbatim>\<open>-l\<close> lists the source files that
- contribute to a session.
+ Option \<^verbatim>\<open>-v\<close> increases the general level of verbosity. Option \<^verbatim>\<open>-l\<close> lists
+ the source files that contribute to a session.
\<^medskip>
- Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for
- outer syntax (multiple uses allowed). The theory sources are checked for
- conflicts wrt.\ this hypothetical change of syntax, e.g.\ to reveal
- occurrences of identifiers that need to be quoted.\<close>
+ Option \<^verbatim>\<open>-k\<close> specifies a newly proposed keyword for outer syntax (multiple
+ uses allowed). The theory sources are checked for conflicts wrt.\ this
+ hypothetical change of syntax, e.g.\ to reveal occurrences of identifiers
+ that need to be quoted.
+\<close>
subsubsection \<open>Examples\<close>
@@ -396,23 +369,22 @@
@{verbatim [display] \<open>isabelle build -b -g main\<close>}
\<^smallskip>
- Provide a general overview of the status of all Isabelle
- sessions, without building anything:
+ Provide a general overview of the status of all Isabelle sessions, without
+ building anything:
@{verbatim [display] \<open>isabelle build -a -n -v\<close>}
\<^smallskip>
- Build all sessions with HTML browser info and PDF
- document preparation:
+ Build all sessions with HTML browser info and PDF document preparation:
@{verbatim [display] \<open>isabelle build -a -o browser_info -o document=pdf\<close>}
\<^smallskip>
- Build all sessions with a maximum of 8 parallel prover
- processes and 4 worker threads each (on a machine with many cores):
+ Build all sessions with a maximum of 8 parallel prover processes and 4
+ worker threads each (on a machine with many cores):
@{verbatim [display] \<open>isabelle build -a -j8 -o threads=4\<close>}
\<^smallskip>
- Build some session images with cleanup of their
- descendants, while retaining their ancestry:
+ Build some session images with cleanup of their descendants, while retaining
+ their ancestry:
@{verbatim [display] \<open>isabelle build -b -c HOL-Algebra HOL-Word\<close>}
\<^smallskip>
@@ -420,14 +392,14 @@
@{verbatim [display] \<open>isabelle build -a -n -c\<close>}
\<^smallskip>
- Build all sessions from some other directory hierarchy,
- according to the settings variable \<^verbatim>\<open>AFP\<close> that happens to
- be defined inside the Isabelle environment:
+ Build all sessions from some other directory hierarchy, according to the
+ settings variable \<^verbatim>\<open>AFP\<close> that happens to be defined inside the Isabelle
+ environment:
@{verbatim [display] \<open>isabelle build -D '$AFP'\<close>}
\<^smallskip>
- Inform about the status of all sessions required for AFP,
- without building anything yet:
+ Inform about the status of all sessions required for AFP, without building
+ anything yet:
@{verbatim [display] \<open>isabelle build -D '$AFP' -R -v -n\<close>}
\<close>