# HG changeset patch # User wenzelm # Date 1221489720 -7200 # Node ID a1cfc43ac47d1a9cf4f78075ac11839ddb2ba4d6 # Parent 1e6d71cd4bf32f6a341cb0389ecc8a2b2ff42818 converted basics.tex to theory file; diff -r 1e6d71cd4bf3 -r a1cfc43ac47d doc-src/System/Makefile --- a/doc-src/System/Makefile Mon Sep 15 16:40:53 2008 +0200 +++ b/doc-src/System/Makefile Mon Sep 15 16:42:00 2008 +0200 @@ -12,7 +12,7 @@ include ../Makefile.in NAME = system -FILES = system.tex basics.tex misc.tex present.tex symbols.tex \ +FILES = system.tex Thy/document/Basics.tex misc.tex present.tex symbols.tex \ ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib OUTPUT = syms.tex diff -r 1e6d71cd4bf3 -r a1cfc43ac47d doc-src/System/Thy/Basics.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Basics.thy Mon Sep 15 16:42:00 2008 +0200 @@ -0,0 +1,527 @@ +(* $Id$ *) + +theory Basics +imports Pure +begin + +chapter {* The Isabelle system environment *} + +text {* + This manual describes Isabelle together with related tools and user + interfaces as seen from an outside (system oriented) view. See also + the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} + and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the + actual Isabelle commands and related functions. + + \medskip The Isabelle system environment emerges from a few general + concepts. + + \begin{itemize} + + \item The \emph{Isabelle settings mechanism} provides environment variables to + all Isabelle programs (including tools and user interfaces). + + \item The \emph{Isabelle tools wrapper} (@{executable_def isatool}) + provides a generic startup platform for Isabelle related utilities. + Thus tools automatically benefit from the settings mechanism. + + \item The raw \emph{Isabelle process} (@{executable_def isabelle} or + @{executable_def "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. + + \item The \emph{Isabelle interface wrapper} (@{executable_def + Isabelle} or @{executable_def "isabelle-interface"}) provides some + abstraction over the actual user interface to be used. The de-facto + standard interface for Isabelle is Proof~General + \cite{proofgeneral}. + + \end{itemize} + + \medskip The beginning user would probably just run the default user + interface (by invoking the capital @{executable Isabelle}). This + assumes that the system has already been installed, of course. In + case you have to do this yourself, see the @{verbatim INSTALL} file + in the top-level directory of the distribution of how to proceed; + binary packages for various system components are available as well. +*} + + +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 at most two 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 Isabelle @{verbatim + bin} directory into their shell's search path, but this is not + required. +*} + + +subsection {* Building the environment *} + +text {* + Whenever any of the Isabelle executables is run, their settings + environment is put together as follows. + + \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} utility (see + \secref{sec:tool-install}). Just doing a plain copy of the + @{verbatim bin} files will not work! + + \item The file @{verbatim "$ISABELLE_HOME/etc/settings"} ist run as + a 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 @{verbatim "~/isabelle"}. + + Thus individual users may override the site-wide defaults. See also + file @{verbatim "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 @{verbatim + "$ISABELLE_HOME/etc/settings"}. This could cause very annoying + maintainance problems later, when the Isabelle installation is + updated or changed otherwise. + + \end{enumerate} + + Note that settings files are actually full GNU bash scripts. So 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} and @{setting_def ISATOOL} are set + automatically to the absolute path names of the @{executable + "isabelle-process"} and @{executable isatool} executables, + respectively. + + \item @{setting_def 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 The Isabelle settings scheme is conceptually simple, but + not completely trivial. For debugging purposes, the resulting + environment may be inspected with the @{tool getenv} utility, see + \secref{sec:tool-getenv}. +*} + + +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 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 + @{verbatim "~/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 "etc/settings"}. + + \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting + ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path + names of the @{executable "isabelle-process"} and @{executable + isatool} executables, respectively. Thus other tools and scripts + need not assume that the Isabelle @{verbatim 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 + Isabelle2008}''. + + \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 @{verbatim "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_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 @{verbatim "isatool tty"} (see also + \secref{sec:tool-tty}). + + \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed + to the command line of any @{verbatim "isatool usedir"} invocation + (see also \secref{sec:tool-usedir}). This typically contains + compilation options for object-logics --- @{tool usedir} is the + basic utility for managing logic sessions (cf.\ the @{verbatim + IsaMakefile}s in the distribution). + + \item[@{setting_def ISABELLE_FILE_IDENT}] specifies a shell command + for producing a source file identification, based on the actual + content instead of the full physical path and date stamp (which is + the default). A typical identification would produce a ``digest'' of + the text, using a cryptographic hash function like SHA-1, for + example. + + \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 isatool} for external + utility programs (see also \secref{sec:isatool}). + + \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"}. + + \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that + specifies the actual user interface that the capital @{executable + Isabelle} or @{executable "isabelle-interface"} should invoke. See + \secref{sec:interface} for more details. + + \end{description} +*} + + +section {* The Isabelle tools wrapper \label{sec:isatool} *} + +text {* + All Isabelle related utilities are called via a common wrapper --- + \ttindex{isatool}: + +\begin{ttbox} +Usage: isatool TOOL [ARGS ...] + + Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL + for more specific help. + + Available tools are: + + browser - Isabelle graph browser + \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 isatool} 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 current Isabelle + installation like this: + +\begin{ttbox} + isatool doc +\end{ttbox} + + View a certain document as follows: +\begin{ttbox} + isatool doc isar-ref +\end{ttbox} + + Create an Isabelle session derived from HOL (see also + \secref{sec:tool-mkdir} and \secref{sec:tool-make}): +\begin{ttbox} + isatool mkdir HOL Test && isatool make +\end{ttbox} + Note that @{verbatim "isatool mkdir"} is usually only invoked once; + existing sessions (including document output etc.) are then updated + by @{verbatim "isatool make"} alone. +*} + + +section {* The raw Isabelle process *} + +text {* + The @{executable_ref isabelle} (or @{executable_ref + "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 [OPTIONS] [INPUT] [OUTPUT] + + Options are: + -C tell ML system to copy output image + -I startup Isar interaction mode + -P startup Proof General interaction mode + -S secure mode -- disallow critical operations + -W OUTPUT startup process wrapper, with messages going to OUTPUT stream + -X startup PGIP interaction mode + -c tell ML system to compress output image + -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). +*} + + +subsection {* 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 The @{verbatim "-c"} option tells the underlying ML system + to compress the output heap (fully transparently). On Poly/ML for + example, the image is garbage collected and all stored values are + maximally shared, resulting in up to @{text "50%"} less disk space + consumption. + + \medskip The @{verbatim "-C"} option tells the ML system to produce + a completely self-contained output image, probably including a copy + of the ML runtime system itself. + + \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. The + @{verbatim "-W"} option makes Isabelle enter a special process + wrapper for interaction via an external program; the protocol is a + stripped-down version of Proof General the interaction mode. + + \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. +*} + + +subsection {* Examples *} + +text {* + Run an interactive session of the default object-logic (as specified + by the @{setting ISABELLE_LOGIC} setting) like this: +\begin{ttbox} +isabelle +\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 FOL}, but output to @{verbatim Foo} (in the + directory specified by the @{verbatim ISABELLE_OUTPUT} setting) --- + may be invoked as follows: +\begin{ttbox} +isabelle FOL Foo +\end{ttbox} + Ending this session normally (e.g.\ by typing control-D) dumps the + whole ML system state into @{verbatim Foo}. Be prepared for several + tens of megabytes. + + The @{verbatim Foo} session may be continued later (still in + writable state) by: +\begin{ttbox} +isabelle Foo +\end{ttbox} + A read-only @{verbatim Foo} session may be started by: +\begin{ttbox} +isabelle -r Foo +\end{ttbox} + + \medskip Note that manual session management like this does + \emph{not} provide proper setup for theory presentation. This would + require the @{tool usedir} utility, see \secref{sec:tool-usedir}. + + \bigskip The next example demonstrates batch execution of + Isabelle. We print a certain theorem of @{verbatim FOL}: +\begin{ttbox} +isabelle -e "prth allE;" -q -r FOL +\end{ttbox} + Note that the output text will be interspersed with additional junk + messages by the ML runtime environment. +*} + + +section {* The Isabelle interface wrapper \label{sec:interface} *} + +text {* + Isabelle is a generic theorem prover, even w.r.t.\ its user + interface. The @{executable_ref Isabelle} (or @{executable_ref + "isabelle-interface"}) executable provides a uniform way for + end-users to invoke a certain interface; which one to start is + determined by the @{setting_ref ISABELLE_INTERFACE} setting + variable, which should give a full path specification to the actual + executable. Also note that the @{tool install} utility provides + some options to install desktop environment icons (see + \secref{sec:tool-install}). + + Presently, the most prominent Isabelle interface is Proof + General~\cite{proofgeneral}\index{user interface!Proof General}. + The Proof General distribution includes an interface wrapper script + for the regular Isar toplevel, see @{verbatim + "ProofGeneral/isar/interface"}. The canonical settings for + Isabelle/Isar are as follows: + +\begin{ttbox} +ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface +PROOFGENERAL_OPTIONS="" +\end{ttbox} + + Thus @{executable Isabelle} would automatically invoke Emacs with + proper setup of the Proof General Lisp packages. There are some + options available, such as @{verbatim "-l"} for passing the logic + image to be used by default, or @{verbatim "-m"} to tune the + standard print mode. The @{verbatim "-I"} option allows to switch + between the Isar and ML view, independently of the interface script + being used. + + \medskip Note that the world may be also seen the other way round: + Emacs may be started first (with proper setup of Proof General + mode), and @{executable isabelle} run from within. This requires + further Emacs Lisp configuration, see the Proof General + documentation \cite{proofgeneral} for more information. +*} + +end diff -r 1e6d71cd4bf3 -r a1cfc43ac47d doc-src/System/basics.tex --- a/doc-src/System/basics.tex Mon Sep 15 16:40:53 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,450 +0,0 @@ - -% $Id$ - -\chapter{The Isabelle system environment} - -This manual describes Isabelle together with related tools and user interfaces -as seen from an outside (system oriented) view. See also the -\emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} and the -\emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the actual Isabelle -commands and related functions. - -\medskip The Isabelle system environment emerges from a few general concepts. -\begin{itemize} -\item The \emph{Isabelle settings mechanism} provides environment variables to - all Isabelle programs (including tools and user interfaces). -\item The \emph{Isabelle tools wrapper} (\ttindex{isatool}) provides a generic - startup platform for Isabelle related utilities. Thus tools automatically - benefit from the settings mechanism. -\item The raw \emph{Isabelle process} (\ttindex{isabelle} or - \texttt{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. -\item The \emph{Isabelle interface wrapper} (\ttindex{Isabelle} or - \texttt{isabelle-interface}) provides some abstraction over the actual user - interface to be used. The de-facto standard interface for Isabelle is - Proof~General \cite{proofgeneral}. -\end{itemize} - -\medskip The beginning user would probably just run the default user interface -(by invoking the capital \texttt{Isabelle}). This assumes that the system has -already been installed, of course. In case you have to do this yourself, see -the \ttindex{INSTALL} file in the top-level directory of the distribution of -how to proceed; binary packages for various system components are available as -well. - - -\section{Isabelle settings} \label{sec:settings} - -The Isabelle system heavily depends on the \emph{settings - mechanism}\indexbold{settings}. Essentially, this is a statically scoped -collection of environment variables, such as \texttt{ISABELLE_HOME}, -\texttt{ML_SYSTEM}, \texttt{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 at most two 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.\footnote{Occasionally, users would still want to put the - Isabelle \texttt{bin} directory into their shell's search path, but this is - not required.} - - -\subsection{Building the environment} - -Whenever any of the Isabelle executables is run, their settings environment is -put together as follows. - -\begin{enumerate} -\item The special variable \settdx{ISABELLE_HOME} is determined automatically - from the location of the binary that has been run. - - You should not try to set \texttt{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 - \texttt{install} utility (see \S\ref{sec:tool-install}). Just doing a plain - copy of the \texttt{bin} files will not work! - -\item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a 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 \texttt{ML_SYSTEM} etc.). - -\item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is - run in the same way as the site default settings. Note that the variable - \texttt{ISABELLE_HOME_USER} has already been set before --- usually to - \texttt{\~\relax/isabelle}. - - Thus individual users may override the site-wide defaults. See also file - \texttt{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 \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very annoying - maintainance problems later, when the Isabelle installation is updated or - changed otherwise. - -\end{enumerate} - -Note that settings files are actually full GNU bash scripts. So one may use -complex shell commands, such as \texttt{if} or \texttt{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 \settdx{ISABELLE} and \settdx{ISATOOL} are set automatically to the - absolute path names of the \texttt{isabelle-process} and \texttt{isatool} - executables, respectively. - -\item \settdx{ISABELLE_OUTPUT} will have the identifiers of the - Isabelle distribution (cf.\ \texttt{ISABELLE_IDENTIFIER}) and the - {\ML} system (cf.\ \texttt{ML_IDENTIFIER}) appended automatically to - its value. -\end{itemize} - -\medskip The Isabelle settings scheme is conceptually simple, but not -completely trivial. For debugging purposes, the resulting environment may be -inspected with the \texttt{getenv} utility, see \S\ref{sec:tool-getenv}. - - -\subsection{Common variables} - -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 *. - -\begin{description} -\item[\settdx{ISABELLE_HOME}*] 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 - \texttt{ISABELLE_HOME} yourself from the shell. - -\item[\settdx{ISABELLE_HOME_USER}] is the user-specific counterpart of - \texttt{ISABELLE_HOME}. The default value is \texttt{\~\relax/isabelle}, - under rare circumstances this may be changed in the global setting file. - Typically, the \texttt{ISABELLE_HOME_USER} directory mimics - \texttt{ISABELLE_HOME} to some extend. In particular, site-wide defaults may - be overridden by a private \texttt{etc/settings}. - -\item[\settdx{ISABELLE}*, \settdx{ISATOOL}*] are automatically set to the full - path names of the \texttt{isabelle-process} and \texttt{isatool} - executables, respectively. Thus other tools and scripts need not assume - that the Isabelle \texttt{bin} directory is on the current search path of - the shell. - -\item[\settdx{ISABELLE_IDENTIFIER}*] refers to the name of this - Isabelle distribution, e.g.\ ``\texttt{Isabelle2007}''. - -\item[\settdx{ML_SYSTEM}, \settdx{ML_HOME}, \settdx{ML_OPTIONS}, - \settdx{ML_PLATFORM}, \settdx{ML_IDENTIFIER}*] specify the underlying {\ML} - system to be used for Isabelle. There is only a fixed set of admissable - \texttt{ML_SYSTEM} names (see the \texttt{etc/settings} file of the - distribution). - - The actual compiler binary will be run from the directory \texttt{ML_HOME}, - with \texttt{ML_OPTIONS} as first arguments on the command line. The - optional \texttt{ML_PLATFORM} may specify the binary format of ML heap - images, which is useful for cross-platform installations. The value of - \texttt{ML_IDENTIFIER} is automatically obtained by composing the values of - \texttt{ML_SYSTEM}, \texttt{ML_PLATFORM} and the Isabelle version values. - -\item[\settdx{ISABELLE_PATH}] is a list of directories (separated by colons) - where Isabelle logic images may reside. When looking up heaps files, the - value of \texttt{ML_IDENTIFIER} is appended to each component internally. - -\item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap files should - be stored by default. The {\ML} system and Isabelle version identifier is - appended here, too. - -\item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory browser - information (HTML text, graph data, and printable documents) is stored (see - also \S\ref{sec:info}). The default value is - \texttt{\$ISABELLE_HOME_USER/browser_info}. - -\item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if none is - given explicitely by the user. The default value is \texttt{HOL}. - -\item[\settdx{ISABELLE_LINE_EDITOR}] specifies the default line editor - for \texttt{isatool tty} (see also \S\ref{sec:tool-tty}). - -\item[\settdx{ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed to the command - line of any \texttt{isatool usedir} invocation (see also - \S\ref{sec:tool-usedir}). This typically contains compilation options for - object-logics --- \texttt{usedir} is the basic utility for managing logic - sessions (cf.\ the \texttt{IsaMakefile}s in the distribution). - -\item[\settdx{ISABELLE_FILE_IDENT}] specifies a shell command for - producing a source file identification, based on the actual content - instead of the full physical path and date stamp (which is the - default). A typical identification would produce a ``digest'' of the - text, using a cryptographic hash function like SHA-1, for example. - -\item[\settdx{ISABELLE_LATEX}, \settdx{ISABELLE_PDFLATEX}, - \settdx{ISABELLE_BIBTEX}, \settdx{ISABELLE_DVIPS}] refer to {\LaTeX} related - tools for Isabelle document preparation (see also \S\ref{sec:tool-latex}). - -\item[\settdx{ISABELLE_TOOLS}] is a colon separated list of directories that - are scanned by \texttt{isatool} for external utility programs (see also - \S\ref{sec:isatool}). - -\item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories with - documentation files. - -\item[\settdx{ISABELLE_DOC_FORMAT}] specifies the preferred document format, - typically \texttt{dvi} or \texttt{pdf}. - -\item[\settdx{DVI_VIEWER}] specifies the command to be used for displaying - \texttt{dvi} files. - -\item[\settdx{PDF_VIEWER}] specifies the command to be used for displaying - \texttt{pdf} files. - -\item[\settdx{PRINT_COMMAND}] specifies the standard printer spool command, - which is expected to accept \texttt{ps} files. - -\item[\settdx{ISABELLE_TMP_PREFIX}*] is the prefix from which any running - \texttt{isabelle} process derives an individual directory for temporary - files. The default is somewhere in \texttt{/tmp}. - -\item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the actual - user interface that the capital \texttt{Isabelle} or - \texttt{isabelle-interface} should invoke. See \S\ref{sec:interface} for - more details. - -\end{description} - - -\section{The Isabelle tools wrapper} \label{sec:isatool} - -All Isabelle related utilities are called via a common wrapper --- -\ttindex{isatool}: -\begin{ttbox} -Usage: isatool TOOL [ARGS ...] - - Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL - for more specific help. - - Available tools are: - - browser - Isabelle graph browser - \dots -\end{ttbox} -In principle, Isabelle tools are ordinary executable scripts that are run -within the Isabelle settings environment, see \S\ref{sec:settings}. The set -of available tools is collected by \texttt{isatool} from the directories -listed in the \texttt{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} - -Show the list of available documentation of the current Isabelle installation -like this: -\begin{ttbox} - isatool doc -\end{ttbox} - -View a certain document as follows: -\begin{ttbox} - isatool doc isar-ref -\end{ttbox} - -Create an Isabelle session derived from HOL (see also \S\ref{sec:tool-mkdir} -and \S\ref{sec:tool-make}): -\begin{ttbox} - isatool mkdir HOL Test && isatool make -\end{ttbox} -Note that \texttt{isatool mkdir} is usually only invoked once; existing -sessions (including document output etc.) are then updated by \texttt{isatool - make} alone. - - -\section{The raw Isabelle process} - -The \ttindex{isabelle} (or \ttindex{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 [OPTIONS] [INPUT] [OUTPUT] - - Options are: - -C tell ML system to copy output image - -I startup Isar interaction mode - -P startup Proof General interaction mode - -S secure mode -- disallow critical operations - -W startup process wrapper (interaction via external program) - -X startup PGIP interaction mode - -c tell ML system to compress output image - -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 -\texttt{ISABELLE_PATH} setting, which may consist of multiple components -separated by colons --- these are tried in the given order with the value of -\texttt{ML_IDENTIFIER} appended internally. In a similar way, base names are -relative to the directory specified by \texttt{ISABELLE_OUTPUT}. In any case, -actual file locations may also be given by including at least one slash -(\texttt{/}) in the name (hint: use \texttt{./} to refer to the current -directory). - - -\subsection*{Options} - -If the input heap file does not have write permission bits set, or the -\texttt{-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 40--80~MB). Users are responsible for -themselves to dispose their heap files when they are no longer needed. - -\medskip The \texttt{-w} option makes the output heap file read-only after -terminating. Thus subsequent invocations cause the logic image to be -read-only automatically. - -\medskip The \texttt{-c} option tells the underlying ML system to compress the -output heap (fully transparently). On Poly/ML for example, the image is -garbage collected and all stored values are maximally shared, resulting in up -to 50\% less disk space consumption. - -\medskip The \texttt{-C} option tells the ML system to produce a completely -self-contained output image, probably including a copy of the ML runtime -system itself. - -\medskip Using the \texttt{-e} option, arbitrary {\ML} code may be passed to -the Isabelle session from the command line. Multiple \texttt{-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 \texttt{-u} option is a shortcut for \texttt{-e} passing -``\texttt{use"ROOT.ML";}'' to the {\ML} session. The \texttt{-f} option -passes ``\texttt{Session.finish();}'', which is intended mainly for -administrative purposes. - -\medskip The \texttt{-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 \texttt{-e} texts). The \texttt{-q} option inhibits -interaction, thus providing a pure batch mode facility. - -\medskip The \texttt{-I} option makes Isabelle enter Isar interaction -mode on startup, instead of the primitive {\ML} top-level. The -\texttt{-P} option configures the top-level loop for interaction with -the Proof~General user interface, and the \texttt{-X} option enables -XML-based PGIP communication. The \texttt{-W} option makes Isabelle -enter a special process wrapper for interaction via an external -program; the protocol is a stripped-down version of Proof~General the -interaction mode. - -\medskip The \texttt{-S} option makes the Isabelle process more secure -by disabling some critical operations, notably runtime compilation and -evaluation of ML source code. - - -\subsection*{Examples} - -Run an interactive session of the default object-logic (as specified -by the \texttt{ISABELLE_LOGIC} setting) like this: -\begin{ttbox} -isabelle -\end{ttbox} -Usually \texttt{ISABELLE_LOGIC} refers to one of the standard logic -images, which are read-only by default. A writable session --- based -on \texttt{FOL}, but output to \texttt{Foo} (in the directory -specified by the \texttt{ISABELLE_OUTPUT} setting) --- may be invoked -as follows: -\begin{ttbox} -isabelle FOL Foo -\end{ttbox} -Ending this session normally (e.g.\ by typing control-D) dumps the whole {\ML} -system state into \texttt{Foo}. Be prepared for several tens of megabytes. - -The \texttt{Foo} session may be continued later (still in writable -state) by: -\begin{ttbox} -isabelle Foo -\end{ttbox} -A read-only \texttt{Foo} session may be started by: -\begin{ttbox} -isabelle -r Foo -\end{ttbox} - -\medskip Note that manual session management like this does \emph{not} provide -proper setup for theory presentation. This would require the \texttt{usedir} -utility, see \S\ref{sec:tool-usedir}. - -\bigskip The next example demonstrates batch execution of Isabelle. We print a -certain theorem of \texttt{FOL}: -\begin{ttbox} -isabelle -e "prth allE;" -q -r FOL -\end{ttbox} -Note that the output text will be interspersed with additional junk messages -by the {\ML} runtime environment. - - -\section{The Isabelle interface wrapper}\label{sec:interface} - -Isabelle is a generic theorem prover, even w.r.t.\ its user interface. The -\ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a -uniform way for end-users to invoke a certain interface; which one to start is -determined by the \settdx{ISABELLE_INTERFACE} setting variable, which should -give a full path specification to the actual executable. Also note that the -\texttt{install} utility provides some options to install desktop environment -icons (see \S\ref{sec:tool-install}). - -Presently, the most prominent Isabelle interface is -Proof~General~\cite{proofgeneral}\index{user interface!Proof General}. There -are separate versions for the raw ML top-level and the proper Isabelle/Isar -interpreter loop. The Proof~General distribution includes separate interface -wrapper scripts (in \texttt{ProofGeneral/isa} and \texttt{ProofGeneral/isar}) -for either of these. The canonical settings for Isabelle/Isar are as follows: -\begin{ttbox} -ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface -PROOFGENERAL_OPTIONS="" -\end{ttbox} -Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of -the Proof~General Lisp packages. There are some options available, such as -\texttt{-l} for passing the logic image to be used by default, or \texttt{-m} -to tune the standard print mode. The \texttt{-I} option allows to switch -between the Isar and ML view, independently of the interface script being -used. - -\medskip Note that the world may be also seen the other way round: Emacs may -be started first (with proper setup of Proof~General mode), and -\texttt{isabelle} run from within. This requires further Emacs Lisp -configuration, see the Proof~General documentation \cite{proofgeneral} for -more information. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "system" -%%% End: