doc-src/System/Thy/Basics.thy
author wenzelm
Mon Sep 15 19:43:10 2008 +0200 (2008-09-15 ago)
changeset 28223 eee194395fdc
parent 28215 a1cfc43ac47d
child 28238 398bf960d3d4
permissions -rw-r--r--
tuned;
wenzelm@28215
     1
(* $Id$ *)
wenzelm@28215
     2
wenzelm@28215
     3
theory Basics
wenzelm@28215
     4
imports Pure
wenzelm@28215
     5
begin
wenzelm@28215
     6
wenzelm@28215
     7
chapter {* The Isabelle system environment *}
wenzelm@28215
     8
wenzelm@28215
     9
text {*
wenzelm@28215
    10
  This manual describes Isabelle together with related tools and user
wenzelm@28215
    11
  interfaces as seen from an outside (system oriented) view.  See also
wenzelm@28215
    12
  the \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref}
wenzelm@28215
    13
  and the \emph{Isabelle Reference Manual}~\cite{isabelle-ref} for the
wenzelm@28215
    14
  actual Isabelle commands and related functions.
wenzelm@28215
    15
wenzelm@28215
    16
  \medskip The Isabelle system environment emerges from a few general
wenzelm@28215
    17
  concepts.
wenzelm@28215
    18
wenzelm@28215
    19
  \begin{itemize}
wenzelm@28215
    20
wenzelm@28223
    21
  \item The \emph{Isabelle settings mechanism} provides environment
wenzelm@28223
    22
  variables to all Isabelle programs (including tools and user
wenzelm@28223
    23
  interfaces).
wenzelm@28215
    24
wenzelm@28215
    25
  \item The \emph{Isabelle tools wrapper} (@{executable_def isatool})
wenzelm@28215
    26
  provides a generic startup platform for Isabelle related utilities.
wenzelm@28215
    27
  Thus tools automatically benefit from the settings mechanism.
wenzelm@28215
    28
wenzelm@28215
    29
  \item The raw \emph{Isabelle process} (@{executable_def isabelle} or
wenzelm@28215
    30
  @{executable_def "isabelle-process"}) runs logic sessions either
wenzelm@28215
    31
  interactively or in batch mode.  In particular, this view abstracts
wenzelm@28215
    32
  over the invocation of the actual ML system to be used.
wenzelm@28215
    33
wenzelm@28215
    34
  \item The \emph{Isabelle interface wrapper} (@{executable_def
wenzelm@28215
    35
  Isabelle} or @{executable_def "isabelle-interface"}) provides some
wenzelm@28215
    36
  abstraction over the actual user interface to be used.  The de-facto
wenzelm@28215
    37
  standard interface for Isabelle is Proof~General
wenzelm@28215
    38
  \cite{proofgeneral}.
wenzelm@28215
    39
wenzelm@28215
    40
  \end{itemize}
wenzelm@28215
    41
wenzelm@28215
    42
  \medskip The beginning user would probably just run the default user
wenzelm@28215
    43
  interface (by invoking the capital @{executable Isabelle}).  This
wenzelm@28215
    44
  assumes that the system has already been installed, of course.  In
wenzelm@28215
    45
  case you have to do this yourself, see the @{verbatim INSTALL} file
wenzelm@28215
    46
  in the top-level directory of the distribution of how to proceed;
wenzelm@28215
    47
  binary packages for various system components are available as well.
wenzelm@28215
    48
*}
wenzelm@28215
    49
wenzelm@28215
    50
wenzelm@28215
    51
section {* Isabelle settings \label{sec:settings} *}
wenzelm@28215
    52
wenzelm@28215
    53
