src/Doc/System/Basics.thy
author wenzelm
Sun Sep 21 20:22:12 2014 +0200 (2014-09-21)
changeset 58413 22dd971f6938
parent 57581 74bbe9317aa4
child 58553 3876a1a9ee42
permissions -rw-r--r--
renamed ISABELLE_POLYML to ML_SYSTEM_POLYML, to avoid overlap with ISABELLE_POLYML_PATH;
wenzelm@28215
     1
theory Basics
wenzelm@43564
     2
imports Base
wenzelm@28215
     3
begin
wenzelm@28215
     4
wenzelm@28215
     5
chapter {* The Isabelle system environment *}
wenzelm@28215
     6
wenzelm@47823
     7
text {* This manual describes Isabelle together with related tools and
wenzelm@47823
     8
  user interfaces as seen from a system oriented view.  See also the
wenzelm@28916
     9
  \emph{Isabelle/Isar Reference Manual}~\cite{isabelle-isar-ref} for
wenzelm@47823
    10
  the actual Isabelle input language and related concepts, and
wenzelm@47823
    11
  \emph{The Isabelle/Isar Implementation
wenzelm@47823
    12
  Manual}~\cite{isabelle-implementation} for the main concepts of the
wenzelm@47823
    13
  underlying implementation in Isabelle/ML.
wenzelm@28215
    14
wenzelm@28916
    15
  \medskip The Isabelle system environment provides the following
wenzelm@28916
    16
  basic infrastructure to integrate tools smoothly.
wenzelm@28215
    17
wenzelm@28238
    18
  \begin{enumerate}
wenzelm@28215
    19
wenzelm@28916
    20
  \item The \emph{Isabelle settings} mechanism provides process
wenzelm@28916
    21
  environment variables to all Isabelle executables (including tools
wenzelm@28916
    22
  and user interfaces).
wenzelm@28215
    23
wenzelm@47823
    24
  \item The raw \emph{Isabelle process} (@{executable_ref
wenzelm@56439
    25
  "isabelle_process"}) runs logic sessions either interactively or in
wenzelm@28504
    26
  batch mode.  In particular, this view abstracts over the invocation
wenzelm@28504
    27
  of the actual ML system to be used.  Regular users rarely need to
wenzelm@28504
    28
  care about the low-level process.
wenzelm@28215
    29
wenzelm@48813
    30
  \item The main \emph{Isabelle tool wrapper} (@{executable_ref
wenzelm@47823
    31
  isabelle}) provides a generic startup environment Isabelle related
wenzelm@47823
    32
  utilities, user interfaces etc.  Such tools automatically benefit
wenzelm@47823
    33
  from the settings mechanism.
wenzelm@28215
    34
wenzelm@28238
    35
  \end{enumerate}
wenzelm@28215
    36
*}
wenzelm@28215
    37
wenzelm@28215
    38
wenzelm@28215
    39
section {* Isabelle settings \label{sec:settings} *}
wenzelm@28215
    40
wenzelm@28215
    41
text {*
wenzelm@28215
    42
  The Isabelle system heavily depends on the \emph{settings
wenzelm@28215
    43
  mechanism}\indexbold{settings}.  Essentially, this is a statically
wenzelm@28215
    44
  scoped collection of environment variables, such as @{setting
wenzelm@28215
    45
  ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting ML_HOME}.  These
wenzelm@28215
    46
  variables are \emph{not} intended to be set directly from the shell,
wenzelm@28215
    47
  though.  Isabelle employs a somewhat more sophisticated scheme of
wenzelm@28215
    48
  \emph{settings files} --- one for site-wide defaults, another for
wenzelm@28215
    49
  additional user-specific modifications.  With all configuration
wenzelm@47823
    50
  variables in clearly defined places, this scheme is more
wenzelm@47823
    51
  maintainable and user-friendly than global shell environment
wenzelm@47823
    52
  variables.
wenzelm@28215
    53
wenzelm@28215
    54
  In particular, we avoid the typical situation where prospective
wenzelm@28215
    55
  users of a software package are told to put several things into
wenzelm@28215
    56
  their shell startup scripts, before being able to actually run the
wenzelm@28215
    57
  program. Isabelle requires none such administrative chores of its
wenzelm@28215
    58
  end-users --- the executables can be invoked straight away.
wenzelm@40800
    59
  Occasionally, users would still want to put the @{file
wenzelm@28238
    60
  "$ISABELLE_HOME/bin"} directory into their shell's search path, but
wenzelm@28238
    61
  this is not required.
wenzelm@28215
    62
*}
wenzelm@28215
    63
wenzelm@28215
    64
wenzelm@32323
    65
subsection {* Bootstrapping the environment \label{sec:boot} *}
wenzelm@28215
    66
