--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/System/Basics.thy Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,554 @@
+theory Basics
+imports Base
+begin
+
+chapter {* The Isabelle system environment *}
+
+text {* This manual describes Isabelle together with related tools and
+ user interfaces as seen from a system oriented view. See also the
+ \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
+ the actual Isabelle input language and related concepts, and
+ \emph{The Isabelle/Isar Implementation
+ Manual}~\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.
+
+ \begin{enumerate}
+
+ \item The \emph{Isabelle settings} mechanism provides process
+ environment variables to all Isabelle executables (including tools
+ and user interfaces).
+
+ \item The raw \emph{Isabelle process} (@{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.
+
+ \item The main \emph{Isabelle tool wrapper} (@{executable_ref
+ isabelle}) provides a generic startup environment Isabelle related
+ utilities, user interfaces etc. Such tools automatically benefit
+ from the settings mechanism.
+
+ \end{enumerate}
+*}
+
+
+section {* Isabelle settings \label{sec:settings} *}
+
+text {*
+ The Isabelle system heavily depends on the \emph{settings
+ mechanism}\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{not} intended to be set directly from the shell,
+ though. Isabelle employs a somewhat more sophisticated scheme of
+ \emph{settings files} --- 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
+ this is not required.
+*}
+
+
+subsection {* Bootstrapping the environment \label{sec:boot} *}
+
+text {* 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.
+
+ \begin{enumerate}
+
+ \item 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!
+
+ \item 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.).
+
+ \item The file @{verbatim "$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
+ "$USER_HOME/.isabelle/IsabelleXXXX"}.
+
+ Thus individual users may override the site-wide defaults. See also
+ file @{file "$ISABELLE_HOME/etc/user-settings.sample"} in the
+ distribution. Typically, a user settings file would contain only a
+ few lines, just the assigments that are really changed. One should
+ definitely \emph{not} start with a full copy the basic @{file
+ "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
+ maintainance problems later, when the Isabelle installation is
+ updated or changed otherwise.
+
+ \end{enumerate}
+
+ Since settings files are regular GNU @{executable_def bash} scripts,
+ one may use complex shell commands, such as @{verbatim "if"} or
+ @{verbatim "case"} 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:
+
+ \begin{itemize}
+
+ \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.
+
+ \end{itemize}
+
+ \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. *}
+
+
+subsection {* Common variables *}
+
+text {*
+ 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 @{text "\<^sup>*"}.
+
+ \begin{description}
+
+ \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] 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{Cygwin itself offers another choice whether
+ its HOME should point to the \texttt{/home} directory tree or the
+ Windows user home.}
+
+ \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] 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!
+
+ \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
+ counterpart of @{setting ISABELLE_HOME}. The default value is
+ relative to @{verbatim "$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
+ "$ISABELLE_HOME_USER/etc/settings"}.
+
+ \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] 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.
+
+ \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] 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] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}
+
+ \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
+ ISABELLE_TOOL}@{text "\<^sup>*"}] 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.
+
+ \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
+ to the name of this Isabelle distribution, e.g.\ ``@{verbatim
+ Isabelle2012}''.
+
+ \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
+ @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
+ ML_IDENTIFIER}@{text "\<^sup>*"}] 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.
+
+ \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
+ (Java Development Kit) installation with @{verbatim javac} and
+ @{verbatim jar} executables. This is essential for Isabelle/Scala
+ and other JVM-based tools to work properly. Note that conventional
+ @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime
+ Environment), not JDK.
+
+ \item[@{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.
+
+ \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
+ directory where output heap files should be stored by default. The
+ ML system and Isabelle version identifier is appended here, too.
+
+ \item[@{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 @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
+
+ \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
+ load if none is given explicitely by the user. The default value is
+ @{verbatim HOL}.
+
+ \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
+ line editor for the @{tool_ref tty} interface.
+
+ \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
+ to the command line of any @{tool_ref usedir} invocation. This
+ typically contains compilation options for object-logics --- @{tool
+ usedir} is the basic tool for managing logic sessions (cf.\ the
+ @{verbatim IsaMakefile}s in the distribution).
+
+ \item[@{setting_def ISABELLE_LATEX}, @{setting_def
+ ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
+ ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
+ document preparation (see also \secref{sec:tool-latex}).
+
+ \item[@{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}).
+
+ \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
+ directories with documentation files.
+
+ \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
+ document format, typically @{verbatim dvi} or @{verbatim pdf}.
+
+ \item[@{setting_def DVI_VIEWER}] specifies the command to be used
+ for displaying @{verbatim dvi} files.
+
+ \item[@{setting_def PDF_VIEWER}] specifies the command to be used
+ for displaying @{verbatim pdf} files.
+
+ \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
+ spool command, which is expected to accept @{verbatim ps} files.
+
+ \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
+ prefix from which any running @{executable "isabelle-process"}
+ derives an individual directory for temporary files. The default is
+ somewhere in @{verbatim "/tmp"}.
+
+ \end{description}
+*}
+
+
+subsection {* Additional components \label{sec:components} *}
+
+text {* Any directory may be registered as an explicit \emph{Isabelle
+ component}. The general layout conventions are that of the main
+ Isabelle distribution itself, and the following two files (both
+ optional) have a special meaning:
+
+ \begin{itemize}
+
+ \item @{verbatim "etc/settings"} 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 bash} script. It may refer to the component's enclosing
+ directory via the @{verbatim "COMPONENT"} shell variable.
+
+ For example, the following setting allows to refer to files within
+ the component later on, without having to hardwire absolute paths:
+
+\begin{ttbox}
+MY_COMPONENT_HOME="$COMPONENT"
+\end{ttbox}
+
+ 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:
+
+\begin{ttbox}
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
+\end{ttbox}
+
+ \item @{verbatim "etc/components"} holds a list of further
+ sub-components of the same structure. The directory specifications
+ given here can be either absolute (with leading @{verbatim "/"}) or
+ relative to the component's main directory.
+
+ \end{itemize}
+
+ 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 @{verbatim "$ISABELLE_HOME_USER/etc/components"}, although it is
+ often more convenient to do that programmatically via the
+ \verb,init_component, shell function in the \verb,etc/settings,
+ script of \verb,$ISABELLE_HOME_USER, (or any other component
+ directory). For example:
+\begin{ttbox}
+init_component "$HOME/screwdriver-2.0"
+\end{ttbox}
+
+ 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:
+
+\begin{ttbox}
+init_components "$HOME/my_component_store" "some_catalog_file"
+\end{ttbox}
+
+ 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.
+*}
+
+
+section {* The raw Isabelle process *}
+
+text {*
+ 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:
+
+\begin{ttbox}
+Usage: isabelle-process [OPTIONS] [INPUT] [OUTPUT]
+
+ Options are:
+ -I startup Isar interaction mode
+ -P startup Proof General interaction mode
+ -S secure mode -- disallow critical operations
+ -T ADDR startup process wrapper, with socket address
+ -W IN:OUT startup process wrapper, with input/output fifos
+ -X startup PGIP interaction mode
+ -e MLTEXT pass MLTEXT to the ML session
+ -f pass 'Session.finish();' to the ML session
+ -m MODE add print mode for output
+ -q non-interactive session
+ -r open heap file read-only
+ -u pass 'use"ROOT.ML";' to the ML session
+ -w reset write permissions on OUTPUT
+
+ INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
+ These are either names to be searched in the Isabelle path, or
+ actual file names (containing at least one /).
+ If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
+\end{ttbox}
+
+ 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 "/"}) in the name (hint: use @{verbatim "./"} to
+ refer to the current directory).
+*}
+
+
+subsubsection {* Options *}
+
+text {*
+ If the input heap file does not have write permission bits set, or
+ the @{verbatim "-r"} option is given explicitely, 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 (approximately
+ 50--200~MB). Users are responsible for themselves to dispose their
+ heap files when they are no longer needed.
+
+ \medskip The @{verbatim "-w"} 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 "-e"} option, arbitrary ML code may be
+ passed to the Isabelle session from the command line. Multiple
+ @{verbatim "-e"}'s are evaluated in the given order. Strange things
+ may happen when errorneous ML code is provided. Also make sure that
+ the ML commands are terminated properly by semicolon.
+
+ \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
+ "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
+ The @{verbatim "-f"} option passes ``@{verbatim
+ "Session.finish();"}'', which is intended mainly for administrative
+ purposes.
+
+ \medskip The @{verbatim "-m"} 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 "-e"} texts). The @{verbatim "-q"}
+ option inhibits interaction, thus providing a pure batch mode
+ facility.
+
+ \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
+ interaction mode on startup, instead of the primitive ML top-level.
+ The @{verbatim "-P"} option configures the top-level loop for
+ interaction with the Proof General user interface, and the
+ @{verbatim "-X"} option enables XML-based PGIP communication.
+
+ \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
+ Isabelle enter a special process wrapper for interaction via the
+ Isabelle/Scala layer, see also @{file
+ "~~/src/Pure/System/isabelle_process.scala"}. The protocol between
+ the ML and JVM process is private to the implementation.
+
+ \medskip The @{verbatim "-S"} option makes the Isabelle process more
+ secure by disabling some critical operations, notably runtime
+ compilation and evaluation of ML source code.
+*}
+
+
+subsubsection {* Examples *}
+
+text {*
+ Run an interactive session of the default object-logic (as specified
+ by the @{setting ISABELLE_LOGIC} setting) like this:
+\begin{ttbox}
+isabelle-process
+\end{ttbox}
+
+ Usually @{setting ISABELLE_LOGIC} refers to one of the standard
+ logic images, which are read-only by default. A writable session
+ --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
+ directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
+ may be invoked as follows:
+\begin{ttbox}
+isabelle-process HOL Test
+\end{ttbox}
+ Ending this session normally (e.g.\ by typing control-D) dumps the
+ whole ML system state into @{verbatim Test} (be prepared for more
+ than 100\,MB):
+
+ The @{verbatim Test} session may be continued later (still in
+ writable state) by:
+\begin{ttbox}
+isabelle-process Test
+\end{ttbox}
+ A read-only @{verbatim Test} session may be started by:
+\begin{ttbox}
+isabelle-process -r Test
+\end{ttbox}
+
+ \medskip Note that manual session management like this does
+ \emph{not} provide proper setup for theory presentation. This would
+ require @{tool usedir}.
+
+ \bigskip The next example demonstrates batch execution of Isabelle.
+ We retrieve the @{verbatim Main} theory value from the theory loader
+ within ML (observe the delicate quoting rules for the Bash shell
+ vs.\ ML):
+\begin{ttbox}
+isabelle-process -e 'Thy_Info.get_theory "Main";' -q -r HOL
+\end{ttbox}
+ Note that the output text will be interspersed with additional junk
+ messages by the ML runtime environment. The @{verbatim "-W"} option
+ allows to communicate with the Isabelle process via an external
+ program in a more robust fashion.
+*}
+
+
+section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
+
+text {*
+ All Isabelle related tools and interfaces are called via a common
+ wrapper --- @{executable isabelle}:
+
+\begin{ttbox}
+Usage: isabelle TOOL [ARGS ...]
+
+ Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
+
+Available tools:
+ \dots
+\end{ttbox}
+
+ 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!
+*}
+
+
+subsubsection {* Examples *}
+
+text {* Show the list of available documentation of the Isabelle
+ distribution:
+
+\begin{ttbox}
+ isabelle doc
+\end{ttbox}
+
+ View a certain document as follows:
+\begin{ttbox}
+ isabelle doc system
+\end{ttbox}
+
+ Query the Isabelle settings environment:
+\begin{ttbox}
+ isabelle getenv ISABELLE_HOME_USER
+\end{ttbox}
+*}
+
+end
\ No newline at end of file