wenzelm@28215: theory Basics
wenzelm@43564: imports Base
wenzelm@28215: begin
wenzelm@28215: 
wenzelm@28215: chapter {* The Isabelle system environment *}
wenzelm@28215: 
wenzelm@47823: text {* This manual describes Isabelle together with related tools and
wenzelm@47823:   user interfaces as seen from a system oriented view.  See also the
wenzelm@28916:   \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
wenzelm@47823:   the actual Isabelle input language and related concepts, and
wenzelm@47823:   \emph{The Isabelle/Isar Implementation
wenzelm@47823:   Manual}~\cite{isabelle-implementation} for the main concepts of the
wenzelm@47823:   underlying implementation in Isabelle/ML.
wenzelm@28215: 
wenzelm@28916:   \medskip The Isabelle system environment provides the following
wenzelm@28916:   basic infrastructure to integrate tools smoothly.
wenzelm@28215: 
wenzelm@28238:   \begin{enumerate}
wenzelm@28215: 
wenzelm@28916:   \item The \emph{Isabelle settings} mechanism provides process
wenzelm@28916:   environment variables to all Isabelle executables (including tools
wenzelm@28916:   and user interfaces).
wenzelm@28215: 
wenzelm@47823:   \item The raw \emph{Isabelle process} (@{executable_ref
wenzelm@28504:   "isabelle-process"}) runs logic sessions either interactively or in
wenzelm@28504:   batch mode.  In particular, this view abstracts over the invocation
wenzelm@28504:   of the actual ML system to be used.  Regular users rarely need to
wenzelm@28504:   care about the low-level process.
wenzelm@28215: 
wenzelm@48813:   \item The main \emph{Isabelle tool wrapper} (@{executable_ref
wenzelm@47823:   isabelle}) provides a generic startup environment Isabelle related
wenzelm@47823:   utilities, user interfaces etc.  Such tools automatically benefit
wenzelm@47823:   from the settings mechanism.
wenzelm@28215: 
wenzelm@28238:   \end{enumerate}
wenzelm@28215: *}
wenzelm@28215: 
wenzelm@28215: 
wenzelm@28215: section {* Isabelle settings \label{sec:settings} *}
wenzelm@28215: 
wenzelm@28215: text {*
wenzelm@28215:   The Isabelle system heavily depends on the \emph{settings
wenzelm@28215:   mechanism}\indexbold{settings}.  Essentially, this is a statically
wenzelm@28215:   scoped collection of environment variables, such as @{setting
wenzelm@28215:   ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
wenzelm@28215:   variables are \emph{not} intended to be set directly from the shell,
wenzelm@28215:   though.  Isabelle employs a somewhat more sophisticated scheme of
wenzelm@28215:   \emph{settings files} --- one for site-wide defaults, another for
wenzelm@28215:   additional user-specific modifications.  With all configuration
wenzelm@47823:   variables in clearly defined places, this scheme is more
wenzelm@47823:   maintainable and user-friendly than global shell environment
wenzelm@47823:   variables.
wenzelm@28215: 
wenzelm@28215:   In particular, we avoid the typical situation where prospective
wenzelm@28215:   users of a software package are told to put several things into
wenzelm@28215:   their shell startup scripts, before being able to actually run the
wenzelm@28215:   program. Isabelle requires none such administrative chores of its
wenzelm@28215:   end-users --- the executables can be invoked straight away.
wenzelm@40800:   Occasionally, users would still want to put the @{file
wenzelm@28238:   "$ISABELLE_HOME/bin"} directory into their shell's search path, but
wenzelm@28238:   this is not required.
wenzelm@28215: *}
wenzelm@28215: 
wenzelm@28215: 
wenzelm@32323: subsection {* Bootstrapping the environment \label{sec:boot} *}
wenzelm@28215: 
wenzelm@32323: text {* Isabelle executables need to be run within a proper settings
wenzelm@32323:   environment.  This is bootstrapped as described below, on the first
wenzelm@32323:   invocation of one of the outer wrapper scripts (such as
wenzelm@32323:   @{executable_ref isabelle}).  This happens only once for each
wenzelm@32323:   process tree, i.e.\ the environment is passed to subprocesses
wenzelm@32323:   according to regular Unix conventions.
wenzelm@28215: 
wenzelm@28215:   \begin{enumerate}
wenzelm@28215: 
wenzelm@28215:   \item The special variable @{setting_def ISABELLE_HOME} is
wenzelm@28215:   determined automatically from the location of the binary that has
wenzelm@28215:   been run.
wenzelm@28215:   
wenzelm@28215:   You should not try to set @{setting ISABELLE_HOME} manually. Also
wenzelm@28215:   note that the Isabelle executables either have to be run from their
wenzelm@28215:   original location in the distribution directory, or via the
wenzelm@48602:   executable objects created by the @{tool install} tool.  Symbolic
wenzelm@40800:   links are admissible, but a plain copy of the @{file
wenzelm@28238:   "$ISABELLE_HOME/bin"} files will not work!
wenzelm@28238: 
wenzelm@40800:   \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
wenzelm@28238:   @{executable_ref bash} shell script with the auto-export option for
wenzelm@28238:   variables enabled.
wenzelm@28215:   
wenzelm@28215:   This file holds a rather long list of shell variable assigments,
wenzelm@28215:   thus providing the site-wide default settings.  The Isabelle
wenzelm@28215:   distribution already contains a global settings file with sensible
wenzelm@28215:   defaults for most variables.  When installing the system, only a few
wenzelm@28215:   of these may have to be adapted (probably @{setting ML_SYSTEM}
wenzelm@28215:   etc.).
wenzelm@28215:   
wenzelm@28285:   \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
wenzelm@28215:   exists) is run in the same way as the site default settings. Note
wenzelm@28215:   that the variable @{setting ISABELLE_HOME_USER} has already been set
wenzelm@40387:   before --- usually to something like @{verbatim
wenzelm@47661:   "$USER_HOME/.isabelle/IsabelleXXXX"}.
wenzelm@28215:   
wenzelm@28215:   Thus individual users may override the site-wide defaults.  See also
wenzelm@40800:   file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
wenzelm@28238:   distribution.  Typically, a user settings file would contain only a
wenzelm@28238:   few lines, just the assigments that are really changed.  One should
wenzelm@40800:   definitely \emph{not} start with a full copy the basic @{file
wenzelm@28215:   "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
wenzelm@28215:   maintainance problems later, when the Isabelle installation is
wenzelm@28215:   updated or changed otherwise.
wenzelm@28215:   
wenzelm@28215:   \end{enumerate}
wenzelm@28215: 
wenzelm@28238:   Since settings files are regular GNU @{executable_def bash} scripts,
wenzelm@28238:   one may use complex shell commands, such as @{verbatim "if"} or
wenzelm@28215:   @{verbatim "case"} statements to set variables depending on the
wenzelm@28215:   system architecture or other environment variables.  Such advanced
wenzelm@28215:   features should be added only with great care, though. In
wenzelm@28215:   particular, external environment references should be kept at a
wenzelm@28215:   minimum.
wenzelm@28215: 
wenzelm@28215:   \medskip A few variables are somewhat special:
wenzelm@28215: 
wenzelm@28215:   \begin{itemize}
wenzelm@28215: 
wenzelm@28502:   \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
wenzelm@28215:   automatically to the absolute path names of the @{executable
wenzelm@28504:   "isabelle-process"} and @{executable isabelle} executables,
wenzelm@28215:   respectively.
wenzelm@28215:   
wenzelm@28238:   \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
wenzelm@28215:   the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
wenzelm@28215:   the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
wenzelm@28215:   to its value.
wenzelm@28215: 
wenzelm@28215:   \end{itemize}
wenzelm@28215: 
wenzelm@28238:   \medskip Note that the settings environment may be inspected with
wenzelm@48602:   the @{tool getenv} tool.  This might help to figure out the effect
wenzelm@48602:   of complex settings scripts.  *}
wenzelm@28215: 
wenzelm@28215: 
wenzelm@48602: subsection {* Common variables *}
wenzelm@28215: 
wenzelm@28215: text {*
wenzelm@28215:   This is a reference of common Isabelle settings variables. Note that
wenzelm@28215:   the list is somewhat open-ended. Third-party utilities or interfaces
wenzelm@28215:   may add their own selection. Variables that are special in some
wenzelm@28215:   sense are marked with @{text "\<^sup>*"}.
wenzelm@28215: 
wenzelm@28215:   \begin{description}
wenzelm@28215: 
wenzelm@47823:   \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform
wenzelm@47823:   user home directory.  On Unix systems this is usually the same as
wenzelm@47823:   @{setting HOME}, but on Windows it is the regular home directory of
wenzelm@47823:   the user, not the one of within the Cygwin root
wenzelm@47823:   file-system.\footnote{Cygwin itself offers another choice whether
wenzelm@47823:   its HOME should point to the \texttt{/home} directory tree or the
wenzelm@47823:   Windows user home.}
wenzelm@47661: 
wenzelm@47661:  \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
wenzelm@47661:   top-level Isabelle distribution directory. This is automatically
wenzelm@47661:   determined from the Isabelle executable that has been invoked.  Do
wenzelm@47661:   not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
wenzelm@28215:   counterpart of @{setting ISABELLE_HOME}. The default value is
wenzelm@47661:   relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
wenzelm@47661:   circumstances this may be changed in the global setting file.
wenzelm@47661:   Typically, the @{setting ISABELLE_HOME_USER} directory mimics
wenzelm@47661:   @{setting ISABELLE_HOME} to some extend. In particular, site-wide
wenzelm@47661:   defaults may be overridden by a private @{verbatim
wenzelm@40387:   "$ISABELLE_HOME_USER/etc/settings"}.
wenzelm@28215:   
wenzelm@36196:   \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
wenzelm@36196:   set to a symbolic identifier for the underlying hardware and
wenzelm@36196:   operating system.  The Isabelle platform identification always
wenzelm@36196:   refers to the 32 bit variant, even this is a 64 bit machine.  Note
wenzelm@36196:   that the ML or Java runtime may have a different idea, depending on
wenzelm@36196:   which binaries are actually run.
wenzelm@36196: 
wenzelm@36196:   \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
wenzelm@36196:   @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
wenzelm@36196:   on a platform that supports this; the value is empty for 32 bit.
wenzelm@47823:   Note that the following bash expression (including the quotes)
wenzelm@47823:   prefers the 64 bit platform, if that is available:
wenzelm@47823: 
wenzelm@47823:   @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}
wenzelm@36196: 
wenzelm@28502:   \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
wenzelm@28500:   ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
wenzelm@28215:   names of the @{executable "isabelle-process"} and @{executable
wenzelm@28504:   isabelle} executables, respectively.  Thus other tools and scripts
wenzelm@40800:   need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
wenzelm@28238:   on the current search path of the shell.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
wenzelm@28215:   to the name of this Isabelle distribution, e.g.\ ``@{verbatim
wenzelm@47823:   Isabelle2012}''.
wenzelm@28215: 
wenzelm@28215:   \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
wenzelm@28215:   @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
wenzelm@28215:   ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
wenzelm@28215:   to be used for Isabelle.  There is only a fixed set of admissable
wenzelm@40800:   @{setting ML_SYSTEM} names (see the @{file
wenzelm@28238:   "$ISABELLE_HOME/etc/settings"} file of the distribution).
wenzelm@28215:   
wenzelm@28215:   The actual compiler binary will be run from the directory @{setting
wenzelm@28215:   ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
wenzelm@28215:   command line.  The optional @{setting ML_PLATFORM} may specify the
wenzelm@28215:   binary format of ML heap images, which is useful for cross-platform
wenzelm@28215:   installations.  The value of @{setting ML_IDENTIFIER} is
wenzelm@28215:   automatically obtained by composing the values of @{setting
wenzelm@28215:   ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
wenzelm@47823: 
wenzelm@47823:   \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
wenzelm@47823:   (Java Development Kit) installation with @{verbatim javac} and
wenzelm@47823:   @{verbatim jar} executables.  This is essential for Isabelle/Scala
wenzelm@47823:   and other JVM-based tools to work properly.  Note that conventional
wenzelm@47823:   @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime
wenzelm@47823:   Environment), not JDK.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_PATH}] is a list of directories
wenzelm@28215:   (separated by colons) where Isabelle logic images may reside.  When
wenzelm@28215:   looking up heaps files, the value of @{setting ML_IDENTIFIER} is
wenzelm@28215:   appended to each component internally.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
wenzelm@28215:   directory where output heap files should be stored by default. The
wenzelm@28215:   ML system and Isabelle version identifier is appended here, too.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
wenzelm@28215:   theory browser information (HTML text, graph data, and printable
wenzelm@28215:   documents) is stored (see also \secref{sec:info}).  The default
wenzelm@28215:   value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
wenzelm@28215:   load if none is given explicitely by the user.  The default value is
wenzelm@28215:   @{verbatim HOL}.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
wenzelm@28238:   line editor for the @{tool_ref tty} interface.
wenzelm@28215: 
wenzelm@28215:   \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
wenzelm@28238:   to the command line of any @{tool_ref usedir} invocation. This
wenzelm@28238:   typically contains compilation options for object-logics --- @{tool
wenzelm@48602:   usedir} is the basic tool for managing logic sessions (cf.\ the
wenzelm@28238:   @{verbatim IsaMakefile}s in the distribution).
wenzelm@28215: 
wenzelm@28215:   \item[@{setting_def ISABELLE_LATEX}, @{setting_def
wenzelm@28215:   ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
wenzelm@28215:   ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
wenzelm@28215:   document preparation (see also \secref{sec:tool-latex}).
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
wenzelm@28504:   directories that are scanned by @{executable isabelle} for external
wenzelm@28504:   utility programs (see also \secref{sec:isabelle-tool}).
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
wenzelm@28215:   directories with documentation files.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
wenzelm@28215:   document format, typically @{verbatim dvi} or @{verbatim pdf}.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def DVI_VIEWER}] specifies the command to be used
wenzelm@28215:   for displaying @{verbatim dvi} files.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def PDF_VIEWER}] specifies the command to be used
wenzelm@28215:   for displaying @{verbatim pdf} files.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
wenzelm@28215:   spool command, which is expected to accept @{verbatim ps} files.
wenzelm@28215:   
wenzelm@28215:   \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
wenzelm@28238:   prefix from which any running @{executable "isabelle-process"}
wenzelm@28238:   derives an individual directory for temporary files.  The default is
wenzelm@28215:   somewhere in @{verbatim "/tmp"}.
wenzelm@28215:   
wenzelm@28215:   \end{description}
wenzelm@28215: *}
wenzelm@28215: 
wenzelm@28215: 
wenzelm@32323: subsection {* Additional components \label{sec:components} *}
wenzelm@32323: 
wenzelm@32323: text {* Any directory may be registered as an explicit \emph{Isabelle
wenzelm@32323:   component}.  The general layout conventions are that of the main
wenzelm@32323:   Isabelle distribution itself, and the following two files (both
wenzelm@32323:   optional) have a special meaning:
wenzelm@32323: 
wenzelm@32323:   \begin{itemize}
wenzelm@32323: 
wenzelm@32323:   \item @{verbatim "etc/settings"} holds additional settings that are
wenzelm@32323:   initialized when bootstrapping the overall Isabelle environment,
wenzelm@32323:   cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
wenzelm@32323:   @{verbatim bash} script.  It may refer to the component's enclosing
wenzelm@32323:   directory via the @{verbatim "COMPONENT"} shell variable.
wenzelm@32323: 
wenzelm@32323:   For example, the following setting allows to refer to files within
wenzelm@32323:   the component later on, without having to hardwire absolute paths:
wenzelm@32323: 
wenzelm@48838: \begin{ttbox}
wenzelm@48838: MY_COMPONENT_HOME="$COMPONENT"
wenzelm@48838: \end{ttbox}
wenzelm@32323: 
wenzelm@32323:   Components can also add to existing Isabelle settings such as
wenzelm@32323:   @{setting_def ISABELLE_TOOLS}, in order to provide
wenzelm@32323:   component-specific tools that can be invoked by end-users.  For
wenzelm@32323:   example:
wenzelm@32323: 
wenzelm@48838: \begin{ttbox}
wenzelm@48838: ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
wenzelm@48838: \end{ttbox}
wenzelm@32323: 
wenzelm@32323:   \item @{verbatim "etc/components"} holds a list of further
wenzelm@32323:   sub-components of the same structure.  The directory specifications
wenzelm@32323:   given here can be either absolute (with leading @{verbatim "/"}) or
wenzelm@32323:   relative to the component's main directory.
wenzelm@32323: 
wenzelm@32323:   \end{itemize}
wenzelm@32323: 
wenzelm@32323:   The root of component initialization is @{setting ISABELLE_HOME}
wenzelm@32323:   itself.  After initializing all of its sub-components recursively,
wenzelm@32323:   @{setting ISABELLE_HOME_USER} is included in the same manner (if
wenzelm@40569:   that directory exists).  This allows to install private components
wenzelm@40569:   via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
wenzelm@40569:   often more convenient to do that programmatically via the
wenzelm@40569:   \verb,init_component, shell function in the \verb,etc/settings,
wenzelm@40569:   script of \verb,$ISABELLE_HOME_USER, (or any other component
wenzelm@40569:   directory).  For example:
wenzelm@48838: \begin{ttbox}
wenzelm@48838: init_component "$HOME/screwdriver-2.0"
wenzelm@48838: \end{ttbox}
wenzelm@48838: 
wenzelm@48838:   This is tolerant wrt.\ missing component directories, but might
wenzelm@48838:   produce a warning.
wenzelm@48838: 
wenzelm@48838:   \medskip More complex situations may be addressed by initializing
wenzelm@48838:   components listed in a given catalog file, relatively to some base
wenzelm@48838:   directory:
wenzelm@48838: 
wenzelm@48838: \begin{ttbox}
wenzelm@48838: init_components "$HOME/my_component_store" "some_catalog_file"
wenzelm@48838: \end{ttbox}
wenzelm@48838: 
wenzelm@48838:   The component directories listed in the catalog file are treated as
wenzelm@48838:   relative to the given base directory.
wenzelm@48844: 
wenzelm@48844:   See also \secref{sec:tool-components} for some tool-support for
wenzelm@48844:   resolving components that are formally initialized but not installed
wenzelm@48844:   yet.
wenzelm@32323: *}
wenzelm@32323: 
wenzelm@32323: 
wenzelm@28215: section {* The raw Isabelle process *}
wenzelm@28215: 
wenzelm@28215: text {*
wenzelm@28504:   The @{executable_def "isabelle-process"} executable runs bare-bones
wenzelm@28504:   Isabelle logic sessions --- either interactively or in batch mode.
wenzelm@28504:   It provides an abstraction over the underlying ML system, and over
wenzelm@28504:   the actual heap file locations.  Its usage is:
wenzelm@28215: 
wenzelm@28215: \begin{ttbox}
wenzelm@28238: Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
wenzelm@28215: 
wenzelm@28215:   Options are:
wenzelm@28215:     -I           startup Isar interaction mode
wenzelm@28215:     -P           startup Proof General interaction mode
wenzelm@28215:     -S           secure mode -- disallow critical operations
wenzelm@45028:     -T ADDR      startup process wrapper, with socket address
wenzelm@38253:     -W IN:OUT    startup process wrapper, with input/output fifos
wenzelm@28215:     -X           startup PGIP interaction mode
wenzelm@28215:     -e MLTEXT    pass MLTEXT to the ML session
wenzelm@28215:     -f           pass 'Session.finish();' to the ML session
wenzelm@28215:     -m MODE      add print mode for output
wenzelm@28215:     -q           non-interactive session
wenzelm@28215:     -r           open heap file read-only
wenzelm@28215:     -u           pass 'use"ROOT.ML";' to the ML session
wenzelm@28215:     -w           reset write permissions on OUTPUT
wenzelm@28215: 
wenzelm@28215:   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
wenzelm@28215:   These are either names to be searched in the Isabelle path, or
wenzelm@28215:   actual file names (containing at least one /).
wenzelm@28215:   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
wenzelm@28215: \end{ttbox}
wenzelm@28215: 
wenzelm@28215:   Input files without path specifications are looked up in the
wenzelm@28215:   @{setting ISABELLE_PATH} setting, which may consist of multiple
wenzelm@28215:   components separated by colons --- these are tried in the given
wenzelm@28215:   order with the value of @{setting ML_IDENTIFIER} appended
wenzelm@28215:   internally.  In a similar way, base names are relative to the
wenzelm@28215:   directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
wenzelm@28215:   actual file locations may also be given by including at least one
wenzelm@28215:   slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
wenzelm@28215:   refer to the current directory).
wenzelm@28215: *}
wenzelm@28215: 
wenzelm@28215: 
wenzelm@28223: subsubsection {* Options *}
wenzelm@28215: 
wenzelm@28215: text {*
wenzelm@28215:   If the input heap file does not have write permission bits set, or
wenzelm@28215:   the @{verbatim "-r"} option is given explicitely, then the session
wenzelm@28215:   started will be read-only.  That is, the ML world cannot be
wenzelm@28215:   committed back into the image file.  Otherwise, a writable session
wenzelm@28215:   enables commits into either the input file, or into another output
wenzelm@28215:   heap file (if that is given as the second argument on the command
wenzelm@28215:   line).
wenzelm@28215: 
wenzelm@28215:   The read-write state of sessions is determined at startup only, it
wenzelm@28215:   cannot be changed intermediately. Also note that heap images may
wenzelm@28215:   require considerable amounts of disk space (approximately
wenzelm@28215:   50--200~MB). Users are responsible for themselves to dispose their
wenzelm@28215:   heap files when they are no longer needed.
wenzelm@28215: 
wenzelm@28215:   \medskip The @{verbatim "-w"} option makes the output heap file
wenzelm@28215:   read-only after terminating.  Thus subsequent invocations cause the
wenzelm@28215:   logic image to be read-only automatically.
wenzelm@28215: 
wenzelm@28215:   \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
wenzelm@28215:   passed to the Isabelle session from the command line. Multiple
wenzelm@28215:   @{verbatim "-e"}'s are evaluated in the given order. Strange things
wenzelm@28215:   may happen when errorneous ML code is provided. Also make sure that
wenzelm@28215:   the ML commands are terminated properly by semicolon.
wenzelm@28215: 
wenzelm@28215:   \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
wenzelm@28215:   "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
wenzelm@28223:   The @{verbatim "-f"} option passes ``@{verbatim
wenzelm@28223:   "Session.finish();"}'', which is intended mainly for administrative
wenzelm@28223:   purposes.
wenzelm@28215: 
wenzelm@28215:   \medskip The @{verbatim "-m"} option adds identifiers of print modes
wenzelm@28215:   to be made active for this session. Typically, this is used by some
wenzelm@28215:   user interface, e.g.\ to enable output of proper mathematical
wenzelm@28215:   symbols.
wenzelm@28215: 
wenzelm@28215:   \medskip Isabelle normally enters an interactive top-level loop
wenzelm@28215:   (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
wenzelm@28215:   option inhibits interaction, thus providing a pure batch mode
wenzelm@28215:   facility.
wenzelm@28215: 
wenzelm@28215:   \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
wenzelm@28215:   interaction mode on startup, instead of the primitive ML top-level.
wenzelm@28215:   The @{verbatim "-P"} option configures the top-level loop for
wenzelm@28215:   interaction with the Proof General user interface, and the
wenzelm@38253:   @{verbatim "-X"} option enables XML-based PGIP communication.
wenzelm@38253: 
wenzelm@45028:   \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
wenzelm@49173:   Isabelle enter a special process wrapper for interaction via
wenzelm@49173:   Isabelle/Scala, see also @{file
wenzelm@45028:   "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
wenzelm@45028:   the ML and JVM process is private to the implementation.
wenzelm@28215: 
wenzelm@28215:   \medskip The @{verbatim "-S"} option makes the Isabelle process more
wenzelm@28215:   secure by disabling some critical operations, notably runtime
wenzelm@28215:   compilation and evaluation of ML source code.
wenzelm@28215: *}
wenzelm@28215: 
wenzelm@28215: 
wenzelm@28223: subsubsection {* Examples *}
wenzelm@28215: 
wenzelm@28215: text {*
wenzelm@28215:   Run an interactive session of the default object-logic (as specified
wenzelm@28215:   by the @{setting ISABELLE_LOGIC} setting) like this:
wenzelm@28215: \begin{ttbox}
wenzelm@28238: isabelle-process
wenzelm@28215: \end{ttbox}
wenzelm@28215: 
wenzelm@28215:   Usually @{setting ISABELLE_LOGIC} refers to one of the standard
wenzelm@28215:   logic images, which are read-only by default.  A writable session
wenzelm@47823:   --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
wenzelm@28238:   directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
wenzelm@28215:   may be invoked as follows:
wenzelm@28215: \begin{ttbox}
wenzelm@47823: isabelle-process HOL Test
wenzelm@28215: \end{ttbox}
wenzelm@28215:   Ending this session normally (e.g.\ by typing control-D) dumps the
wenzelm@47823:   whole ML system state into @{verbatim Test} (be prepared for more
wenzelm@47823:   than 100\,MB):
wenzelm@28215: 
wenzelm@47823:   The @{verbatim Test} session may be continued later (still in
wenzelm@28215:   writable state) by:
wenzelm@28215: \begin{ttbox}
wenzelm@47823: isabelle-process Test
wenzelm@28215: \end{ttbox}
wenzelm@47823:   A read-only @{verbatim Test} session may be started by:
wenzelm@28215: \begin{ttbox}
wenzelm@47823: isabelle-process -r Test
wenzelm@28215: \end{ttbox}
wenzelm@28215: 
wenzelm@28215:   \medskip Note that manual session management like this does
wenzelm@28215:   \emph{not} provide proper setup for theory presentation.  This would
wenzelm@48602:   require @{tool usedir}.
wenzelm@28215: 
wenzelm@28238:   \bigskip The next example demonstrates batch execution of Isabelle.
wenzelm@47823:   We retrieve the @{verbatim Main} theory value from the theory loader
wenzelm@47823:   within ML (observe the delicate quoting rules for the Bash shell
wenzelm@47823:   vs.\ ML):
wenzelm@28215: \begin{ttbox}
wenzelm@47823: isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
wenzelm@28215: \end{ttbox}
wenzelm@28215:   Note that the output text will be interspersed with additional junk
wenzelm@28238:   messages by the ML runtime environment.  The @{verbatim "-W"} option
wenzelm@28238:   allows to communicate with the Isabelle process via an external
wenzelm@28238:   program in a more robust fashion.
wenzelm@28238: *}
wenzelm@28238: 
wenzelm@28238: 
wenzelm@48813: section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
wenzelm@28238: 
wenzelm@28238: text {*
wenzelm@28238:   All Isabelle related tools and interfaces are called via a common
wenzelm@28504:   wrapper --- @{executable isabelle}:
wenzelm@28238: 
wenzelm@28238: \begin{ttbox}
wenzelm@28504: Usage: isabelle TOOL [ARGS ...]
wenzelm@28238: 
wenzelm@28506:   Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
wenzelm@28238: 
wenzelm@48858: Available tools:
wenzelm@48858:   \dots
wenzelm@28238: \end{ttbox}
wenzelm@28238: 
wenzelm@28238:   In principle, Isabelle tools are ordinary executable scripts that
wenzelm@28238:   are run within the Isabelle settings environment, see
wenzelm@28238:   \secref{sec:settings}.  The set of available tools is collected by
wenzelm@28504:   @{executable isabelle} from the directories listed in the @{setting
wenzelm@28238:   ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
wenzelm@28238:   from the shell.  Neither should you add the tool directories to your
wenzelm@28238:   shell's search path!
wenzelm@28238: *}
wenzelm@28238: 
wenzelm@28238: 
wenzelm@28238: subsubsection {* Examples *}
wenzelm@28238: 
wenzelm@48813: text {* Show the list of available documentation of the Isabelle
wenzelm@48813:   distribution:
wenzelm@28238: 
wenzelm@28238: \begin{ttbox}
wenzelm@28504:   isabelle doc
wenzelm@28238: \end{ttbox}
wenzelm@28238: 
wenzelm@28238:   View a certain document as follows:
wenzelm@28238: \begin{ttbox}
wenzelm@47823:   isabelle doc system
wenzelm@28238: \end{ttbox}
wenzelm@28238: 
wenzelm@48813:   Query the Isabelle settings environment:
wenzelm@28238: \begin{ttbox}
wenzelm@48813:   isabelle getenv ISABELLE_HOME_USER
wenzelm@28238: \end{ttbox}
wenzelm@28215: *}
wenzelm@28215: 
wenzelm@28223: end