wenzelm@32323
    67
text {* Isabelle executables need to be run within a proper settings
wenzelm@32323
    68
  environment.  This is bootstrapped as described below, on the first
wenzelm@32323
    69
  invocation of one of the outer wrapper scripts (such as
wenzelm@32323
    70
  @{executable_ref isabelle}).  This happens only once for each
wenzelm@32323
    71
  process tree, i.e.\ the environment is passed to subprocesses
wenzelm@32323
    72
  according to regular Unix conventions.
wenzelm@28215
    73
wenzelm@28215
    74
  \begin{enumerate}
wenzelm@28215
    75
wenzelm@28215
    76
  \item The special variable @{setting_def ISABELLE_HOME} is
wenzelm@28215
    77
  determined automatically from the location of the binary that has
wenzelm@28215
    78
  been run.
wenzelm@28215
    79
  
wenzelm@28215
    80
  You should not try to set @{setting ISABELLE_HOME} manually. Also
wenzelm@28215
    81
  note that the Isabelle executables either have to be run from their
wenzelm@28215
    82
  original location in the distribution directory, or via the
wenzelm@48602
    83
  executable objects created by the @{tool install} tool.  Symbolic
wenzelm@40800
    84
  links are admissible, but a plain copy of the @{file
wenzelm@28238
    85
  "$ISABELLE_HOME/bin"} files will not work!
wenzelm@28238
    86
wenzelm@40800
    87
  \item The file @{file "$ISABELLE_HOME/etc/settings"} is run as a
wenzelm@28238
    88
  @{executable_ref bash} shell script with the auto-export option for
wenzelm@28238
    89
  variables enabled.
wenzelm@28215
    90
  
wenzelm@28215
    91
  This file holds a rather long list of shell variable assigments,
wenzelm@28215
    92
  thus providing the site-wide default settings.  The Isabelle
wenzelm@28215
    93
  distribution already contains a global settings file with sensible
wenzelm@28215
    94
  defaults for most variables.  When installing the system, only a few
wenzelm@28215
    95
  of these may have to be adapted (probably @{setting ML_SYSTEM}
wenzelm@28215
    96
  etc.).
wenzelm@28215
    97
  
wenzelm@54705
    98
  \item The file @{file_unchecked "$ISABELLE_HOME_USER/etc/settings"} (if it
wenzelm@28215
    99
  exists) is run in the same way as the site default settings. Note
wenzelm@28215
   100
  that the variable @{setting ISABELLE_HOME_USER} has already been set
wenzelm@40387
   101
  before --- usually to something like @{verbatim
wenzelm@47661
   102
  "$USER_HOME/.isabelle/IsabelleXXXX"}.
wenzelm@28215
   103
  
wenzelm@54937
   104
  Thus individual users may override the site-wide defaults.
wenzelm@54937
   105
  Typically, a user settings file contains only a few lines, with some
wenzelm@54937
   106
  assignments that are actually changed.  Never copy the central
wenzelm@54937
   107
  @{file "$ISABELLE_HOME/etc/settings"} file!
wenzelm@28215
   108
  
wenzelm@28215
   109
  \end{enumerate}
wenzelm@28215
   110
wenzelm@28238
   111
  Since settings files are regular GNU @{executable_def bash} scripts,
wenzelm@28238
   112
  one may use complex shell commands, such as @{verbatim "if"} or
wenzelm@28215
   113
  @{verbatim "case"} statements to set variables depending on the
wenzelm@28215
   114
  system architecture or other environment variables.  Such advanced
wenzelm@28215
   115
  features should be added only with great care, though. In
wenzelm@28215
   116
  particular, external environment references should be kept at a
wenzelm@28215
   117
  minimum.
wenzelm@28215
   118
wenzelm@28215
   119
  \medskip A few variables are somewhat special:
wenzelm@28215
   120
wenzelm@28215
   121
  \begin{itemize}
wenzelm@28215
   122
wenzelm@28502
   123
  \item @{setting_def ISABELLE_PROCESS} and @{setting_def ISABELLE_TOOL} are set
wenzelm@28215
   124
  automatically to the absolute path names of the @{executable
wenzelm@56439
   125
  "isabelle_process"} and @{executable isabelle} executables,
wenzelm@28215
   126
  respectively.
wenzelm@28215
   127
  
wenzelm@28238
   128
  \item @{setting_ref ISABELLE_OUTPUT} will have the identifiers of
wenzelm@28215
   129
  the Isabelle distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and
wenzelm@28215
   130
  the ML system (cf.\ @{setting ML_IDENTIFIER}) appended automatically
wenzelm@28215
   131
  to its value.
wenzelm@28215
   132
wenzelm@28215
   133
  \end{itemize}
wenzelm@28215
   134
wenzelm@28238
   135
  \medskip Note that the settings environment may be inspected with
wenzelm@48602
   136
  the @{tool getenv} tool.  This might help to figure out the effect
wenzelm@48602
   137
  of complex settings scripts.  *}