text {*
wenzelm@28215
    54
  The Isabelle system heavily depends on the \emph{settings
wenzelm@28215
    55
  mechanism}\indexbold{settings}.  Essentially, this is a statically
wenzelm@28215
    56
  scoped collection of environment variables, such as @{setting
wenzelm@28215
    57
  ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
wenzelm@28215
    58
  variables are \emph{not} intended to be set directly from the shell,
wenzelm@28215
    59
  though.  Isabelle employs a somewhat more sophisticated scheme of
wenzelm@28215
    60
  \emph{settings files} --- one for site-wide defaults, another for
wenzelm@28215
    61
  additional user-specific modifications.  With all configuration
wenzelm@28215
    62
  variables in at most two places, this scheme is more maintainable
wenzelm@28215
    63
  and user-friendly than global shell environment variables.
wenzelm@28215
    64
wenzelm@28215
    65
  In particular, we avoid the typical situation where prospective
wenzelm@28215
    66
  users of a software package are told to put several things into
wenzelm@28215
    67
  their shell startup scripts, before being able to actually run the
wenzelm@28215
    68
  program. Isabelle requires none such administrative chores of its
wenzelm@28215
    69
  end-users --- the executables can be invoked straight away.
wenzelm@28215
    70
  Occasionally, users would still want to put the Isabelle @{verbatim
wenzelm@28215
    71
  bin} directory into their shell's search path, but this is not
wenzelm@28215
    72
  required.
wenzelm@28215
    73
*}
wenzelm@28215
    74
wenzelm@28215
    75
wenzelm@28215
    76
subsection {* Building the environment *}
wenzelm@28215
    77
wenzelm@28215
    78
text {*
wenzelm@28215
    79
  Whenever any of the Isabelle executables is run, their settings
wenzelm@28215
    80
  environment is put together as follows.
wenzelm@28215
    81
wenzelm@28215
    82
  \begin{enumerate}
wenzelm@28215
    83
wenzelm@28215
    84
  \item The special variable @{setting_def ISABELLE_HOME} is
wenzelm@28215
    85
  determined automatically from the location of the binary that has
wenzelm@28215
    86
  been run.
wenzelm@28215
    87
  
wenzelm@28215
    88
  You should not try to set @{setting ISABELLE_HOME} manually. Also
wenzelm@28215
    89
  note that the Isabelle executables either have to be run from their
wenzelm@28215
    90
  original location in the distribution directory, or via the
wenzelm@28215
    91
  executable objects created by the @{tool install} utility (see
wenzelm@28215
    92
  \secref{sec:tool-install}).  Just doing a plain copy of the
wenzelm@28215
    93
  @{verbatim bin} files will not work!
wenzelm@28215
    94
  
wenzelm@28215
    95
  \item The file @{verbatim "$ISABELLE_HOME/etc/settings"} ist run as
wenzelm@28215
    96
  a shell script with the auto-export option for variables enabled.
wenzelm@28215
    97
  
wenzelm@28215
    98
  This file holds a rather long list of shell variable assigments,
wenzelm@28215
    99
  thus providing the site-wide default settings.  The Isabelle
wenzelm@28215
   100
  distribution already contains a global settings file with sensible
wenzelm@28215
   101
  defaults for most variables.  When installing the system, only a few
wenzelm@28215
   102
  of these may have to be adapted (probably @{setting ML_SYSTEM}
wenzelm@28215
   103
  etc.).
wenzelm@28215
   104
  
wenzelm@28215
   105
  \item The file @{verbatim "$ISABELLE_HOME_USER/etc/settings"} (if it
wenzelm@28215
   106
  exists) is run in the same way as the site default settings. Note
wenzelm@28215
   107
  that the variable @{setting ISABELLE_HOME_USER} has already been set
wenzelm@28215
   108
  before --- usually to @{verbatim "~/isabelle"}.
wenzelm@28215
   109
  
wenzelm@28215
   110
  Thus individual users may override the site-wide defaults.  See also
wenzelm@28215
   111
  file @{verbatim "etc/user-settings.sample"} in the distribution.
wenzelm@28215
   112
  Typically, a user settings file would contain only a few lines, just
wenzelm@28215
   113
  the assigments that are really changed.  One should definitely
wenzelm@28215
   114
  \emph{not} start with a full copy the basic @{verbatim
wenzelm@28215
   115
  "$ISABELLE_HOME/etc/settings"}. This could cause very annoying
wenzelm@28215
   116
  maintainance problems later, when the Isabelle installation is
wenzelm@28215
   117
  updated or changed otherwise.
wenzelm@28215
   118
  
wenzelm@28215
   119
  \end{enumerate}
wenzelm@28215
   120
wenzelm@28215
   121
  Note that settings files are actually full GNU bash scripts. So one
wenzelm@28215
   122
  may use complex shell commands, such as @{verbatim "if"} or
wenzelm@28215
   123
  @{verbatim "case"} statements to set variables depending on the
wenzelm@28215
   124
  system architecture or other environment variables.  Such advanced
wenzelm@28215
   125
  features should be added only with great care, though. In
wenzelm@28215
   126
  particular, external environment references should be kept at a
wenzelm@28215
   127
  minimum.
wenzelm@28215
   128
wenzelm@28215
   129
  \medskip A few variables are somewhat special:
wenzelm@28215
   130
wenzelm@28215
   131
  \begin{itemize}
wenzelm@28215
   132
wenzelm@28215
   133
  \item @{setting_def ISABELLE} and @{setting_def ISATOOL} are set
wenzelm@28215
   134
  automatically to the absolute path names of the @{executable
wenzelm@28215
   135
  "isabelle-process"} and @{executable isatool} executables,
wenzelm@28215
   136
  respectively.
wenzelm@28215
   137
  
wenzelm@28215
   138
  \item @{setting_def ISABELLE_OUTPUT} will have the identifiers of
wenzelm@28215
   139
  the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
wenzelm@28215
   140
  the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
wenzelm@28215
   141
  to its value.
wenzelm@28215
   142
wenzelm@28215
   143
  \end{itemize}
wenzelm@28215
   144
wenzelm@28215
   145
  \medskip The Isabelle settings scheme is conceptually simple, but
wenzelm@28215
   146
  not completely trivial.  For debugging purposes, the resulting
wenzelm@28215
   147
  environment may be inspected with the @{tool getenv} utility, see
wenzelm@28215
   148
  \secref{sec:tool-getenv}.
wenzelm@28215
   149
*}
wenzelm@28215
   150
wenzelm@28215
   151
wenzelm@28215
   152
subsection{* Common variables *}
wenzelm@28215
   153
wenzelm@28215
   154
text {*
wenzelm@28215
   155
  This is a reference of common Isabelle settings variables. Note that
wenzelm@28215
   156
  the list is somewhat open-ended. Third-party utilities or interfaces
wenzelm@28215
   157
  may add their own selection. Variables that are special in some
wenzelm@28215
   158
  sense are marked with @{text "\<^sup>*"}.
wenzelm@28215
   159
wenzelm@28215
   160
  \begin{description}
wenzelm@28215
   161
wenzelm@28215
   162
  \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the
wenzelm@28215
   163
  location of the top-level Isabelle distribution directory. This is
wenzelm@28215
   164
  automatically determined from the Isabelle executable that has been
wenzelm@28215
   165
  invoked.  Do not attempt to set @{setting ISABELLE_HOME} yourself
wenzelm@28215
   166
  from the shell.
wenzelm@28215
   167
  
wenzelm@28215
   168
  \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
wenzelm@28215
   169
  counterpart of @{setting ISABELLE_HOME}. The default value is
wenzelm@28215
   170
  @{verbatim "~/isabelle"}, under rare circumstances this may be
wenzelm@28215
   171
  changed in the global setting file.  Typically, the @{setting
wenzelm@28215
   172
  ISABELLE_HOME_USER} directory mimics @{setting ISABELLE_HOME} to
wenzelm@28215
   173
  some extend. In particular, site-wide defaults may be overridden by
wenzelm@28215
   174
  a private @{verbatim "etc/settings"}.
wenzelm@28215
   175
  
wenzelm@28215
   176
  \item[@{setting_def ISABELLE}@{text "\<^sup>*"}, @{setting
wenzelm@28215
   177
  ISATOOL}@{text "\<^sup>*"}] are automatically set to the full path
wenzelm@28215
   178
  names of the @{executable "isabelle-process"} and @{executable
wenzelm@28215
   179
  isatool} executables, respectively.  Thus other tools and scripts
wenzelm@28215
   180
  need not assume that the Isabelle @{verbatim bin} directory is on
wenzelm@28215
   181
  the current search path of the shell.
wenzelm@28215
   182
  
wenzelm@28215
   183
  \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
wenzelm@28215
   184
  to the name of this Isabelle distribution, e.g.\ ``@{verbatim
wenzelm@28215
   185
  Isabelle2008}''.
wenzelm@28215
   186
wenzelm@28215
   187
  \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
wenzelm@28215
   188
  @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
wenzelm@28215
   189
  ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
wenzelm@28215
   190
  to be used for Isabelle.  There is only a fixed set of admissable
wenzelm@28215
   191
  @{setting ML_SYSTEM} names (see the @{verbatim "etc/settings"} file
wenzelm@28215
   192
  of the distribution).
wenzelm@28215
   193
  
wenzelm@28215
   194
  The actual compiler binary will be run from the directory @{setting
wenzelm@28215
   195
  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
wenzelm@28215
   196
  command line.  The optional @{setting ML_PLATFORM} may specify the
wenzelm@28215
   197
  binary format of ML heap images, which is useful for cross-platform
wenzelm@28215
   198
  installations.  The value of @{setting ML_IDENTIFIER} is
wenzelm@28215
   199
  automatically obtained by composing the values of @{setting
wenzelm@28215
   200
  ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
wenzelm@28215
   201
  
wenzelm@28215
   202
  \item[@{setting_def ISABELLE_PATH}] is a list of directories
wenzelm@28215
   203
  (separated by colons) where Isabelle logic images may reside.  When
wenzelm@28215
   204
  looking up heaps files, the value of @{setting ML_IDENTIFIER} is
wenzelm@28215
   205
  appended to each component internally.
wenzelm@28215
   206
  
wenzelm@28215
   207
  \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
wenzelm@28215
   208
  directory where output heap files should be stored by default. The
wenzelm@28215
   209
  ML system and Isabelle version identifier is appended here, too.
wenzelm@28215
   210
  
wenzelm@28215
   211
  \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
wenzelm@28215
   212
  theory browser information (HTML text, graph data, and printable
wenzelm@28215
   213
  documents) is stored (see also \secref{sec:info}).  The default
wenzelm@28215
   214
  value is @{verbatim "$ISABELLE_HOME_USER/browser_info"}.
wenzelm@28215
   215
  
wenzelm@28215
   216
  \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
wenzelm@28215
   217
  load if none is given explicitely by the user.  The default value is
wenzelm@28215
   218
  @{verbatim HOL}.
wenzelm@28215
   219
  
wenzelm@28215
   220
  \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the default
wenzelm@28215
   221
  line editor for @{verbatim "isatool tty"} (see also
wenzelm@28215
   222
  \secref{sec:tool-tty}).
wenzelm@28215
   223
wenzelm@28215
   224
  \item[@{setting_def ISABELLE_USEDIR_OPTIONS}] is implicitly prefixed
wenzelm@28215
   225
  to the command line of any @{verbatim "isatool usedir"} invocation
wenzelm@28215
   226
  (see also \secref{sec:tool-usedir}). This typically contains
wenzelm@28215
   227
  compilation options for object-logics --- @{tool usedir} is the
wenzelm@28215
   228
  basic utility for managing logic sessions (cf.\ the @{verbatim
wenzelm@28215
   229
  IsaMakefile}s in the distribution).
wenzelm@28215
   230
wenzelm@28215
   231
  \item[@{setting_def ISABELLE_FILE_IDENT}] specifies a shell command
wenzelm@28215
   232
  for producing a source file identification, based on the actual
wenzelm@28215
   233
  content instead of the full physical path and date stamp (which is
wenzelm@28215
   234
  the default). A typical identification would produce a ``digest'' of
wenzelm@28215
   235
  the text, using a cryptographic hash function like SHA-1, for
wenzelm@28215
   236
  example.
wenzelm@28215
   237
  
wenzelm@28215
   238
  \item[@{setting_def ISABELLE_LATEX}, @{setting_def
wenzelm@28215
   239
  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}, @{setting_def
wenzelm@28215
   240
  ISABELLE_DVIPS}] refer to {\LaTeX} related tools for Isabelle
wenzelm@28215
   241
  document preparation (see also \secref{sec:tool-latex}).
wenzelm@28215
   242
  
wenzelm@28215
   243
  \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
wenzelm@28215
   244
  directories that are scanned by @{executable isatool} for external
wenzelm@28215
   245
  utility programs (see also \secref{sec:isatool}).
wenzelm@28215
   246
  
wenzelm@28215
   247
  \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
wenzelm@28215
   248
  directories with documentation files.
wenzelm@28215
   249
  
wenzelm@28215
   250
  \item[@{setting_def ISABELLE_DOC_FORMAT}] specifies the preferred
wenzelm@28215
   251
  document format, typically @{verbatim dvi} or @{verbatim pdf}.
wenzelm@28215
   252
  
wenzelm@28215
   253
  \item[@{setting_def DVI_VIEWER}] specifies the command to be used
wenzelm@28215
   254
  for displaying @{verbatim dvi} files.
wenzelm@28215
   255
  
wenzelm@28215
   256
  \item[@{setting_def PDF_VIEWER}] specifies the command to be used
wenzelm@28215
   257
  for displaying @{verbatim pdf} files.
wenzelm@28215
   258
  
wenzelm@28215
   259
  \item[@{setting_def PRINT_COMMAND}] specifies the standard printer
wenzelm@28215
   260
  spool command, which is expected to accept @{verbatim ps} files.
wenzelm@28215
   261
  
wenzelm@28215
   262
  \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
wenzelm@28215
   263
  prefix from which any running @{executable isabelle} process derives
wenzelm@28215
   264
  an individual directory for temporary files.  The default is
wenzelm@28215
   265
  somewhere in @{verbatim "/tmp"}.
wenzelm@28215
   266
  
wenzelm@28215
   267
  \item[@{setting_def ISABELLE_INTERFACE}] is an identifier that
wenzelm@28215
   268
  specifies the actual user interface that the capital @{executable
wenzelm@28215
   269
  Isabelle} or @{executable "isabelle-interface"} should invoke.  See
wenzelm@28215
   270
  \secref{sec:interface} for more details.
wenzelm@28215
   271
wenzelm@28215
   272
  \end{description}
wenzelm@28215
   273
*}
wenzelm@28215
   274
wenzelm@28215
   275
wenzelm@28215
   276
section {* The Isabelle tools wrapper \label{sec:isatool} *}
wenzelm@28215
   277
wenzelm@28215
   278
text {*
wenzelm@28215
   279
  All Isabelle related utilities are called via a common wrapper ---
wenzelm@28223
   280
  @{executable isatool}:
wenzelm@28215
   281
wenzelm@28215
   282
\begin{ttbox}
wenzelm@28215
   283
Usage: isatool TOOL [ARGS ...]
wenzelm@28215
   284
wenzelm@28215
   285
  Start Isabelle utility program TOOL with ARGS. Pass "-?" to TOOL
wenzelm@28215
   286
  for more specific help.
wenzelm@28215
   287
wenzelm@28215
   288
  Available tools are:
wenzelm@28215
   289
wenzelm@28215
   290
    browser - Isabelle graph browser
wenzelm@28215
   291
    \dots
wenzelm@28215
   292
\end{ttbox}
wenzelm@28215
   293
wenzelm@28215
   294
  In principle, Isabelle tools are ordinary executable scripts that
wenzelm@28215
   295
  are run within the Isabelle settings environment, see
wenzelm@28215
   296
  \secref{sec:settings}.  The set of available tools is collected by
wenzelm@28215
   297
  @{executable isatool} from the directories listed in the @{setting
wenzelm@28215
   298
  ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
wenzelm@28215
   299
  from the shell.  Neither should you add the tool directories to your
wenzelm@28215
   300
  shell's search path!
wenzelm@28215
   301
*}
wenzelm@28215
   302
wenzelm@28215
   303
wenzelm@28215
   304
subsubsection {* Examples *}
wenzelm@28215
   305
wenzelm@28215
   306
text {*
wenzelm@28215
   307
  Show the list of available documentation of the current Isabelle
wenzelm@28215
   308
  installation like this:
wenzelm@28215
   309
wenzelm@28215
   310
\begin{ttbox}
wenzelm@28215
   311
  isatool doc
wenzelm@28215
   312
\end{ttbox}
wenzelm@28215
   313
wenzelm@28215
   314
  View a certain document as follows:
wenzelm@28215
   315
\begin{ttbox}
wenzelm@28215
   316
  isatool doc isar-ref
wenzelm@28215
   317
\end{ttbox}
wenzelm@28215
   318
wenzelm@28215
   319
  Create an Isabelle session derived from HOL (see also
wenzelm@28215
   320
  \secref{sec:tool-mkdir} and \secref{sec:tool-make}):
wenzelm@28215
   321
\begin{ttbox}
wenzelm@28215
   322
  isatool mkdir HOL Test && isatool make
wenzelm@28215
   323
\end{ttbox}
wenzelm@28215
   324
  Note that @{verbatim "isatool mkdir"} is usually only invoked once;
wenzelm@28215
   325
  existing sessions (including document output etc.) are then updated
wenzelm@28215
   326
  by @{verbatim "isatool make"} alone.
wenzelm@28215
   327
*}
wenzelm@28215
   328
wenzelm@28215
   329
wenzelm@28215
   330
section {* The raw Isabelle process *}
wenzelm@28215
   331
wenzelm@28215
   332
text {*
wenzelm@28215
   333
  The @{executable_ref isabelle} (or @{executable_ref
wenzelm@28215
   334
  "isabelle-process"}) executable runs bare-bones Isabelle logic
wenzelm@28215
   335
  sessions --- either interactively or in batch mode.  It provides an
wenzelm@28215
   336
  abstraction over the underlying ML system, and over the actual heap
wenzelm@28215
   337
  file locations.  Its usage is:
wenzelm@28215
   338
wenzelm@28215
   339
\begin{ttbox}
wenzelm@28215
   340
Usage: isabelle [OPTIONS] [INPUT] [OUTPUT]
wenzelm@28215
   341
wenzelm@28215
   342
  Options are:
wenzelm@28215
   343
    -C           tell ML system to copy output image
wenzelm@28215
   344
    -I           startup Isar interaction mode
wenzelm@28215
   345
    -P           startup Proof General interaction mode
wenzelm@28215
   346
    -S           secure mode -- disallow critical operations
wenzelm@28215
   347
    -W OUTPUT    startup process wrapper, with messages going to OUTPUT stream
wenzelm@28215
   348
    -X           startup PGIP interaction mode
wenzelm@28215
   349
    -c           tell ML system to compress output image
wenzelm@28215
   350
    -e MLTEXT    pass MLTEXT to the ML session
wenzelm@28215
   351
    -f           pass 'Session.finish();' to the ML session
wenzelm@28215
   352
    -m MODE      add print mode for output
wenzelm@28215
   353
    -q           non-interactive session
wenzelm@28215
   354
    -r           open heap file read-only
wenzelm@28215
   355
    -u           pass 'use"ROOT.ML";' to the ML session
wenzelm@28215
   356
    -w           reset write permissions on OUTPUT
wenzelm@28215
   357
wenzelm@28215
   358
  INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
wenzelm@28215
   359
  These are either names to be searched in the Isabelle path, or
wenzelm@28215
   360
  actual file names (containing at least one /).
wenzelm@28215
   361
  If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
wenzelm@28215
   362
\end{ttbox}
wenzelm@28215
   363
wenzelm@28215
   364
  Input files without path specifications are looked up in the
wenzelm@28215
   365
  @{setting ISABELLE_PATH} setting, which may consist of multiple
wenzelm@28215
   366
  components separated by colons --- these are tried in the given
wenzelm@28215
   367
  order with the value of @{setting ML_IDENTIFIER} appended
wenzelm@28215
   368
  internally.  In a similar way, base names are relative to the
wenzelm@28215
   369
  directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
wenzelm@28215
   370
  actual file locations may also be given by including at least one
wenzelm@28215
   371
  slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
wenzelm@28215
   372
  refer to the current directory).
wenzelm@28215
   373
*}
wenzelm@28215
   374
wenzelm@28215
   375
wenzelm@28223
   376
subsubsection {* Options *}
wenzelm@28215
   377
wenzelm@28215
   378
text {*
wenzelm@28215
   379
  If the input heap file does not have write permission bits set, or
wenzelm@28215
   380
  the @{verbatim "-r"} option is given explicitely, then the session
wenzelm@28215
   381
  started will be read-only.  That is, the ML world cannot be
wenzelm@28215
   382
  committed back into the image file.  Otherwise, a writable session
wenzelm@28215
   383
  enables commits into either the input file, or into another output
wenzelm@28215
   384
  heap file (if that is given as the second argument on the command
wenzelm@28215
   385
  line).
wenzelm@28215
   386
wenzelm@28215
   387
  The read-write state of sessions is determined at startup only, it
wenzelm@28215
   388
  cannot be changed intermediately. Also note that heap images may
wenzelm@28215
   389
  require considerable amounts of disk space (approximately
wenzelm@28215
   390
  50--200~MB). Users are responsible for themselves to dispose their
wenzelm@28215
   391
  heap files when they are no longer needed.
wenzelm@28215
   392
wenzelm@28215
   393
  \medskip The @{verbatim "-w"} option makes the output heap file
wenzelm@28215
   394
  read-only after terminating.  Thus subsequent invocations cause the
wenzelm@28215
   395
  logic image to be read-only automatically.
wenzelm@28215
   396
wenzelm@28215
   397
  \medskip The @{verbatim "-c"} option tells the underlying ML system
wenzelm@28215
   398
  to compress the output heap (fully transparently).  On Poly/ML for
wenzelm@28215
   399
  example, the image is garbage collected and all stored values are
wenzelm@28215
   400
  maximally shared, resulting in up to @{text "50%"} less disk space
wenzelm@28215
   401
  consumption.
wenzelm@28215
   402
wenzelm@28215
   403
  \medskip The @{verbatim "-C"} option tells the ML system to produce
wenzelm@28215
   404
  a completely self-contained output image, probably including a copy
wenzelm@28215
   405
  of the ML runtime system itself.
wenzelm@28215
   406
wenzelm@28215
   407
  \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
wenzelm@28215
   408
  passed to the Isabelle session from the command line. Multiple
wenzelm@28215
   409
  @{verbatim "-e"}'s are evaluated in the given order. Strange things
wenzelm@28215
   410
  may happen when errorneous ML code is provided. Also make sure that
wenzelm@28215
   411
  the ML commands are terminated properly by semicolon.
wenzelm@28215
   412
wenzelm@28215
   413
  \medskip The @{verbatim "-u"} option is a shortcut for @{verbatim
wenzelm@28215
   414
  "-e"} passing ``@{verbatim "use \"ROOT.ML\";"}'' to the ML session.
wenzelm@28223
   415
  The @{verbatim "-f"} option passes ``@{verbatim
wenzelm@28223
   416
  "Session.finish();"}'', which is intended mainly for administrative
wenzelm@28223
   417
  purposes.
wenzelm@28215
   418
wenzelm@28215
   419
  \medskip The @{verbatim "-m"} option adds identifiers of print modes
wenzelm@28215
   420
  to be made active for this session. Typically, this is used by some
wenzelm@28215
   421
  user interface, e.g.\ to enable output of proper mathematical
wenzelm@28215
   422
  symbols.
wenzelm@28215
   423
wenzelm@28215
   424
  \medskip Isabelle normally enters an interactive top-level loop
wenzelm@28215
   425
  (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
wenzelm@28215
   426
  option inhibits interaction, thus providing a pure batch mode
wenzelm@28215
   427
  facility.
wenzelm@28215
   428
wenzelm@28215
   429
  \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
wenzelm@28215
   430
  interaction mode on startup, instead of the primitive ML top-level.
wenzelm@28215
   431
  The @{verbatim "-P"} option configures the top-level loop for
wenzelm@28215
   432
  interaction with the Proof General user interface, and the
wenzelm@28215
   433
  @{verbatim "-X"} option enables XML-based PGIP communication.  The
wenzelm@28215
   434
  @{verbatim "-W"} option makes Isabelle enter a special process
wenzelm@28215
   435
  wrapper for interaction via an external program; the protocol is a
wenzelm@28215
   436
  stripped-down version of Proof General the interaction mode.
wenzelm@28215
   437
wenzelm@28215
   438
  \medskip The @{verbatim "-S"} option makes the Isabelle process more
wenzelm@28215
   439
  secure by disabling some critical operations, notably runtime
wenzelm@28215
   440
  compilation and evaluation of ML source code.
wenzelm@28215
   441
*}
wenzelm@28215
   442
wenzelm@28215
   443
wenzelm@28223
   444
subsubsection {* Examples *}
wenzelm@28215
   445
wenzelm@28215
   446
text {*
wenzelm@28215
   447
  Run an interactive session of the default object-logic (as specified
wenzelm@28215
   448
  by the @{setting ISABELLE_LOGIC} setting) like this:
wenzelm@28215
   449
\begin{ttbox}
wenzelm@28215
   450
isabelle
wenzelm@28215
   451
\end{ttbox}
wenzelm@28215
   452
wenzelm@28215
   453
  Usually @{setting ISABELLE_LOGIC} refers to one of the standard
wenzelm@28215
   454
  logic images, which are read-only by default.  A writable session
wenzelm@28215
   455
  --- based on @{verbatim FOL}, but output to @{verbatim Foo} (in the
wenzelm@28215
   456
  directory specified by the @{verbatim ISABELLE_OUTPUT} setting) ---
wenzelm@28215
   457
  may be invoked as follows:
wenzelm@28215
   458
\begin{ttbox}
wenzelm@28215
   459
isabelle FOL Foo
wenzelm@28215
   460
\end{ttbox}
wenzelm@28215
   461
  Ending this session normally (e.g.\ by typing control-D) dumps the
wenzelm@28215
   462
  whole ML system state into @{verbatim Foo}. Be prepared for several
wenzelm@28215
   463
  tens of megabytes.
wenzelm@28215
   464
wenzelm@28215
   465
  The @{verbatim Foo} session may be continued later (still in
wenzelm@28215
   466
  writable state) by:
wenzelm@28215
   467
\begin{ttbox}
wenzelm@28215
   468
isabelle Foo
wenzelm@28215
   469
\end{ttbox}
wenzelm@28215
   470
  A read-only @{verbatim Foo} session may be started by:
wenzelm@28215
   471
\begin{ttbox}
wenzelm@28215
   472
isabelle -r Foo
wenzelm@28215
   473
\end{ttbox}
wenzelm@28215
   474
wenzelm@28215
   475
  \medskip Note that manual session management like this does
wenzelm@28215
   476
  \emph{not} provide proper setup for theory presentation.  This would
wenzelm@28215
   477
  require the @{tool usedir} utility, see \secref{sec:tool-usedir}.
wenzelm@28215
   478
wenzelm@28215
   479
  \bigskip The next example demonstrates batch execution of
wenzelm@28215
   480
  Isabelle. We print a certain theorem of @{verbatim FOL}:
wenzelm@28215
   481
\begin{ttbox}
wenzelm@28215
   482
isabelle -e "prth allE;" -q -r FOL
wenzelm@28215
   483
\end{ttbox}
wenzelm@28215
   484
  Note that the output text will be interspersed with additional junk
wenzelm@28215
   485
  messages by the ML runtime environment.
wenzelm@28215
   486
*}
wenzelm@28215
   487
wenzelm@28215
   488
wenzelm@28215
   489
section {* The Isabelle interface wrapper \label{sec:interface} *}
wenzelm@28215
   490
wenzelm@28215
   491
text {*
wenzelm@28215
   492
  Isabelle is a generic theorem prover, even w.r.t.\ its user
wenzelm@28215
   493
  interface.  The @{executable_ref Isabelle} (or @{executable_ref
wenzelm@28215
   494
  "isabelle-interface"}) executable provides a uniform way for
wenzelm@28215
   495
  end-users to invoke a certain interface; which one to start is
wenzelm@28215
   496
  determined by the @{setting_ref ISABELLE_INTERFACE} setting
wenzelm@28215
   497
  variable, which should give a full path specification to the actual
wenzelm@28215
   498
  executable.  Also note that the @{tool install} utility provides
wenzelm@28215
   499
  some options to install desktop environment icons (see
wenzelm@28215
   500
  \secref{sec:tool-install}).
wenzelm@28215
   501
wenzelm@28215
   502
  Presently, the most prominent Isabelle interface is Proof
wenzelm@28215
   503
  General~\cite{proofgeneral}\index{user interface!Proof General}.
wenzelm@28215
   504
  The Proof General distribution includes an interface wrapper script
wenzelm@28215
   505
  for the regular Isar toplevel, see @{verbatim
wenzelm@28215
   506
  "ProofGeneral/isar/interface"}.  The canonical settings for
wenzelm@28215
   507
  Isabelle/Isar are as follows:
wenzelm@28215
   508
wenzelm@28215
   509
\begin{ttbox}
wenzelm@28215
   510
ISABELLE_INTERFACE=\$ISABELLE_HOME/contrib/ProofGeneral/isar/interface
wenzelm@28215
   511
PROOFGENERAL_OPTIONS=""
wenzelm@28215
   512
\end{ttbox}
wenzelm@28215
   513
wenzelm@28215
   514
  Thus @{executable Isabelle} would automatically invoke Emacs with
wenzelm@28215
   515
  proper setup of the Proof General Lisp packages.  There are some
wenzelm@28215
   516
  options available, such as @{verbatim "-l"} for passing the logic
wenzelm@28215
   517
  image to be used by default, or @{verbatim "-m"} to tune the
wenzelm@28215
   518
  standard print mode.  The @{verbatim "-I"} option allows to switch
wenzelm@28215
   519
  between the Isar and ML view, independently of the interface script
wenzelm@28215
   520
  being used.
wenzelm@28215
   521
  
wenzelm@28215
   522
  \medskip Note that the world may be also seen the other way round:
wenzelm@28215
   523
  Emacs may be started first (with proper setup of Proof General
wenzelm@28215
   524
  mode), and @{executable isabelle} run from within.  This requires
wenzelm@28215
   525
  further Emacs Lisp configuration, see the Proof General
wenzelm@28215
   526
  documentation \cite{proofgeneral} for more information.
wenzelm@28215
   527
*}
wenzelm@28215
   528
wenzelm@28223
   529
end