doc-src/System/basics.tex
 changeset 13047 f27cc0a43feb parent 12464 f9d3c92eae4d child 14933 3fd8c03e3ee6
equal inserted replaced
13046:69ab0e74ccda 13047:f27cc0a43feb
     2 % $Id$
     2 % $Id$
     3
     3
     4 \chapter{The Isabelle system environment}
     4 \chapter{The Isabelle system environment}
     5
     5
     6 This manual describes Isabelle together with related tools and user interfaces
     6 This manual describes Isabelle together with related tools and user interfaces
     7 as seen from an outside (system oriented) view.  See also the \emph{Isabelle
     7 as seen from an outside (system oriented) view.  See also the
     8   Isar Reference Manual}~\cite{isabelle-isar-ref} and the \emph{Isabelle
     8 \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} and the
     9   Reference Manual}~\cite{isabelle-ref} for the actual Isabelle commands and
     9 \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the actual Isabelle
    10 related functions.
    10 commands and related functions.
    11
    11
    12 \medskip The Isabelle system environment emerges from a few general concepts.
    12 \medskip The Isabelle system environment emerges from a few general concepts.
    13 \begin{itemize}
    13 \begin{itemize}
    14 \item The \emph{Isabelle settings mechanism} provides environment variables to
    14 \item The \emph{Isabelle settings mechanism} provides environment variables to
    15   all Isabelle programs (including tools and user interfaces).
    15   all Isabelle programs (including tools and user interfaces).
    24   \texttt{isabelle-interface}) provides some abstraction over the actual user
    24   \texttt{isabelle-interface}) provides some abstraction over the actual user
    25   interface to be used.  The de-facto standard interface for Isabelle is
    25   interface to be used.  The de-facto standard interface for Isabelle is
    26   Proof~General \cite{proofgeneral}.
    26   Proof~General \cite{proofgeneral}.
    27 \end{itemize}
    27 \end{itemize}
    28
    28
    29 \medskip The beginning user would probably just run a standard user interface
    29 \medskip The beginning user would probably just run the default user interface
    30 (by invoking the capital \texttt{Isabelle}).  This assumes that the system has
    30 (by invoking the capital \texttt{Isabelle}).  This assumes that the system has
    31 already been installed, of course.  In case you have to do this yourself, see
    31 already been installed, of course.  In case you have to do this yourself, see
    32 the \ttindex{INSTALL} file in the top-level directory of the distribution of
    32 the \ttindex{INSTALL} file in the top-level directory of the distribution of
    33 how to proceed; binary packages for various system components are available as
    33 how to proceed; binary packages for various system components are available as
    34 well.
    34 well.
    53 straight away.\footnote{Occasionally, users would still want to put the
    53 straight away.\footnote{Occasionally, users would still want to put the
    54   Isabelle \texttt{bin} directory into their shell's search path, but this is
    54   Isabelle \texttt{bin} directory into their shell's search path, but this is
    55   not required.}
    55   not required.}
    56
    56
    57
    57
    58 \subsection{Constructing the environment}
    58 \subsection{Building the environment}
    59
    59
    60 Whenever any of the Isabelle executables is run, their settings environment is
    60 Whenever any of the Isabelle executables is run, their settings environment is
    61 put together as follows.
    61 put together as follows.
    62
    62
    63 \begin{enumerate}
    63 \begin{enumerate}
    71   copy of the \texttt{bin} files will not work!
    71   copy of the \texttt{bin} files will not work!
    72
    72
    73 \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script  73 \item The file \texttt{\$ISABELLE_HOME/etc/settings} ist run as a shell script
    74   with the auto-export option for variables enabled.
    74   with the auto-export option for variables enabled.
    75
    75
    76   This file typically contains a rather long list of shell variable
    76   This file holds a rather long list of shell variable assigments, thus
    77   assigments, thus providing the site-wide default settings.  The Isabelle
    77   providing the site-wide default settings.  The Isabelle distribution already
    78   distribution already contains a global settings file with sensible defaults
    78   contains a global settings file with sensible defaults for most variables.
    79   for most variables. When installing the system, only a few of these may have
    79   When installing the system, only a few of these may have to be adapted
    80   to be adapted (probably \texttt{ML_SYSTEM} etc.).
    80   (probably \texttt{ML_SYSTEM} etc.).
    81
    81
    82 \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is  82 \item The file \texttt{\$ISABELLE_HOME_USER/etc/settings} (if it exists) is
    83   run in the same way as the site default settings. Note that the variable
    83   run in the same way as the site default settings. Note that the variable
    84   \texttt{ISABELLE_HOME_USER} has already been set before --- usually to
    84   \texttt{ISABELLE_HOME_USER} has already been set before --- usually to
    85   \texttt{\~\relax/isabelle}.
    85   \texttt{\~\relax/isabelle}.
   288
   288
   289 If the input heap file does not have write permission bits set, or the
   289 If the input heap file does not have write permission bits set, or the
   290 \texttt{-r} option is given explicitely, then the session started will be
   290 \texttt{-r} option is given explicitely, then the session started will be
   291 read-only.  That is, the {\ML} world cannot be committed back into the image
   291 read-only.  That is, the {\ML} world cannot be committed back into the image
   292 file.  Otherwise, a writable session enables commits into either the input
   292 file.  Otherwise, a writable session enables commits into either the input
   293 file, or into an alternative output heap file (in case that is given as the
   293 file, or into another output heap file (if that is given as the second
   294 second argument on the command line).
   294 argument on the command line).
   295
   295
   296 The read-write state of sessions is determined at startup only, it cannot be
   296 The read-write state of sessions is determined at startup only, it cannot be
   297 changed intermediately. Also note that heap images may require considerable
   297 changed intermediately. Also note that heap images may require considerable
   298 amounts of disk space (approximately 20--40~MB). Users are responsible for
   298 amounts of disk space (approximately 20--40~MB). Users are responsible for
   299 themselves to dispose their heap files when they are no longer needed.
   299 themselves to dispose their heap files when they are no longer needed.
   331 interaction, thus providing a pure batch mode facility.
   331 interaction, thus providing a pure batch mode facility.
   332
   332
   333 \medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
   333 \medskip The \texttt{-I} option makes Isabelle enter Isar interaction mode on
   334 startup, instead of the primitive {\ML} top-level.  The \texttt{-P} option
   334 startup, instead of the primitive {\ML} top-level.  The \texttt{-P} option
   335 configures the top-level loop for interaction with the Proof~General user
   335 configures the top-level loop for interaction with the Proof~General user
   336 interface; do not enable this in ordinary sessions.
   336 interface; do not enable this in plain TTY sessions.
   337
   337
   338
   338
   339 \subsection*{Examples}
   339 \subsection*{Examples}
   340
   340
   341 Run an interactive session of the default object-logic (as specified
   341 Run an interactive session of the default object-logic (as specified
   379
   379
   380 \section{The Isabelle interface wrapper}\label{sec:interface}
   380 \section{The Isabelle interface wrapper}\label{sec:interface}
   381
   381
   382 Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
   382 Isabelle is a generic theorem prover, even w.r.t.\ its user interface.  The
   383 \ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
   383 \ttindex{Isabelle} (or \ttindex{isabelle-interface}) executable provides a
   384 uniform way for end-users to invoke a certain interface; which one to start
   384 uniform way for end-users to invoke a certain interface; which one to start is
   385 actually is determined by the \settdx{ISABELLE_INTERFACE} setting variable.
   385 determined by the \settdx{ISABELLE_INTERFACE} setting variable.  Also note
   386 Also note that the \texttt{install} utility provides some options to install
   386 that the \texttt{install} utility provides some options to install desktop
   387 desktop environment icons as well (see \S\ref{sec:tool-install}).
   387 environment icons as well (see \S\ref{sec:tool-install}).
   388
   388
   389 An interface may be specified either by giving an identifier that the Isabelle
   389 An interface may be specified either by giving an identifier that the Isabelle
   390 distribution knows about, or by specifying an actual path name (containing a
   390 distribution knows about, or by specifying an actual path name (containing a
   391 slash \texttt{/}'') of some executable.  Currently, the following interfaces
   391 slash \texttt{/}'') of some executable.  Currently, the following interfaces
   392 are available:
   392 are available:
   414   \end{ttbox}
   414   \end{ttbox}
   415   Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
   415   Thus \texttt{Isabelle} would automatically invoke Emacs with proper setup of
   416   the Proof~General Lisp packages.  There are some options available, such as
   416   the Proof~General Lisp packages.  There are some options available, such as
   417   \texttt{-l} for passing the logic image to be used by default, or
   417   \texttt{-l} for passing the logic image to be used by default, or
   418   \texttt{-m} to tune the standard print mode.  The \texttt{-I} option allows
   418   \texttt{-m} to tune the standard print mode.  The \texttt{-I} option allows
   419   to switch between the Isar and ML view, independently of the actual
   419   to switch between the Isar and ML view, independently of the interface
   420   interface script being used.
   420   script being used.
   421
   421
   422   \medskip Note that the world may be also seen the other way round: Emacs may
   422   \medskip Note that the world may be also seen the other way round: Emacs may
   423   be started first (with proper setup of Proof~General mode), and
   423   be started first (with proper setup of Proof~General mode), and
   424   \texttt{isabelle} run from within.  This requires further Emacs Lisp
   424   \texttt{isabelle} run from within.  This requires further Emacs Lisp
   425   configuration, see the Proof~General documentation \cite{proofgeneral} for
   425   configuration, see the Proof~General documentation \cite{proofgeneral} for