doc-src/System/basics.tex
changeset 4540 24fcf5ecae88
parent 3278 636322bfd057
child 4547 3030c5b18580
equal deleted inserted replaced
4539:4227bd14dbe7 4540:24fcf5ecae88
    91   variable \texttt{ISABELLE_HOME_USER} has already been set before ---
    91   variable \texttt{ISABELLE_HOME_USER} has already been set before ---
    92   usually to \texttt{\~\relax/isabelle}.
    92   usually to \texttt{\~\relax/isabelle}.
    93   
    93   
    94   Thus individual users may override the site-wide defaults. See also
    94   Thus individual users may override the site-wide defaults. See also
    95   file \texttt{etc/user-settings.sample} in the distribution.
    95   file \texttt{etc/user-settings.sample} in the distribution.
    96   Typically, user settings should be a few lines only, just containing
    96   Typically, a user settings file would contain only a few lines, just
    97   the assigments that are really needed.  One should definitely
    97   the assigments that are really needed.  One should definitely
    98   \emph{not} start with a full copy the central
    98   \emph{not} start with a full copy the central
    99   \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very
    99   \texttt{\$ISABELLE_HOME/etc/settings}. This could cause very
   100   annoying maintainance problems later, when the Isabelle installation
   100   annoying maintainance problems later, when the Isabelle installation
   101   is updated or changed otherwise.
   101   is updated or changed otherwise.
   166   automatically.
   166   automatically.
   167   
   167   
   168 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
   168 \item[\settdx{ISABELLE_OUTPUT}*] is a directory where output heap
   169   files should be stored by default. The \texttt{ML_SYSTEM} identifier
   169   files should be stored by default. The \texttt{ML_SYSTEM} identifier
   170   is appended here, too.
   170   is appended here, too.
       
   171   
       
   172 \item[\settdx{ISABELLE_BROWSER_INFO}] is the directory where theory
       
   173   browser information (HTML and graph data) is stored (see also
       
   174   \S\ref{sec:info}).
   171 
   175 
   172 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
   176 \item[\settdx{ISABELLE_LOGIC}] specifies the default logic to load if
   173   none is given explicitely by the user --- e.g.\ when running
   177   none is given explicitely by the user --- e.g.\ when running
   174   \texttt{isabelle} directly, or some user interface.
   178   \texttt{isabelle} directly, or some user interface.
   175   
   179   
   193 \item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the
   197 \item[\settdx{ISABELLE_INSTALL_FONTS}] determines the way that the
   194   Isabelle symbol fonts are installed into your currently running X11
   198   Isabelle symbol fonts are installed into your currently running X11
   195   display server. X11 fonts are a non-trivial issue, see
   199   display server. X11 fonts are a non-trivial issue, see
   196   \S\ref{sec:tool-installfonts} for more information.
   200   \S\ref{sec:tool-installfonts} for more information.
   197   
   201   
       
   202 \item[\settdx{ISABELLE_TMP_PREFIX}] is the prefix from which any
       
   203   \texttt{isabelle} session derives an individual directory for
       
   204   temporary files.  The default value of \texttt{ISABELLE_TMP_PREFIX}
       
   205   is \texttt{/tmp/isabelle}; this should not need to be changed under
       
   206   normal circumstances.
       
   207   
   198 \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
   208 \item[\settdx{ISABELLE_INTERFACE}] is an identifier that specifies the
   199   actual user interface that the capital \texttt{Isabelle} should
   209   actual user interface that the capital \texttt{Isabelle} should
   200   invoke.  Currently available are \texttt{none}, \texttt{xterm} and
   210   invoke.  Currently available are \texttt{none}, \texttt{xterm} and
   201   \texttt{emacs}. See \S\ref{sec:interface} for more details.
   211   \texttt{emacs}. See \S\ref{sec:interface} for more details.
   202 
   212 
   215   Options are:
   225   Options are:
   216     -e MLTEXT    pass MLTEXT to the ML session
   226     -e MLTEXT    pass MLTEXT to the ML session
   217     -m MODE      add print mode for output
   227     -m MODE      add print mode for output
   218     -q           non-interactive session
   228     -q           non-interactive session
   219     -r           open heap file read-only
   229     -r           open heap file read-only
       
   230     -u           pass 'use"ROOT.ML";' to the ML session
       
   231     -w           reset write permissions on OUTPUT
   220 
   232 
   221   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
   233   INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
   222   These are either names to be searched in the Isabelle path, or actual
   234   These are either names to be searched in the Isabelle path, or actual
   223   file names (then containing at least one /).
   235   file names (containing at least one /).
   224   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   236   If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
   225 \end{ttbox}
   237 \end{ttbox}
   226 Input files without path specifications are looked up in the
   238 Input files without path specifications are looked up in the
   227 \texttt{ISABELLE_PATH} setting, which may consist of multiple
   239 \texttt{ISABELLE_PATH} setting, which may consist of multiple
   228 components separated by colons --- these are tried in order.
   240 components separated by colons --- these are tried in order.
   229 Likewise, short output names are relative to the directory specified
   241 Likewise, base names are relative to the directory specified by
   230 by \texttt{ISABELLE_OUTPUT}.  In any case, actual file locations may
   242 \texttt{ISABELLE_OUTPUT}.  In any case, actual file locations may also
   231 also be given by including at least one \texttt{/} in the name (hint:
   243 be given by including at least one \texttt{/} in the name (hint: use
   232 use \texttt{./} to refer to the current directory).
   244 \texttt{./} to refer to the current directory).
   233 
   245 
   234 
   246 
   235 \subsection*{Options}
   247 \subsection*{Options}
   236 
   248 
   237 If the input heap file does not have write permission bits set, or the
   249 If the input heap file does not have write permission bits set, or the
   244 The read-write state of sessions is determined at startup only, it
   256 The read-write state of sessions is determined at startup only, it
   245 cannot be changed intermediately. Also note that heap images may
   257 cannot be changed intermediately. Also note that heap images may
   246 require considerable amounts of disk space. Users are responsible
   258 require considerable amounts of disk space. Users are responsible
   247 themselves to dispose their heap files when they are no longer needed.
   259 themselves to dispose their heap files when they are no longer needed.
   248 
   260 
       
   261 \medskip The \texttt{-w} option makes the output heap file read-only
       
   262 after terminating the Isabelle session.  Thus subsequent invocations
       
   263 cause logic image to be read-only automatically.
       
   264 
   249 \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
   265 \medskip Using the \texttt{-e} option, arbitrary {\ML} code may be
   250 passed to the Isabelle session from the command line. Multiple
   266 passed to the Isabelle session from the command line. Multiple
   251 \texttt{-e}'s are evaluated in order. Strange things may happen when
   267 \texttt{-e}'s are evaluated in order. Strange things may happen when
   252 errorneous {\ML} code is given. Also make sure that commands are
   268 errorneous {\ML} code is given. Also make sure that commands are
   253 terminated properly by semicolon.
   269 terminated properly by semicolon.
   254 
   270 
       
   271 \medskip The \texttt{-u} option is a shortcut for \texttt{-e}, passing
       
   272 \texttt{use"ROOT.ML";} to the {\ML} session.
       
   273 
   255 \medskip The \texttt{-m} option adds identifiers of print modes to be
   274 \medskip The \texttt{-m} option adds identifiers of print modes to be
   256 made active for this session. Typically, this is used by some user
   275 made active for this session. Typically, this is used by some user
   257 interface, for example to enable output of mathematical symbols from a
   276 interface, for example to enable output of mathematical symbols from a
   258 special screen font.
   277 special screen font.
   259 
   278 
   288 \end{ttbox}
   307 \end{ttbox}
   289 A read-only \texttt{Foo} session may be started by:
   308 A read-only \texttt{Foo} session may be started by:
   290 \begin{ttbox}
   309 \begin{ttbox}
   291 isabelle -r Foo
   310 isabelle -r Foo
   292 \end{ttbox}
   311 \end{ttbox}
   293 One may also use something like \texttt{chmod~-w} on the logic image
       
   294 to have it read-only automatically.
       
   295 
   312 
   296 \medskip The next example demonstrates batch execution of Isabelle. We
   313 \medskip The next example demonstrates batch execution of Isabelle. We
   297 print a certain theorem of \texttt{FOL}:
   314 print a certain theorem of \texttt{FOL}:
   298 \begin{ttbox}
   315 \begin{ttbox}
   299 isabelle -e "prth allE;" -q -r FOL
   316 isabelle -e "prth allE;" -q -r FOL
   312   Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
   329   Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
   313   for more specific help.
   330   for more specific help.
   314 
   331 
   315   Available tools are:
   332   Available tools are:
   316 
   333 
       
   334     browser - Isabelle theory graph browser
   317     doc - view Isabelle documentation
   335     doc - view Isabelle documentation
   318     \(\vdots\)
   336     \dots
   319 \end{ttbox}
   337 \end{ttbox}
   320 Basically, Isabelle tools are ordinary executable scripts.  These are
   338 Basically, Isabelle tools are ordinary executable scripts.  These are
   321 run within the same settings environment as Isabelle proper, though,
   339 run within the same settings environment as Isabelle proper, see
   322 see \S\ref{sec:settings}.  The set of available tools is collected by
   340 \S\ref{sec:settings}.  The set of available tools is collected by
   323 isatool from the directories listed in the \texttt{ISABELLE_TOOLS}
   341 isatool from the directories listed in the \texttt{ISABELLE_TOOLS}
   324 setting.  Do not try to call the scripts directly. Neither should you
   342 setting.  Do not try to call the scripts directly. Neither should you
   325 add the tools directories to your shell's search path.
   343 add the tools directories to your shell's search path.
   326 
   344 
   327 
   345 
   339 setting variable. Currently, the following are recognized:
   357 setting variable. Currently, the following are recognized:
   340 \begin{ttdescription}
   358 \begin{ttdescription}
   341 \item[none] is just a pass-through to \texttt{isabelle}. Thus
   359 \item[none] is just a pass-through to \texttt{isabelle}. Thus
   342   \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
   360   \texttt{Isabelle} basically becomes an alias for \texttt{isabelle}.
   343   
   361   
   344 \item[xterm] refers to a simple xterm-based interface which is part of
   362 \item[xterm] refers to a simple xterm based interface which is part of
   345   the Isabelle distribution.
   363   the Isabelle distribution.
   346   
   364   
   347 \item[emacs] refers to David Aspinall's \emph{Isamode} for emacs.
   365 \item[emacs] refers to David Aspinall's \emph{Isamode} for emacs.
   348   Isabelle just provides a wrapper for this, the actual Isamode
   366   Isabelle just provides a wrapper for this, the actual Isamode
   349   distribution is available elsewhere.
   367   distribution is available elsewhere.