src/Doc/System/Basics.thy
changeset 48985 5386df44a037
parent 48937 e7418f8d49fe
child 49173 fa01a202399c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Doc/System/Basics.thy	Tue Aug 28 18:57:32 2012 +0200
     1.3 @@ -0,0 +1,554 @@
     1.4 +theory Basics
     1.5 +imports Base
     1.6 +begin
     1.7 +
     1.8 +chapter {* The Isabelle system environment *}
     1.9 +
    1.10 +text {* This manual describes Isabelle together with related tools and
    1.11 +  user interfaces as seen from a system oriented view.  See also the
    1.12 +  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
    1.13 +  the actual Isabelle input language and related concepts, and
    1.14 +  \emph{The Isabelle/Isar Implementation
    1.15 +  Manual}~\cite{isabelle-implementation} for the main concepts of the
    1.16 +  underlying implementation in Isabelle/ML.
    1.17 +
    1.18 +  \medskip The Isabelle system environment provides the following
    1.19 +  basic infrastructure to integrate tools smoothly.
    1.20 +
    1.21 +  \begin{enumerate}
    1.22 +
    1.23 +  \item The \emph{Isabelle settings} mechanism provides process
    1.24 +  environment variables to all Isabelle executables (including tools
    1.25 +  and user interfaces).
    1.26 +
    1.27 +  \item The raw \emph{Isabelle process} (@{executable_ref
    1.28 +  "isabelle-process"}) runs logic sessions either interactively or in
    1.29 +  batch mode.  In particular, this view abstracts over the invocation
    1.30 +  of the actual ML system to be used.  Regular users rarely need to
    1.31 +  care about the low-level process.
    1.32 +
    1.33 +  \item The main \emph{Isabelle tool wrapper} (@{executable_ref
    1.34 +  isabelle}) provides a generic startup environment Isabelle related
    1.35 +  utilities, user interfaces etc.  Such tools automatically benefit
    1.36 +  from the settings mechanism.
    1.37 +
    1.38 +  \end{enumerate}
    1.39 +*}
    1.40 +
    1.41 +
    1.42 +section {* Isabelle settings \label{sec:settings} *}
    1.43 +
    1.44 +text {*
    1.45 +  The Isabelle system heavily depends on the \emph{settings
    1.46 +  mechanism}\indexbold{settings}.  Essentially, this is a statically
    1.47 +  scoped collection of environment variables, such as @{setting
    1.48 +  ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
    1.49 +  variables are \emph{not} intended to be set directly from the shell,
    1.50 +  though.  Isabelle employs a somewhat more sophisticated scheme of
    1.51 +  \emph{settings files} --- one for site-wide defaults, another for
    1.52 +  additional user-specific modifications.  With all configuration
    1.53 +  variables in clearly defined places, this scheme is more
    1.54 +  maintainable and user-friendly than global shell environment
    1.55 +  variables.
    1.56 +
    1.57 +  In particular, we avoid the typical situation where prospective
    1.58 +  users of a software package are told to put several things into
    1.59 +  their shell startup scripts, before being able to actually run the
    1.60 +  program. Isabelle requires none such administrative chores of its
    1.61 +  end-users --- the executables can be invoked straight away.
    1.62 +  Occasionally, users would still want to put the @{file
    1.63 +  "$ISABELLE_HOME/bin"} directory into their shell's search path, but
    1.64 +  this is not required.
    1.65 +*}
    1.66 +
    1.67 +
    1.68 +subsection {* Bootstrapping the environment \label{sec:boot} *}
    1.69 +
    1.70 +text {* Isabelle executables need to be run within a proper settings
    1.71 +  environment.  This is bootstrapped as described below, on the first
    1.72 +  invocation of one of the outer wrapper scripts (such as
    1.73 +  @{executable_ref isabelle}).  This happens only once for each
    1.74 +  process tree, i.e.\ the environment is passed to subprocesses
    1.75 +  according to regular Unix conventions.
    1.76 +
    1.77 +  \begin{enumerate}
    1.78 +
    1.79 +  \item The special variable @{setting_def ISABELLE_HOME} is
    1.80 +  determined automatically from the location of the binary that has
    1.81 +  been run.
    1.82 +  
    1.83 +  You should not try to set @{setting ISABELLE_HOME} manually. Also
    1.84 +  note that the Isabelle executables either have to be run from their
    1.85 +  original location in the distribution directory, or via the
    1.86 +  executable objects created by the @{tool install} tool.  Symbolic
    1.87 +  links are admissible, but a plain copy of the @{file
    1.88 +  "$ISABELLE_HOME/bin"} files will not work!
    1.89 +
    1.90 +  \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
    1.91 +  @{executable_ref bash} shell script with the auto-export option for
    1.92 +  variables enabled.
    1.93 +  
    1.94 +  This file holds a rather long list of shell variable assigments,
    1.95 +  thus providing the site-wide default settings.  The Isabelle
    1.96 +  distribution already contains a global settings file with sensible
    1.97 +  defaults for most variables.  When installing the system, only a few
    1.98 +  of these may have to be adapted (probably @{setting ML_SYSTEM}
    1.99 +  etc.).
   1.100 +  
   1.101 +  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
   1.102 +  exists) is run in the same way as the site default settings. Note
   1.103 +  that the variable @{setting ISABELLE_HOME_USER} has already been set
   1.104 +  before --- usually to something like @{verbatim
   1.105 +  "$USER_HOME/.isabelle/IsabelleXXXX"}.
   1.106 +  
   1.107 +  Thus individual users may override the site-wide defaults.  See also
   1.108 +  file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
   1.109 +  distribution.  Typically, a user settings file would contain only a
   1.110 +  few lines, just the assigments that are really changed.  One should
   1.111 +  definitely \emph{not} start with a full copy the basic @{file
   1.112 +  "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
   1.113 +  maintainance problems later, when the Isabelle installation is
   1.114 +  updated or changed otherwise.
   1.115 +  
   1.116 +  \end{enumerate}
   1.117 +
   1.118 +  Since settings files are regular GNU @{executable_def bash} scripts,
   1.119 +  one may use complex shell commands, such as @{verbatim "if"} or
   1.120 +  @{verbatim "case"} statements to set variables depending on the
   1.121 +  system architecture or other environment variables.  Such advanced
   1.122 +  features should be added only with great care, though. In
   1.123 +  particular, external environment references should be kept at a
   1.124 +  minimum.
   1.125 +
   1.126 +  \medskip A few variables are somewhat special:
   1.127 +
   1.128 +  \begin{itemize}
   1.129 +
   1.130 +  \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
   1.131 +  automatically to the absolute path names of the @{executable
   1.132 +  "isabelle-process"} and @{executable isabelle} executables,
   1.133 +  respectively.
   1.134 +  
   1.135 +  \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
   1.136 +  the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
   1.137 +  the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
   1.138 +  to its value.
   1.139 +
   1.140 +  \end{itemize}
   1.141 +
   1.142 +  \medskip Note that the settings environment may be inspected with
   1.143 +  the @{tool getenv} tool.  This might help to figure out the effect
   1.144 +  of complex settings scripts.  *}
   1.145 +
   1.146 +
   1.147 +subsection {* Common variables *}
   1.148 +
   1.149 +text {*
   1.150 +  This is a reference of common Isabelle settings variables. Note that
   1.151 +  the list is somewhat open-ended. Third-party utilities or interfaces
   1.152 +  may add their own selection. Variables that are special in some
   1.153 +  sense are marked with @{text "\<^sup>*"}.
   1.154 +
   1.155 +  \begin{description}
   1.156 +
   1.157 +  \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform
   1.158 +  user home directory.  On Unix systems this is usually the same as
   1.159 +  @{setting HOME}, but on Windows it is the regular home directory of
   1.160 +  the user, not the one of within the Cygwin root
   1.161 +  file-system.\footnote{Cygwin itself offers another choice whether
   1.162 +  its HOME should point to the \texttt{/home} directory tree or the
   1.163 +  Windows user home.}
   1.164 +
   1.165 + \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
   1.166 +  top-level Isabelle distribution directory. This is automatically
   1.167 +  determined from the Isabelle executable that has been invoked.  Do
   1.168 +  not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
   1.169 +  
   1.170 +  \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
   1.171 +  counterpart of @{setting ISABELLE_HOME}. The default value is
   1.172 +  relative to @{verbatim "$USER_HOME/.isabelle"}, under rare
   1.173 +  circumstances this may be changed in the global setting file.
   1.174 +  Typically, the @{setting ISABELLE_HOME_USER} directory mimics
   1.175 +  @{setting ISABELLE_HOME} to some extend. In particular, site-wide
   1.176 +  defaults may be overridden by a private @{verbatim
   1.177 +  "$ISABELLE_HOME_USER/etc/settings"}.
   1.178 +  
   1.179 +  \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
   1.180 +  set to a symbolic identifier for the underlying hardware and
   1.181 +  operating system.  The Isabelle platform identification always
   1.182 +  refers to the 32 bit variant, even this is a 64 bit machine.  Note
   1.183 +  that the ML or Java runtime may have a different idea, depending on
   1.184 +  which binaries are actually run.
   1.185 +
   1.186 +  \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
   1.187 +  @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
   1.188 +  on a platform that supports this; the value is empty for 32 bit.
   1.189 +  Note that the following bash expression (including the quotes)
   1.190 +  prefers the 64 bit platform, if that is available:
   1.191 +
   1.192 +  @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}
   1.193 +
   1.194 +  \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
   1.195 +  ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
   1.196 +  names of the @{executable "isabelle-process"} and @{executable
   1.197 +  isabelle} executables, respectively.  Thus other tools and scripts
   1.198 +  need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
   1.199 +  on the current search path of the shell.
   1.200 +  
   1.201 +  \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
   1.202 +  to the name of this Isabelle distribution, e.g.\ ``@{verbatim
   1.203 +  Isabelle2012}''.
   1.204 +
   1.205 +  \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
   1.206 +  @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
   1.207 +  ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
   1.208 +  to be used for Isabelle.  There is only a fixed set of admissable
   1.209 +  @{setting ML_SYSTEM} names (see the @{file
   1.210 +  "$ISABELLE_HOME/etc/settings"} file of the distribution).
   1.211 +  
   1.212 +  The actual compiler binary will be run from the directory @{setting
   1.213 +  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
   1.214 +  command line.  The optional @{setting ML_PLATFORM} may specify the
   1.215 +  binary format of ML heap images, which is useful for cross-platform
   1.216 +  installations.  The value of @{setting ML_IDENTIFIER} is
   1.217 +  automatically obtained by composing the values of @{setting
   1.218 +  ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
   1.219 +
   1.220 +  \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
   1.221 +  (Java Development Kit) installation with @{verbatim javac} and
   1.222 +  @{verbatim jar} executables.  This is essential for Isabelle/Scala
   1.223 +  and other JVM-based tools to work properly.  Note that conventional
   1.224 +  @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime
   1.225 +  Environment), not JDK.
   1.226 +  
   1.227 +  \item[@{setting_def ISABELLE_PATH}] is a list of directories
   1.228 +  (separated by colons) where Isabelle logic images may reside.  When
   1.229 +  looking up heaps files, the value of @{setting ML_IDENTIFIER} is
   1.230 +  appended to each component internally.
   1.231 +  
   1.232 +  \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
   1.233 +  directory where output heap files should be stored by default. The
   1.234 +  ML system and Isabelle version identifier is appended here, too.
   1.235 +  
   1.236 +  \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
   1.237 +  theory browser information (HTML text, graph data, and printable
   1.238 +  documents) is stored (see also \secref{sec:info}).  The default
   1.239 +  value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
   1.240 +  
   1.241 +  \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
   1.242 +  load if none is given explicitely by the user.  The default value is
   1.243 +  @{verbatim HOL}.
   1.244 +  
   1.245 +  \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
   1.246 +  line editor for the @{tool_ref tty} interface.
   1.247 +
   1.248 +  \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
   1.249 +  to the command line of any @{tool_ref usedir} invocation. This
   1.250 +  typically contains compilation options for object-logics --- @{tool
   1.251 +  usedir} is the basic tool for managing logic sessions (cf.\ the
   1.252 +  @{verbatim IsaMakefile}s in the distribution).
   1.253 +
   1.254 +  \item[@{setting_def ISABELLE_LATEX}, @{setting_def
   1.255 +  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
   1.256 +  ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
   1.257 +  document preparation (see also \secref{sec:tool-latex}).
   1.258 +  
   1.259 +  \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
   1.260 +  directories that are scanned by @{executable isabelle} for external
   1.261 +  utility programs (see also \secref{sec:isabelle-tool}).
   1.262 +  
   1.263 +  \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
   1.264 +  directories with documentation files.
   1.265 +  
   1.266 +  \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
   1.267 +  document format, typically @{verbatim dvi} or @{verbatim pdf}.
   1.268 +  
   1.269 +  \item[@{setting_def DVI_VIEWER}] specifies the command to be used
   1.270 +  for displaying @{verbatim dvi} files.
   1.271 +  
   1.272 +  \item[@{setting_def PDF_VIEWER}] specifies the command to be used
   1.273 +  for displaying @{verbatim pdf} files.
   1.274 +  
   1.275 +  \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
   1.276 +  spool command, which is expected to accept @{verbatim ps} files.
   1.277 +  
   1.278 +  \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
   1.279 +  prefix from which any running @{executable "isabelle-process"}
   1.280 +  derives an individual directory for temporary files.  The default is
   1.281 +  somewhere in @{verbatim "/tmp"}.
   1.282 +  
   1.283 +  \end{description}
   1.284 +*}
   1.285 +
   1.286 +
   1.287 +subsection {* Additional components \label{sec:components} *}
   1.288 +
   1.289 +text {* Any directory may be registered as an explicit \emph{Isabelle
   1.290 +  component}.  The general layout conventions are that of the main
   1.291 +  Isabelle distribution itself, and the following two files (both
   1.292 +  optional) have a special meaning:
   1.293 +
   1.294 +  \begin{itemize}
   1.295 +
   1.296 +  \item @{verbatim "etc/settings"} holds additional settings that are
   1.297 +  initialized when bootstrapping the overall Isabelle environment,
   1.298 +  cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
   1.299 +  @{verbatim bash} script.  It may refer to the component's enclosing
   1.300 +  directory via the @{verbatim "COMPONENT"} shell variable.
   1.301 +
   1.302 +  For example, the following setting allows to refer to files within
   1.303 +  the component later on, without having to hardwire absolute paths:
   1.304 +
   1.305 +\begin{ttbox}
   1.306 +MY_COMPONENT_HOME="$COMPONENT"
   1.307 +\end{ttbox}
   1.308 +
   1.309 +  Components can also add to existing Isabelle settings such as
   1.310 +  @{setting_def ISABELLE_TOOLS}, in order to provide
   1.311 +  component-specific tools that can be invoked by end-users.  For
   1.312 +  example:
   1.313 +
   1.314 +\begin{ttbox}
   1.315 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
   1.316 +\end{ttbox}
   1.317 +
   1.318 +  \item @{verbatim "etc/components"} holds a list of further
   1.319 +  sub-components of the same structure.  The directory specifications
   1.320 +  given here can be either absolute (with leading @{verbatim "/"}) or
   1.321 +  relative to the component's main directory.
   1.322 +
   1.323 +  \end{itemize}
   1.324 +
   1.325 +  The root of component initialization is @{setting ISABELLE_HOME}
   1.326 +  itself.  After initializing all of its sub-components recursively,
   1.327 +  @{setting ISABELLE_HOME_USER} is included in the same manner (if
   1.328 +  that directory exists).  This allows to install private components
   1.329 +  via @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
   1.330 +  often more convenient to do that programmatically via the
   1.331 +  \verb,init_component, shell function in the \verb,etc/settings,
   1.332 +  script of \verb,$ISABELLE_HOME_USER, (or any other component
   1.333 +  directory).  For example:
   1.334 +\begin{ttbox}
   1.335 +init_component "$HOME/screwdriver-2.0"
   1.336 +\end{ttbox}
   1.337 +
   1.338 +  This is tolerant wrt.\ missing component directories, but might
   1.339 +  produce a warning.
   1.340 +
   1.341 +  \medskip More complex situations may be addressed by initializing
   1.342 +  components listed in a given catalog file, relatively to some base
   1.343 +  directory:
   1.344 +
   1.345 +\begin{ttbox}
   1.346 +init_components "$HOME/my_component_store" "some_catalog_file"
   1.347 +\end{ttbox}
   1.348 +
   1.349 +  The component directories listed in the catalog file are treated as
   1.350 +  relative to the given base directory.
   1.351 +
   1.352 +  See also \secref{sec:tool-components} for some tool-support for
   1.353 +  resolving components that are formally initialized but not installed
   1.354 +  yet.
   1.355 +*}
   1.356 +
   1.357 +
   1.358 +section {* The raw Isabelle process *}
   1.359 +
   1.360 +text {*
   1.361 +  The @{executable_def "isabelle-process"} executable runs bare-bones
   1.362 +  Isabelle logic sessions --- either interactively or in batch mode.
   1.363 +  It provides an abstraction over the underlying ML system, and over
   1.364 +  the actual heap file locations.  Its usage is:
   1.365 +
   1.366 +\begin{ttbox}
   1.367 +Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
   1.368 +
   1.369 +  Options are:
   1.370 +    -I           startup Isar interaction mode
   1.371 +    -P           startup Proof General interaction mode
   1.372 +    -S           secure mode -- disallow critical operations
   1.373 +    -T ADDR      startup process wrapper, with socket address
   1.374 +    -W IN:OUT    startup process wrapper, with input/output fifos
   1.375 +    -X           startup PGIP interaction mode
   1.376 +    -e MLTEXT    pass MLTEXT to the ML session
   1.377 +    -f           pass 'Session.finish();' to the ML session
   1.378 +    -m MODE      add print mode for output
   1.379 +    -q           non-interactive session
   1.380 +    -r           open heap file read-only
   1.381 +    -u           pass 'use"ROOT.ML";' to the ML session
   1.382 +    -w           reset write permissions on OUTPUT
   1.383 +
   1.384 +  INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
   1.385 +  These are either names to be searched in the Isabelle path, or
   1.386 +  actual file names (containing at least one /).
   1.387 +  If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   1.388 +\end{ttbox}
   1.389 +
   1.390 +  Input files without path specifications are looked up in the
   1.391 +  @{setting ISABELLE_PATH} setting, which may consist of multiple
   1.392 +  components separated by colons --- these are tried in the given
   1.393 +  order with the value of @{setting ML_IDENTIFIER} appended
   1.394 +  internally.  In a similar way, base names are relative to the
   1.395 +  directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
   1.396 +  actual file locations may also be given by including at least one
   1.397 +  slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
   1.398 +  refer to the current directory).
   1.399 +*}
   1.400 +
   1.401 +
   1.402 +subsubsection {* Options *}
   1.403 +
   1.404 +text {*
   1.405 +  If the input heap file does not have write permission bits set, or
   1.406 +  the @{verbatim "-r"} option is given explicitely, then the session
   1.407 +  started will be read-only.  That is, the ML world cannot be
   1.408 +  committed back into the image file.  Otherwise, a writable session
   1.409 +  enables commits into either the input file, or into another output
   1.410 +  heap file (if that is given as the second argument on the command
   1.411 +  line).
   1.412 +
   1.413 +  The read-write state of sessions is determined at startup only, it
   1.414 +  cannot be changed intermediately. Also note that heap images may
   1.415 +  require considerable amounts of disk space (approximately
   1.416 +  50--200~MB). Users are responsible for themselves to dispose their
   1.417 +  heap files when they are no longer needed.
   1.418 +
   1.419 +  \medskip The @{verbatim "-w"} option makes the output heap file
   1.420 +  read-only after terminating.  Thus subsequent invocations cause the
   1.421 +  logic image to be read-only automatically.
   1.422 +
   1.423 +  \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
   1.424 +  passed to the Isabelle session from the command line. Multiple
   1.425 +  @{verbatim "-e"}'s are evaluated in the given order. Strange things
   1.426 +  may happen when errorneous ML code is provided. Also make sure that
   1.427 +  the ML commands are terminated properly by semicolon.
   1.428 +
   1.429 +  \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
   1.430 +  "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
   1.431 +  The @{verbatim "-f"} option passes ``@{verbatim
   1.432 +  "Session.finish();"}'', which is intended mainly for administrative
   1.433 +  purposes.
   1.434 +
   1.435 +  \medskip The @{verbatim "-m"} option adds identifiers of print modes
   1.436 +  to be made active for this session. Typically, this is used by some
   1.437 +  user interface, e.g.\ to enable output of proper mathematical
   1.438 +  symbols.
   1.439 +
   1.440 +  \medskip Isabelle normally enters an interactive top-level loop
   1.441 +  (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
   1.442 +  option inhibits interaction, thus providing a pure batch mode
   1.443 +  facility.
   1.444 +
   1.445 +  \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
   1.446 +  interaction mode on startup, instead of the primitive ML top-level.
   1.447 +  The @{verbatim "-P"} option configures the top-level loop for
   1.448 +  interaction with the Proof General user interface, and the
   1.449 +  @{verbatim "-X"} option enables XML-based PGIP communication.
   1.450 +
   1.451 +  \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
   1.452 +  Isabelle enter a special process wrapper for interaction via the
   1.453 +  Isabelle/Scala layer, see also @{file
   1.454 +  "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
   1.455 +  the ML and JVM process is private to the implementation.
   1.456 +
   1.457 +  \medskip The @{verbatim "-S"} option makes the Isabelle process more
   1.458 +  secure by disabling some critical operations, notably runtime
   1.459 +  compilation and evaluation of ML source code.
   1.460 +*}
   1.461 +
   1.462 +
   1.463 +subsubsection {* Examples *}
   1.464 +
   1.465 +text {*
   1.466 +  Run an interactive session of the default object-logic (as specified
   1.467 +  by the @{setting ISABELLE_LOGIC} setting) like this:
   1.468 +\begin{ttbox}
   1.469 +isabelle-process
   1.470 +\end{ttbox}
   1.471 +
   1.472 +  Usually @{setting ISABELLE_LOGIC} refers to one of the standard
   1.473 +  logic images, which are read-only by default.  A writable session
   1.474 +  --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
   1.475 +  directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
   1.476 +  may be invoked as follows:
   1.477 +\begin{ttbox}
   1.478 +isabelle-process HOL Test
   1.479 +\end{ttbox}
   1.480 +  Ending this session normally (e.g.\ by typing control-D) dumps the
   1.481 +  whole ML system state into @{verbatim Test} (be prepared for more
   1.482 +  than 100\,MB):
   1.483 +
   1.484 +  The @{verbatim Test} session may be continued later (still in
   1.485 +  writable state) by:
   1.486 +\begin{ttbox}
   1.487 +isabelle-process Test
   1.488 +\end{ttbox}
   1.489 +  A read-only @{verbatim Test} session may be started by:
   1.490 +\begin{ttbox}
   1.491 +isabelle-process -r Test
   1.492 +\end{ttbox}
   1.493 +
   1.494 +  \medskip Note that manual session management like this does
   1.495 +  \emph{not} provide proper setup for theory presentation.  This would
   1.496 +  require @{tool usedir}.
   1.497 +
   1.498 +  \bigskip The next example demonstrates batch execution of Isabelle.
   1.499 +  We retrieve the @{verbatim Main} theory value from the theory loader
   1.500 +  within ML (observe the delicate quoting rules for the Bash shell
   1.501 +  vs.\ ML):
   1.502 +\begin{ttbox}
   1.503 +isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
   1.504 +\end{ttbox}
   1.505 +  Note that the output text will be interspersed with additional junk
   1.506 +  messages by the ML runtime environment.  The @{verbatim "-W"} option
   1.507 +  allows to communicate with the Isabelle process via an external
   1.508 +  program in a more robust fashion.
   1.509 +*}
   1.510 +
   1.511 +
   1.512 +section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
   1.513 +
   1.514 +text {*
   1.515 +  All Isabelle related tools and interfaces are called via a common
   1.516 +  wrapper --- @{executable isabelle}:
   1.517 +
   1.518 +\begin{ttbox}
   1.519 +Usage: isabelle TOOL [ARGS ...]
   1.520 +
   1.521 +  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
   1.522 +
   1.523 +Available tools:
   1.524 +  \dots
   1.525 +\end{ttbox}
   1.526 +
   1.527 +  In principle, Isabelle tools are ordinary executable scripts that
   1.528 +  are run within the Isabelle settings environment, see
   1.529 +  \secref{sec:settings}.  The set of available tools is collected by
   1.530 +  @{executable isabelle} from the directories listed in the @{setting
   1.531 +  ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
   1.532 +  from the shell.  Neither should you add the tool directories to your
   1.533 +  shell's search path!
   1.534 +*}
   1.535 +
   1.536 +
   1.537 +subsubsection {* Examples *}
   1.538 +
   1.539 +text {* Show the list of available documentation of the Isabelle
   1.540 +  distribution:
   1.541 +
   1.542 +\begin{ttbox}
   1.543 +  isabelle doc
   1.544 +\end{ttbox}
   1.545 +
   1.546 +  View a certain document as follows:
   1.547 +\begin{ttbox}
   1.548 +  isabelle doc system
   1.549 +\end{ttbox}
   1.550 +
   1.551 +  Query the Isabelle settings environment:
   1.552 +\begin{ttbox}
   1.553 +  isabelle getenv ISABELLE_HOME_USER
   1.554 +\end{ttbox}
   1.555 +*}
   1.556 +
   1.557 +end
   1.558 \ No newline at end of file