diff -r e6d9e46ff7bc -r e7418f8d49fe doc-src/System/Thy/Basics.thy --- a/doc-src/System/Thy/Basics.thy Mon Aug 27 16:10:54 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,554 +0,0 @@ -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