wenzelm@28215
   138
wenzelm@28215
   139
wenzelm@48602
   140
subsection {* Common variables *}
wenzelm@28215
   141
wenzelm@28215
   142
text {*
wenzelm@28215
   143
  This is a reference of common Isabelle settings variables. Note that
wenzelm@28215
   144
  the list is somewhat open-ended. Third-party utilities or interfaces
wenzelm@28215
   145
  may add their own selection. Variables that are special in some
wenzelm@28215
   146
  sense are marked with @{text "\<^sup>*"}.
wenzelm@28215
   147
wenzelm@28215
   148
  \begin{description}
wenzelm@28215
   149
wenzelm@47823
   150
  \item[@{setting_def USER_HOME}@{text "\<^sup>*"}] Is the cross-platform
wenzelm@47823
   151
  user home directory.  On Unix systems this is usually the same as
wenzelm@47823
   152
  @{setting HOME}, but on Windows it is the regular home directory of
wenzelm@47823
   153
  the user, not the one of within the Cygwin root
wenzelm@47823
   154
  file-system.\footnote{Cygwin itself offers another choice whether
wenzelm@47823
   155
  its HOME should point to the \texttt{/home} directory tree or the
wenzelm@47823
   156
  Windows user home.}
wenzelm@47661
   157
wenzelm@47661
   158
 \item[@{setting_def ISABELLE_HOME}@{text "\<^sup>*"}] is the location of the
wenzelm@47661
   159
  top-level Isabelle distribution directory. This is automatically
wenzelm@47661
   160
  determined from the Isabelle executable that has been invoked.  Do
wenzelm@47661
   161
  not attempt to set @{setting ISABELLE_HOME} yourself from the shell!
wenzelm@28215
   162
  
wenzelm@28215
   163
  \item[@{setting_def ISABELLE_HOME_USER}] is the user-specific
wenzelm@28215
   164
  counterpart of @{setting ISABELLE_HOME}. The default value is
wenzelm@54705
   165
  relative to @{file_unchecked "$USER_HOME/.isabelle"}, under rare
wenzelm@47661
   166
  circumstances this may be changed in the global setting file.
wenzelm@47661
   167
  Typically, the @{setting ISABELLE_HOME_USER} directory mimics
wenzelm@47661
   168
  @{setting ISABELLE_HOME} to some extend. In particular, site-wide
wenzelm@47661
   169
  defaults may be overridden by a private @{verbatim
wenzelm@40387
   170
  "$ISABELLE_HOME_USER/etc/settings"}.
wenzelm@50182
   171
wenzelm@50182
   172
  \item[@{setting_def ISABELLE_PLATFORM_FAMILY}@{text "\<^sup>*"}] is
wenzelm@50182
   173
  automatically set to the general platform family: @{verbatim linux},
wenzelm@50182
   174
  @{verbatim macos}, @{verbatim windows}.  Note that
wenzelm@50182
   175
  platform-dependent tools usually need to refer to the more specific
wenzelm@50182
   176
  identification according to @{setting ISABELLE_PLATFORM}, @{setting
wenzelm@50182
   177
  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
wenzelm@50182
   178
wenzelm@36196
   179
  \item[@{setting_def ISABELLE_PLATFORM}@{text "\<^sup>*"}] is automatically
wenzelm@36196
   180
  set to a symbolic identifier for the underlying hardware and
wenzelm@36196
   181
  operating system.  The Isabelle platform identification always
wenzelm@36196
   182
  refers to the 32 bit variant, even this is a 64 bit machine.  Note
wenzelm@36196
   183
  that the ML or Java runtime may have a different idea, depending on
wenzelm@36196
   184
  which binaries are actually run.
wenzelm@36196
   185
wenzelm@36196
   186
  \item[@{setting_def ISABELLE_PLATFORM64}@{text "\<^sup>*"}] is similar to
wenzelm@36196
   187
  @{setting ISABELLE_PLATFORM} but refers to the proper 64 bit variant
wenzelm@36196
   188
  on a platform that supports this; the value is empty for 32 bit.
wenzelm@47823
   189
  Note that the following bash expression (including the quotes)
wenzelm@47823
   190
  prefers the 64 bit platform, if that is available:
wenzelm@47823
   191
wenzelm@47823
   192
  @{verbatim [display] "\"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}\""}
wenzelm@36196
   193
wenzelm@28502
   194
  \item[@{setting_def ISABELLE_PROCESS}@{text "\<^sup>*"}, @{setting
wenzelm@28500
   195
  ISABELLE_TOOL}@{text "\<^sup>*"}] are automatically set to the full path
wenzelm@56439
   196
  names of the @{executable "isabelle_process"} and @{executable
wenzelm@28504
   197
  isabelle} executables, respectively.  Thus other tools and scripts
wenzelm@40800
   198
  need not assume that the @{file "$ISABELLE_HOME/bin"} directory is
wenzelm@28238
   199
  on the current search path of the shell.
wenzelm@28215
   200
  
wenzelm@28215
   201
  \item[@{setting_def ISABELLE_IDENTIFIER}@{text "\<^sup>*"}] refers
wenzelm@28215
   202
  to the name of this Isabelle distribution, e.g.\ ``@{verbatim
wenzelm@47823
   203
  Isabelle2012}''.
wenzelm@28215
   204
wenzelm@28215
   205
  \item[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME},
wenzelm@28215
   206
  @{setting_def ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def
wenzelm@28215
   207
  ML_IDENTIFIER}@{text "\<^sup>*"}] specify the underlying ML system
wenzelm@28215
   208
  to be used for Isabelle.  There is only a fixed set of admissable
wenzelm@40800
   209
  @{setting ML_SYSTEM} names (see the @{file
wenzelm@28238
   210
  "$ISABELLE_HOME/etc/settings"} file of the distribution).
wenzelm@28215
   211
  
wenzelm@28215
   212
  The actual compiler binary will be run from the directory @{setting
wenzelm@28215
   213
  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the
wenzelm@28215
   214
  command line.  The optional @{setting ML_PLATFORM} may specify the
wenzelm@28215
   215
  binary format of ML heap images, which is useful for cross-platform
wenzelm@28215
   216
  installations.  The value of @{setting ML_IDENTIFIER} is
wenzelm@28215
   217
  automatically obtained by composing the values of @{setting
wenzelm@28215
   218
  ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version values.
wenzelm@47823
   219
wenzelm@58413
   220
  \item[@{setting_def ML_SYSTEM_POLYML}@{text "\<^sup>*"}] is @{verbatim true}
wenzelm@51434
   221
  for @{setting ML_SYSTEM} values derived from Poly/ML, as opposed to
wenzelm@51434
   222
  SML/NJ where it is empty.  This is particularly useful with the
wenzelm@51434
   223
  build option @{system_option condition}
wenzelm@51434
   224
  (\secref{sec:system-options}) to restrict big sessions to something
wenzelm@51434
   225
  that SML/NJ can still handle.
wenzelm@51434
   226
wenzelm@47823
   227
  \item[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK
wenzelm@47823
   228
  (Java Development Kit) installation with @{verbatim javac} and
wenzelm@47823
   229
  @{verbatim jar} executables.  This is essential for Isabelle/Scala
wenzelm@47823
   230
  and other JVM-based tools to work properly.  Note that conventional
wenzelm@47823
   231
  @{verbatim JAVA_HOME} usually points to the JRE (Java Runtime
wenzelm@47823
   232
  Environment), not JDK.
wenzelm@28215
   233
  
wenzelm@28215
   234
  \item[@{setting_def ISABELLE_PATH}] is a list of directories
wenzelm@28215
   235
  (separated by colons) where Isabelle logic images may reside.  When
wenzelm@28215
   236
  looking up heaps files, the value of @{setting ML_IDENTIFIER} is
wenzelm@28215
   237
  appended to each component internally.
wenzelm@28215
   238
  
wenzelm@28215
   239
  \item[@{setting_def ISABELLE_OUTPUT}@{text "\<^sup>*"}] is a
wenzelm@28215
   240
  directory where output heap files should be stored by default. The
wenzelm@28215
   241
  ML system and Isabelle version identifier is appended here, too.
wenzelm@28215
   242
  
wenzelm@28215
   243
  \item[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where
wenzelm@28215
   244
  theory browser information (HTML text, graph data, and printable
wenzelm@28215
   245
  documents) is stored (see also \secref{sec:info}).  The default
wenzelm@54705
   246
  value is @{file_unchecked "$ISABELLE_HOME_USER/browser_info"}.
wenzelm@28215
   247
  
wenzelm@28215
   248
  \item[@{setting_def ISABELLE_LOGIC}] specifies the default logic to
wenzelm@28215
   249
  load if none is given explicitely by the user.  The default value is
wenzelm@28215
   250
  @{verbatim HOL}.
wenzelm@28215
   251
  
wenzelm@57439
   252
  \item[@{setting_def ISABELLE_LINE_EDITOR}] specifies the
wenzelm@57439
   253
  line editor for the @{tool_ref console} interface.
wenzelm@28215
   254
wenzelm@28215
   255
  \item[@{setting_def ISABELLE_LATEX}, @{setting_def
wenzelm@52746
   256
  ISABELLE_PDFLATEX}, @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX}
wenzelm@52746
   257
  related tools for Isabelle document preparation (see also
wenzelm@52746
   258
  \secref{sec:tool-latex}).
wenzelm@28215
   259
  
wenzelm@28215
   260
  \item[@{setting_def ISABELLE_TOOLS}] is a colon separated list of
wenzelm@28504
   261
  directories that are scanned by @{executable isabelle} for external
wenzelm@28504
   262
  utility programs (see also \secref{sec:isabelle-tool}).
wenzelm@28215
   263
  
wenzelm@28215
   264
  \item[@{setting_def ISABELLE_DOCS}] is a colon separated list of
wenzelm@28215
   265
  directories with documentation files.
wenzelm@50197
   266
wenzelm@54683
   267
  \item[@{setting_def PDF_VIEWER}] specifies the program to be used
wenzelm@54683
   268
  for displaying @{verbatim pdf} files.
wenzelm@54683
   269
wenzelm@54683
   270
  \item[@{setting_def DVI_VIEWER}] specifies the program to be used
wenzelm@54683
   271
  for displaying @{verbatim dvi} files.
wenzelm@28215
   272
  
wenzelm@28215
   273
  \item[@{setting_def ISABELLE_TMP_PREFIX}@{text "\<^sup>*"}] is the
wenzelm@56439
   274
  prefix from which any running @{executable "isabelle_process"}
wenzelm@28238
   275
  derives an individual directory for temporary files.  The default is
wenzelm@54705
   276
  somewhere in @{file_unchecked "/tmp"}.
wenzelm@28215
   277
  
wenzelm@28215
   278
  \end{description}
wenzelm@28215
   279
*}
wenzelm@28215
   280
wenzelm@28215
   281
wenzelm@32323
   282
subsection {* Additional components \label{sec:components} *}
wenzelm@32323
   283
wenzelm@32323
   284
text {* Any directory may be registered as an explicit \emph{Isabelle
wenzelm@32323
   285
  component}.  The general layout conventions are that of the main
wenzelm@32323
   286
  Isabelle distribution itself, and the following two files (both
wenzelm@32323
   287
  optional) have a special meaning:
wenzelm@32323
   288
wenzelm@32323
   289
  \begin{itemize}
wenzelm@32323
   290
wenzelm@32323
   291
  \item @{verbatim "etc/settings"} holds additional settings that are
wenzelm@32323
   292
  initialized when bootstrapping the overall Isabelle environment,
wenzelm@32323
   293
  cf.\ \secref{sec:boot}.  As usual, the content is interpreted as a
wenzelm@32323
   294
  @{verbatim bash} script.  It may refer to the component's enclosing
wenzelm@32323
   295
  directory via the @{verbatim "COMPONENT"} shell variable.
wenzelm@32323
   296
wenzelm@32323
   297
  For example, the following setting allows to refer to files within
wenzelm@32323
   298
  the component later on, without having to hardwire absolute paths:
wenzelm@32323
   299
wenzelm@48838
   300
\begin{ttbox}
wenzelm@48838
   301
MY_COMPONENT_HOME="$COMPONENT"
wenzelm@48838
   302
\end{ttbox}
wenzelm@32323
   303
wenzelm@32323
   304
  Components can also add to existing Isabelle settings such as
wenzelm@32323
   305
  @{setting_def ISABELLE_TOOLS}, in order to provide
wenzelm@32323
   306
  component-specific tools that can be invoked by end-users.  For
wenzelm@32323
   307
  example:
wenzelm@32323
   308
wenzelm@48838
   309
\begin{ttbox}
wenzelm@48838
   310
ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
wenzelm@48838
   311
\end{ttbox}
wenzelm@32323
   312
wenzelm@32323
   313
  \item @{verbatim "etc/components"} holds a list of further
wenzelm@32323
   314
  sub-components of the same structure.  The directory specifications
wenzelm@32323
   315
  given here can be either absolute (with leading @{verbatim "/"}) or
wenzelm@32323
   316
  relative to the component's main directory.
wenzelm@32323
   317
wenzelm@32323
   318
  \end{itemize}
wenzelm@32323
   319
wenzelm@32323
   320
  The root of component initialization is @{setting ISABELLE_HOME}
wenzelm@32323
   321
  itself.  After initializing all of its sub-components recursively,
wenzelm@32323
   322
  @{setting ISABELLE_HOME_USER} is included in the same manner (if
wenzelm@40569
   323
  that directory exists).  This allows to install private components
wenzelm@54705
   324
  via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is
wenzelm@40569
   325
  often more convenient to do that programmatically via the
wenzelm@40569
   326
  \verb,init_component, shell function in the \verb,etc/settings,
wenzelm@40569
   327
  script of \verb,$ISABELLE_HOME_USER, (or any other component
wenzelm@40569
   328
  directory).  For example:
wenzelm@48838
   329
\begin{ttbox}
wenzelm@48838
   330
init_component "$HOME/screwdriver-2.0"
wenzelm@48838
   331
\end{ttbox}
wenzelm@48838
   332
wenzelm@48838
   333
  This is tolerant wrt.\ missing component directories, but might
wenzelm@48838
   334
  produce a warning.
wenzelm@48838
   335
wenzelm@48838
   336
  \medskip More complex situations may be addressed by initializing
wenzelm@48838
   337
  components listed in a given catalog file, relatively to some base
wenzelm@48838
   338
  directory:
wenzelm@48838
   339
wenzelm@48838
   340
\begin{ttbox}
wenzelm@48838
   341
init_components "$HOME/my_component_store" "some_catalog_file"
wenzelm@48838
   342
\end{ttbox}
wenzelm@48838
   343
wenzelm@48838
   344
  The component directories listed in the catalog file are treated as
wenzelm@48838
   345
  relative to the given base directory.
wenzelm@48844
   346
wenzelm@48844
   347
  See also \secref{sec:tool-components} for some tool-support for
wenzelm@48844
   348
  resolving components that are formally initialized but not installed
wenzelm@48844
   349
  yet.
wenzelm@32323
   350
*}
wenzelm@32323
   351
wenzelm@32323
   352
wenzelm@57439
   353
section {* The raw Isabelle process \label{sec:isabelle-process} *}
wenzelm@28215
   354
wenzelm@28215
   355
text {*
wenzelm@56439
   356
  The @{executable_def "isabelle_process"} executable runs bare-bones
wenzelm@28504
   357
  Isabelle logic sessions --- either interactively or in batch mode.
wenzelm@28504
   358
  It provides an abstraction over the underlying ML system, and over
wenzelm@28504
   359
  the actual heap file locations.  Its usage is:
wenzelm@28215
   360
wenzelm@28215
   361
\begin{ttbox}
wenzelm@56439
   362
Usage: isabelle_process [OPTIONS] [INPUT] [OUTPUT]
wenzelm@28215
   363
wenzelm@28215
   364
  Options are:
wenzelm@28215
   365
    -I           startup Isar interaction mode
wenzelm@57581
   366
    -O           system options from given YXML file
wenzelm@28215
   367
    -P           startup Proof General interaction mode
wenzelm@28215
   368
    -S           secure mode -- disallow critical operations
wenzelm@45028
   369
    -T ADDR      startup process wrapper, with socket address
wenzelm@38253
   370
    -W IN:OUT    startup process wrapper, with input/output fifos
wenzelm@28215
   371
    -e MLTEXT    pass MLTEXT to the ML session
wenzelm@28215
   372
    -m MODE      add print mode for output
wenzelm@52056
   373
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@28215
   374
    -q           non-interactive session
wenzelm@28215
   375
    -r           open heap file read-only
wenzelm@28215
   376
    -w           reset write permissions on OUTPUT
wenzelm@28215
   377
wenzelm@28215
   378
  INPUT (default "\$ISABELLE_LOGIC") and OUTPUT specify in/out heaps.
wenzelm@28215
   379
  These are either names to be searched in the Isabelle path, or
wenzelm@28215
   380
  actual file names (containing at least one /).
wenzelm@28215
   381
  If INPUT is "RAW_ML_SYSTEM", just start the bare bones ML system.
wenzelm@28215
   382
\end{ttbox}
wenzelm@28215
   383
wenzelm@28215
   384
  Input files without path specifications are looked up in the
wenzelm@28215
   385
  @{setting ISABELLE_PATH} setting, which may consist of multiple
wenzelm@28215
   386
  components separated by colons --- these are tried in the given
wenzelm@28215
   387
  order with the value of @{setting ML_IDENTIFIER} appended
wenzelm@28215
   388
  internally.  In a similar way, base names are relative to the
wenzelm@28215
   389
  directory specified by @{setting ISABELLE_OUTPUT}.  In any case,
wenzelm@28215
   390
  actual file locations may also be given by including at least one
wenzelm@28215
   391
  slash (@{verbatim "/"}) in the name (hint: use @{verbatim "./"} to
wenzelm@28215
   392
  refer to the current directory).
wenzelm@28215
   393
*}
wenzelm@28215
   394
wenzelm@28215
   395
wenzelm@28223
   396
subsubsection {* Options *}
wenzelm@28215
   397
wenzelm@28215
   398
text {*
wenzelm@28215
   399
  If the input heap file does not have write permission bits set, or
wenzelm@57581
   400
  the @{verbatim "-r"} option is given explicitly, then the session
wenzelm@28215
   401
  started will be read-only.  That is, the ML world cannot be
wenzelm@28215
   402
  committed back into the image file.  Otherwise, a writable session
wenzelm@28215
   403
  enables commits into either the input file, or into another output
wenzelm@28215
   404
  heap file (if that is given as the second argument on the command
wenzelm@28215
   405
  line).
wenzelm@28215
   406
wenzelm@28215
   407
  The read-write state of sessions is determined at startup only, it
wenzelm@28215
   408
  cannot be changed intermediately. Also note that heap images may
wenzelm@28215
   409
  require considerable amounts of disk space (approximately
wenzelm@28215
   410
  50--200~MB). Users are responsible for themselves to dispose their
wenzelm@28215
   411
  heap files when they are no longer needed.
wenzelm@28215
   412
wenzelm@28215
   413
  \medskip The @{verbatim "-w"} option makes the output heap file
wenzelm@28215
   414
  read-only after terminating.  Thus subsequent invocations cause the
wenzelm@28215
   415
  logic image to be read-only automatically.
wenzelm@28215
   416
wenzelm@28215
   417
  \medskip Using the @{verbatim "-e"} option, arbitrary ML code may be
wenzelm@28215
   418
  passed to the Isabelle session from the command line. Multiple
wenzelm@28215
   419
  @{verbatim "-e"}'s are evaluated in the given order. Strange things
wenzelm@56604
   420
  may happen when erroneous ML code is provided. Also make sure that
wenzelm@28215
   421
  the ML commands are terminated properly by semicolon.
wenzelm@28215
   422
wenzelm@28215
   423
  \medskip The @{verbatim "-m"} option adds identifiers of print modes
wenzelm@28215
   424
  to be made active for this session. Typically, this is used by some
wenzelm@28215
   425
  user interface, e.g.\ to enable output of proper mathematical
wenzelm@28215
   426
  symbols.
wenzelm@28215
   427
wenzelm@28215
   428
  \medskip Isabelle normally enters an interactive top-level loop
wenzelm@28215
   429
  (after processing the @{verbatim "-e"} texts). The @{verbatim "-q"}
wenzelm@28215
   430
  option inhibits interaction, thus providing a pure batch mode
wenzelm@28215
   431
  facility.
wenzelm@28215
   432
wenzelm@52061
   433
  \medskip Option @{verbatim "-o"} allows to override Isabelle system
wenzelm@52056
   434
  options for this process, see also \secref{sec:system-options}.
wenzelm@57581
   435
  Alternatively, option @{verbatim "-O"} specifies the full environment of
wenzelm@57581
   436
  system options as a file in YXML format (according to the Isabelle/Scala
wenzelm@57581
   437
  function @{verbatim isabelle.Options.encode}).
wenzelm@52056
   438
wenzelm@28215
   439
  \medskip The @{verbatim "-I"} option makes Isabelle enter Isar
wenzelm@28215
   440
  interaction mode on startup, instead of the primitive ML top-level.
wenzelm@28215
   441
  The @{verbatim "-P"} option configures the top-level loop for
wenzelm@51932
   442
  interaction with the Proof General user interface.
wenzelm@38253
   443
wenzelm@45028
   444
  \medskip The @{verbatim "-T"} or @{verbatim "-W"} option makes
wenzelm@49173
   445
  Isabelle enter a special process wrapper for interaction via
wenzelm@49173
   446
  Isabelle/Scala, see also @{file
wenzelm@45028
   447
  "~~/src/Pure/System/isabelle_process.scala"}.  The protocol between
wenzelm@45028
   448
  the ML and JVM process is private to the implementation.
wenzelm@28215
   449
wenzelm@28215
   450
  \medskip The @{verbatim "-S"} option makes the Isabelle process more
wenzelm@28215
   451
  secure by disabling some critical operations, notably runtime
wenzelm@28215
   452
  compilation and evaluation of ML source code.
wenzelm@28215
   453
*}
wenzelm@28215
   454
wenzelm@28215
   455
wenzelm@28223
   456
subsubsection {* Examples *}
wenzelm@28215
   457
wenzelm@28215
   458
text {*
wenzelm@28215
   459
  Run an interactive session of the default object-logic (as specified
wenzelm@28215
   460
  by the @{setting ISABELLE_LOGIC} setting) like this:
wenzelm@28215
   461
\begin{ttbox}
wenzelm@56439
   462
isabelle_process
wenzelm@28215
   463
\end{ttbox}
wenzelm@28215
   464
wenzelm@28215
   465
  Usually @{setting ISABELLE_LOGIC} refers to one of the standard
wenzelm@28215
   466
  logic images, which are read-only by default.  A writable session
wenzelm@47823
   467
  --- based on @{verbatim HOL}, but output to @{verbatim Test} (in the
wenzelm@28238
   468
  directory specified by the @{setting ISABELLE_OUTPUT} setting) ---
wenzelm@28215
   469
  may be invoked as follows:
wenzelm@28215
   470
\begin{ttbox}
wenzelm@56439
   471
isabelle_process HOL Test
wenzelm@28215
   472
\end{ttbox}
wenzelm@28215
   473
  Ending this session normally (e.g.\ by typing control-D) dumps the
wenzelm@47823
   474
  whole ML system state into @{verbatim Test} (be prepared for more
wenzelm@47823
   475
  than 100\,MB):
wenzelm@28215
   476
wenzelm@47823
   477
  The @{verbatim Test} session may be continued later (still in
wenzelm@28215
   478
  writable state) by:
wenzelm@28215
   479
\begin{ttbox}
wenzelm@56439
   480
isabelle_process Test
wenzelm@28215
   481
\end{ttbox}
wenzelm@47823
   482
  A read-only @{verbatim Test} session may be started by:
wenzelm@28215
   483
\begin{ttbox}
wenzelm@56439
   484
isabelle_process -r Test
wenzelm@28215
   485
\end{ttbox}
wenzelm@28215
   486
wenzelm@28238
   487
  \bigskip The next example demonstrates batch execution of Isabelle.
wenzelm@47823
   488
  We retrieve the @{verbatim Main} theory value from the theory loader
wenzelm@47823
   489
  within ML (observe the delicate quoting rules for the Bash shell
wenzelm@47823
   490
  vs.\ ML):
wenzelm@28215
   491
\begin{ttbox}
wenzelm@56439
   492
isabelle_process -e 'Thy_Info.get_theory "Main";' -q -r HOL
wenzelm@28215
   493
\end{ttbox}
wenzelm@28215
   494
  Note that the output text will be interspersed with additional junk
wenzelm@28238
   495
  messages by the ML runtime environment.  The @{verbatim "-W"} option
wenzelm@28238
   496
  allows to communicate with the Isabelle process via an external
wenzelm@28238
   497
  program in a more robust fashion.
wenzelm@28238
   498
*}
wenzelm@28238
   499
wenzelm@28238
   500
wenzelm@48813
   501
section {* The Isabelle tool wrapper \label{sec:isabelle-tool} *}
wenzelm@28238
   502
wenzelm@28238
   503
text {*
wenzelm@28238
   504
  All Isabelle related tools and interfaces are called via a common
wenzelm@28504
   505
  wrapper --- @{executable isabelle}:
wenzelm@28238
   506
wenzelm@28238
   507
\begin{ttbox}
wenzelm@28504
   508
Usage: isabelle TOOL [ARGS ...]
wenzelm@28238
   509
wenzelm@28506
   510
  Start Isabelle tool NAME with ARGS; pass "-?" for tool specific help.
wenzelm@28238
   511
wenzelm@48858
   512
Available tools:
wenzelm@48858
   513
  \dots
wenzelm@28238
   514
\end{ttbox}
wenzelm@28238
   515
wenzelm@28238
   516
  In principle, Isabelle tools are ordinary executable scripts that
wenzelm@28238
   517
  are run within the Isabelle settings environment, see
wenzelm@28238
   518
  \secref{sec:settings}.  The set of available tools is collected by
wenzelm@28504
   519
  @{executable isabelle} from the directories listed in the @{setting
wenzelm@28238
   520
  ISABELLE_TOOLS} setting.  Do not try to call the scripts directly
wenzelm@28238
   521
  from the shell.  Neither should you add the tool directories to your
wenzelm@28238
   522
  shell's search path!
wenzelm@28238
   523
*}
wenzelm@28238
   524
wenzelm@28238
   525
wenzelm@28238
   526
subsubsection {* Examples *}
wenzelm@28238
   527
wenzelm@48813
   528
text {* Show the list of available documentation of the Isabelle
wenzelm@48813
   529
  distribution:
wenzelm@28238
   530
wenzelm@28238
   531
\begin{ttbox}
wenzelm@28504
   532
  isabelle doc
wenzelm@28238
   533
\end{ttbox}
wenzelm@28238
   534
wenzelm@28238
   535
  View a certain document as follows:
wenzelm@28238
   536
\begin{ttbox}
wenzelm@47823
   537
  isabelle doc system
wenzelm@28238
   538
\end{ttbox}
wenzelm@28238
   539
wenzelm@48813
   540
  Query the Isabelle settings environment:
wenzelm@28238
   541
\begin{ttbox}
wenzelm@48813
   542
  isabelle getenv ISABELLE_HOME_USER
wenzelm@28238
   543
\end{ttbox}
wenzelm@28215
   544
*}
wenzelm@28215
   545
wenzelm@28223
   546
end