doc-src/System/basics.tex
 changeset 3262 7115da553895 parent 3217 d30d62128fe5 child 3278 636322bfd057
equal inserted replaced
3261:8fe63a9cd0c7 3262:7115da553895
     1
     1
     2 % $Id$
     2 % $Id$
     3
     3
     4 \chapter{Basic concepts}
     4 \chapter{Basic concepts}
     5
     5
     6 The \emph{Isabelle System Manual} describes Isabelle together with its
     6 The \emph{Isabelle System Manual} describes Isabelle together with
     7 related tools and user interfaces --- as seen from an outside
     7 related tools and user interfaces as seen from an outside (operating
     8 (operating system oriented) view.  See the \emph{Isabelle Reference
     8 system oriented) view.  See the \emph{Isabelle Reference Manual} for
     9   Manual} for all internal {\ML} level user commands, on the other
     9 all internal {\ML} level user commands, on the other hand.
    10 hand.

    11
    10
    12 \medskip The Isabelle system level environment is based on a few
    11 \medskip The Isabelle system level environment is based on a few
    13 general concepts:
    12 general concepts:
    14 \begin{itemize}
    13 \begin{itemize}
    15 \item The \emph{Isabelle settings mechanism}, which provides
    14 \item The \emph{Isabelle settings mechanism}, which provides
    29   provides some abstraction over the actual user interface to be used.
    28   provides some abstraction over the actual user interface to be used.
    30 \end{itemize}
    29 \end{itemize}
    31
    30
    32 \medskip The beginning user would probably just run one of the
    31 \medskip The beginning user would probably just run one of the
    33 interfaces (by invoking the capital \texttt{Isabelle}), and maybe some
    32 interfaces (by invoking the capital \texttt{Isabelle}), and maybe some
    34 basic other tools like \texttt{doc} (see \S\ref{sec:tool-doc}).  This
    33 basic tools like \texttt{doc} (see \S\ref{sec:tool-doc}).  This
    35 assumes that the system has already been installed properly, of
    34 assumes that the system has already been installed properly, of
    36 course.\footnote{In case you have to do this yourself from scratch,
    35 course.\footnote{In case you have to do this yourself, see the
    37   see the \ttindex{INSTALL} file in the top-level directory of the
    36   \ttindex{INSTALL} file in the top-level directory of the
    38   distribution. The information provided there should be sufficient as
    37   distribution. The information provided there should be sufficient as
    39   a start.}
    38   a start.}
    40
    39
    41
    40
    42 \section{Isabelle settings} \label{sec:settings}
    41 \section{Isabelle settings} \label{sec:settings}
    48 intended to be set directly from the shell!
    47 intended to be set directly from the shell!
    49
    48
    50 Isabelle employs a somewhat more sophisticated scheme of
    49 Isabelle employs a somewhat more sophisticated scheme of
    51 \emph{settings files} --- one for site-wide defaults, another for
    50 \emph{settings files} --- one for site-wide defaults, another for
    52 optional user-specific modifications.  With all configuration
    51 optional user-specific modifications.  With all configuration
    53 variables in only one or two places, this is considered much more
    52 variables in just a few places, this is considered much more
    54 maintainable and user-friendly than ordinary shell environment
    53 maintainable and user-friendly than ordinary shell environment
    55 variables.
    54 variables.
    56
    55
    57 In particular, we avoid the typical situation where prospective users
    56 In particular, we avoid the typical situation where prospective users
    58 of a software package are told to put this and that in their shell
    57 of a software package are told to put this and that in their shell
    62 shell's search path, of course.
    61 shell's search path, of course.
    63
    62
    64
    63
    65 \subsection{Building the environment}
    64 \subsection{Building the environment}
    66
    65
    67 Whenever any of the Isabelle executables is run, theri settings
    66 Whenever any of the Isabelle executables is run, their settings
    68 environment is built as follows:
    67 environment is built as follows:
    69
    68
    70 \begin{enumerate}
    69 \begin{enumerate}
    71 \item The special variable \settdx{ISABELLE_HOME} is determined
    70 \item The special variable \settdx{ISABELLE_HOME} is determined
    72   automatically from the location of the binary that has been run.
    71   automatically from the location of the binary that has been run.
    92   usually to \texttt{\~\relax/isabelle}.
    91   usually to \texttt{\~\relax/isabelle}.
    93
    92
    94   Thus individual users may override the site-wide defaults. See also
    93   Thus individual users may override the site-wide defaults. See also
    95   file \texttt{etc/user-settings.sample} in the distribution.
    94   file \texttt{etc/user-settings.sample} in the distribution.
    96   Typically, user settings are a few lines only, just containing the
    95   Typically, user settings are a few lines only, just containing the
    97   assigments that are really required.  One should definitely
    96   assigments that are really needed.  One should definitely \emph{not}
    98   \emph{not} start with a full copy the central
    97   start with a full copy the central
    99   \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very anoying  98 \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very
   100   maintainance problems later, when the Isabelle installation is
    99   annoying maintainance problems later, when the Isabelle installation
   101   updated or changed otherwise.
   100   is updated or changed otherwise.
   102
   101
   103 \end{enumerate}
   102 \end{enumerate}
   104
   103
   105 Note that settings files are actually full GNU bash scripts. So one
   104 Note that settings files are actually full GNU bash scripts. So one
   106 may use complex shell commands, say \texttt{if} or \texttt{case}
   105 may use complex shell commands, say \texttt{if} or \texttt{case}
   164   colons) where Isabelle logic images may reside. Note that the
   163   colons) where Isabelle logic images may reside. Note that the
   165   \texttt{ML_SYSTEM} identifier is appended to each component
   164   \texttt{ML_SYSTEM} identifier is appended to each component
   166   automatically.
   165   automatically.
   167
   166
   168 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
   167 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
   169   files should be stored. The \texttt{ML_SYSTEM} identifier is
   168   files should be stored by default. The \texttt{ML_SYSTEM} identifier
   170   appended here, too.
   169   is appended here, too.
   171
   170
   172 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
   171 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
   173   none is given explicitely by the user --- e.g.\ when running
   172   none is given explicitely by the user --- e.g.\ when running
   174   \texttt{isabelle} directly, or some user interface.
   173   \texttt{isabelle} directly, or some user interface.
   175
   174
   184   directories that are scanned by \texttt{isatool} for utility
   183   directories that are scanned by \texttt{isatool} for utility
   185   programs (see also \S\ref{sec:isatool}).
   184   programs (see also \S\ref{sec:isatool}).
   186
   185
   187 \item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories
   186 \item[\settdx{ISABELLE_DOCS}] is a colon separated list of directories
   188   with documentation files.
   187   with documentation files.
   189
   188
   190 \item[\settdx{DVI_VIEWER}] specifies the program to be used for
   189 \item[\settdx{DVI_VIEWER}] specifies the command to be used for
   191   displaying \texttt{dvi} files.
   190   displaying \texttt{dvi} files.
   192
   191
   193 \item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the
   192 \item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the
   194   Isabelle symbol fonts are installed into your running X11 display
   193   Isabelle symbol fonts are installed into your currently running X11
   195   server. X11 fonts are a non-trivial issue, see \S\ref{sec:fonts} for
   194   display server. X11 fonts are a non-trivial issue, see
   196   more information.
   195   \S\ref{sec:tool-installfonts} for more information.
   197
   196
   198 \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
   197 \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
   199   actual user interface that the capital \texttt{Isabelle} should
   198   actual user interface that the capital \texttt{Isabelle} should
   200   invoke.  Currently available are \texttt{none}, \texttt{xterm} and
   199   invoke.  Currently available are \texttt{none}, \texttt{xterm} and
   201   \texttt{emacs}. See \S\ref{sec:interface} for more details.
   200   \texttt{emacs}. See \S\ref{sec:interface} for more details.
   226 Input files without path specifications are looked up in the
   225 Input files without path specifications are looked up in the
   227 \texttt{ISABELLE_PATH} setting, which may consist of multiple
   226 \texttt{ISABELLE_PATH} setting, which may consist of multiple
   228 components separated by colons --- these are tried in order.  Short
   227 components separated by colons --- these are tried in order.  Short
   229 output names are relative to the directory specified by
   228 output names are relative to the directory specified by
   230 \texttt{ISABELLE_OUTPUT} setting.  In any case, actual file locations
   229 \texttt{ISABELLE_OUTPUT} setting.  In any case, actual file locations
   231 could also be given by including at least one \texttt{/} in the name
   230 may also be given by including at least one \texttt{/} in the name
   232 (use \texttt{./} to refer to the current directory).
   231 (hint: use \texttt{./} to refer to the current directory).
   233
   232
   234
   233
   235 \subsection*{Options}
   234 \subsection*{Options}
   236
   235
   237 If the input heap file does not have write permission bits set, or the
   236 If the input heap file does not have write permission bits set, or the
   246 require considerable amounts of disk space. Users are responsible
   245 require considerable amounts of disk space. Users are responsible
   247 themselves to dispose their heap files when they are no longer needed.
   246 themselves to dispose their heap files when they are no longer needed.
   248
   247
   249 \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
   248 \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
   250 passed to the Isabelle session from the command line. Multiple
   249 passed to the Isabelle session from the command line. Multiple
   251 \texttt{-e}'s are evaluated in the given order. Strange things may
   250 \texttt{-e}'s are evaluated in order. Strange things may happen when
   252 happen when errorneous {\ML} code is supplied. Also make sure that
   251 errorneous {\ML} code is given. Also make sure that commands are
   253 commands are terminated properly by semicolon.
   252 terminated properly by semicolon.
   254
   253
   255 \medskip The \texttt{-m} option adds identifiers of print modes that
   254 \medskip The \texttt{-m} option adds identifiers of print modes to be
   256 are to be made active for this session. Typically this is used by some
   255 made active for this session. Typically, this is used by some user
   257 user interface, for example to enable output of mathematical symbols
   256 interface, for example to enable output of mathematical symbols from a
   258 from a special screen font. See also \S\ref{sec:tool-installfonts}
   257 special screen font. See also \S\ref{sec:tool-installfonts} about
   259 about fonts and the \emph{Isabelle Reference Manual} about print modes
   258 fonts and the \emph{Isabelle Reference Manual} about print modes in
   260 in general.
   259 general.
   261
   260
   262 \medskip Isabelle normally enters an interactice {\ML} top-level loop
   261 \medskip Isabelle normally enters an interactice {\ML} top-level loop
   263 (after processing the \texttt{-e} texts). The \texttt{-q} option
   262 (after processing the \texttt{-e} texts). The \texttt{-q} option
   264 inhibits this, thus providing a pure batch mode facility.
   263 inhibits this, thus providing a pure batch mode facility.
   265
   264
   282 Ending this session normally (e.g.\ by typing control-D) dumps the
   281 Ending this session normally (e.g.\ by typing control-D) dumps the
   283 whole {\ML} system state into \texttt{Foo}. Be prepared for several
   282 whole {\ML} system state into \texttt{Foo}. Be prepared for several
   284 megabytes!
   283 megabytes!
   285
   284
   286 The \texttt{Foo} session may be continued later (still in writable
   285 The \texttt{Foo} session may be continued later (still in writable
   287 state) at exactly the same point:
   286 state) by:
   288 \begin{ttbox}
   287 \begin{ttbox}
   289 isabelle Foo
   288 isabelle Foo
   290 \end{ttbox}
   289 \end{ttbox}
   291 A read-only \texttt{Foo} session may be started by:
   290 A read-only \texttt{Foo} session may be started by:
   292 \begin{ttbox}
   291 \begin{ttbox}