src/Doc/System/Environment.thy
author wenzelm
Wed Oct 04 12:00:53 2017 +0200 (6 months ago)
changeset 66787 64b47495676d
parent 66785 6fbd7fc824a9
child 66789 feb36b73a7f0
permissions -rw-r--r--
obsolete;
wenzelm@62643
     1
     (*:maxLineLen=78:*)
wenzelm@61575
     2
wenzelm@62640
     3
theory Environment
wenzelm@43564
     4
imports Base
wenzelm@28215
     5
begin
wenzelm@28215
     6
wenzelm@58618
     7
chapter \<open>The Isabelle system environment\<close>
wenzelm@28215
     8
wenzelm@61575
     9
text \<open>
wenzelm@62588
    10
  This manual describes Isabelle together with related tools as seen from a
wenzelm@62588
    11
  system oriented view. See also the \<^emph>\<open>Isabelle/Isar Reference Manual\<close> @{cite
wenzelm@62588
    12
  "isabelle-isar-ref"} for the actual Isabelle input language and related
wenzelm@62588
    13
  concepts, and \<^emph>\<open>The Isabelle/Isar Implementation Manual\<close> @{cite
wenzelm@62588
    14
  "isabelle-implementation"} for the main concepts of the underlying
wenzelm@62588
    15
  implementation in Isabelle/ML.
wenzelm@58618
    16
\<close>
wenzelm@28215
    17
wenzelm@28215
    18
wenzelm@58618
    19
section \<open>Isabelle settings \label{sec:settings}\<close>
wenzelm@28215
    20
wenzelm@58618
    21
text \<open>
wenzelm@62588
    22
  Isabelle executables may depend on the \<^emph>\<open>Isabelle settings\<close> within the
wenzelm@62588
    23
  process environment. This is a statically scoped collection of environment
wenzelm@62013
    24
  variables, such as @{setting ISABELLE_HOME}, @{setting ML_SYSTEM}, @{setting
wenzelm@62013
    25
  ML_HOME}. These variables are \<^emph>\<open>not\<close> intended to be set directly from the
wenzelm@62588
    26
  shell, but are provided by Isabelle \<^emph>\<open>components\<close> their \<^emph>\<open>settings files\<close> as
wenzelm@62588
    27
  explained below.
wenzelm@58618
    28
\<close>
wenzelm@28215
    29
wenzelm@28215
    30
wenzelm@58618
    31
subsection \<open>Bootstrapping the environment \label{sec:boot}\<close>
wenzelm@28215
    32
wenzelm@61575
    33
text \<open>
wenzelm@61575
    34
  Isabelle executables need to be run within a proper settings environment.
wenzelm@61575
    35
  This is bootstrapped as described below, on the first invocation of one of
wenzelm@61575
    36
  the outer wrapper scripts (such as @{executable_ref isabelle}). This happens
wenzelm@61575
    37
  only once for each process tree, i.e.\ the environment is passed to
wenzelm@61575
    38
  subprocesses according to regular Unix conventions.
wenzelm@28215
    39
wenzelm@61575
    40
    \<^enum> The special variable @{setting_def ISABELLE_HOME} is determined
wenzelm@61575
    41
    automatically from the location of the binary that has been run.
wenzelm@28238
    42
wenzelm@61575
    43
    You should not try to set @{setting ISABELLE_HOME} manually. Also note
wenzelm@61575
    44
    that the Isabelle executables either have to be run from their original
wenzelm@61575
    45
    location in the distribution directory, or via the executable objects
wenzelm@61575
    46
    created by the @{tool install} tool. Symbolic links are admissible, but a
wenzelm@63680
    47
    plain copy of the \<^dir>\<open>$ISABELLE_HOME/bin\<close> files will not work!
wenzelm@61458
    48
wenzelm@63680
    49
    \<^enum> The file \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> is run as a @{executable_ref
wenzelm@63680
    50
    bash} shell script with the auto-export option for variables enabled.
wenzelm@28215
    51
wenzelm@61575
    52
    This file holds a rather long list of shell variable assignments, thus
wenzelm@61575
    53
    providing the site-wide default settings. The Isabelle distribution
wenzelm@61575
    54
    already contains a global settings file with sensible defaults for most
wenzelm@61575
    55
    variables. When installing the system, only a few of these may have to be
wenzelm@61575
    56
    adapted (probably @{setting ML_SYSTEM} etc.).
wenzelm@61575
    57
wenzelm@63669
    58
    \<^enum> The file @{path "$ISABELLE_HOME_USER/etc/settings"} (if it
wenzelm@61575
    59
    exists) is run in the same way as the site default settings. Note that the
wenzelm@61575
    60
    variable @{setting ISABELLE_HOME_USER} has already been set before ---
wenzelm@61575
    61
    usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/IsabelleXXXX\<close>.
wenzelm@61575
    62
wenzelm@61575
    63
    Thus individual users may override the site-wide defaults. Typically, a
wenzelm@61575
    64
    user settings file contains only a few lines, with some assignments that
wenzelm@63680
    65
    are actually changed. Never copy the central
wenzelm@63680
    66
    \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file!
wenzelm@61575
    67
wenzelm@61575
    68
  Since settings files are regular GNU @{executable_def bash} scripts, one may
wenzelm@61575
    69
  use complex shell commands, such as \<^verbatim>\<open>if\<close> or \<^verbatim>\<open>case\<close> statements to set
wenzelm@61575
    70
  variables depending on the system architecture or other environment
wenzelm@61575
    71
  variables. Such advanced features should be added only with great care,
wenzelm@61575
    72
  though. In particular, external environment references should be kept at a
wenzelm@28215
    73
  minimum.
wenzelm@28215
    74
wenzelm@61406
    75
  \<^medskip>
wenzelm@61406
    76
  A few variables are somewhat special:
wenzelm@28215
    77
wenzelm@62588
    78
    \<^item> @{setting_def ISABELLE_TOOL} is set automatically to the absolute path
wenzelm@62588
    79
    name of the @{executable isabelle} executables.
wenzelm@28215
    80
wenzelm@61575
    81
    \<^item> @{setting_ref ISABELLE_OUTPUT} will have the identifiers of the Isabelle
wenzelm@61575
    82
    distribution (cf.\ @{setting ISABELLE_IDENTIFIER}) and the ML system (cf.\
wenzelm@61575
    83
    @{setting ML_IDENTIFIER}) appended automatically to its value.
wenzelm@28215
    84
wenzelm@61406
    85
  \<^medskip>
wenzelm@61575
    86
  Note that the settings environment may be inspected with the @{tool getenv}
wenzelm@61575
    87
  tool. This might help to figure out the effect of complex settings scripts.
wenzelm@61575
    88
\<close>
wenzelm@28215
    89
wenzelm@28215
    90
wenzelm@58618
    91
subsection \<open>Common variables\<close>
wenzelm@28215
    92
wenzelm@58618
    93
text \<open>
wenzelm@61575
    94
  This is a reference of common Isabelle settings variables. Note that the
wenzelm@61575
    95
  list is somewhat open-ended. Third-party utilities or interfaces may add
wenzelm@61575
    96
  their own selection. Variables that are special in some sense are marked
wenzelm@61575
    97
  with \<open>\<^sup>*\<close>.
wenzelm@28215
    98
wenzelm@61575
    99
  \<^descr>[@{setting_def USER_HOME}\<open>\<^sup>*\<close>] Is the cross-platform user home directory.
wenzelm@61575
   100
  On Unix systems this is usually the same as @{setting HOME}, but on Windows
wenzelm@61575
   101
  it is the regular home directory of the user, not the one of within the
wenzelm@61575
   102
  Cygwin root file-system.\<^footnote>\<open>Cygwin itself offers another choice whether its
wenzelm@63669
   103
  HOME should point to the @{path "/home"} directory tree or the Windows user
wenzelm@63669
   104
  home.\<close>
wenzelm@47661
   105
wenzelm@61575
   106
  \<^descr>[@{setting_def ISABELLE_HOME}\<open>\<^sup>*\<close>] is the location of the top-level
wenzelm@61575
   107
  Isabelle distribution directory. This is automatically determined from the
wenzelm@61575
   108
  Isabelle executable that has been invoked. Do not attempt to set @{setting
wenzelm@61575
   109
  ISABELLE_HOME} yourself from the shell!
wenzelm@50182
   110
wenzelm@61575
   111
  \<^descr>[@{setting_def ISABELLE_HOME_USER}] is the user-specific counterpart of
wenzelm@63669
   112
  @{setting ISABELLE_HOME}. The default value is relative to @{path
wenzelm@61575
   113
  "$USER_HOME/.isabelle"}, under rare circumstances this may be changed in the
wenzelm@61575
   114
  global setting file. Typically, the @{setting ISABELLE_HOME_USER} directory
wenzelm@61575
   115
  mimics @{setting ISABELLE_HOME} to some extend. In particular, site-wide
wenzelm@61575
   116
  defaults may be overridden by a private \<^verbatim>\<open>$ISABELLE_HOME_USER/etc/settings\<close>.
wenzelm@61575
   117
wenzelm@61575
   118
  \<^descr>[@{setting_def ISABELLE_PLATFORM_FAMILY}\<open>\<^sup>*\<close>] is automatically set to the
wenzelm@61575
   119
  general platform family: \<^verbatim>\<open>linux\<close>, \<^verbatim>\<open>macos\<close>, \<^verbatim>\<open>windows\<close>. Note that
wenzelm@50182
   120
  platform-dependent tools usually need to refer to the more specific
wenzelm@50182
   121
  identification according to @{setting ISABELLE_PLATFORM}, @{setting
wenzelm@50182
   122
  ISABELLE_PLATFORM32}, @{setting ISABELLE_PLATFORM64}.
wenzelm@50182
   123
wenzelm@61575
   124
  \<^descr>[@{setting_def ISABELLE_PLATFORM}\<open>\<^sup>*\<close>] is automatically set to a symbolic
wenzelm@61575
   125
  identifier for the underlying hardware and operating system. The Isabelle
wenzelm@61575
   126
  platform identification always refers to the 32 bit variant, even this is a
wenzelm@61575
   127
  64 bit machine. Note that the ML or Java runtime may have a different idea,
wenzelm@61575
   128
  depending on which binaries are actually run.
wenzelm@36196
   129
wenzelm@61575
   130
  \<^descr>[@{setting_def ISABELLE_PLATFORM64}\<open>\<^sup>*\<close>] is similar to @{setting
wenzelm@61575
   131
  ISABELLE_PLATFORM} but refers to the proper 64 bit variant on a platform
wenzelm@61575
   132
  that supports this; the value is empty for 32 bit. Note that the following
wenzelm@61575
   133
  bash expression (including the quotes) prefers the 64 bit platform, if that
wenzelm@61575
   134
  is available:
wenzelm@47823
   135
wenzelm@61407
   136
  @{verbatim [display] \<open>"${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"\<close>}
wenzelm@36196
   137
wenzelm@62588
   138
  \<^descr>[@{setting ISABELLE_TOOL}\<open>\<^sup>*\<close>] is automatically set to the full path name
wenzelm@66787
   139
  of the @{executable isabelle} executable.
wenzelm@28215
   140
wenzelm@61575
   141
  \<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
wenzelm@66785
   142
  Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2017\<close>''.
wenzelm@61575
   143
wenzelm@61575
   144
  \<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
wenzelm@61575
   145
  ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
wenzelm@61575
   146
  specify the underlying ML system to be used for Isabelle. There is only a
wenzelm@63680
   147
  fixed set of admissable @{setting ML_SYSTEM} names (see the
wenzelm@63680
   148
  \<^file>\<open>$ISABELLE_HOME/etc/settings\<close> file of the distribution).
wenzelm@61575
   149
wenzelm@28215
   150
  The actual compiler binary will be run from the directory @{setting
wenzelm@61575
   151
  ML_HOME}, with @{setting ML_OPTIONS} as first arguments on the command line.
wenzelm@61575
   152
  The optional @{setting ML_PLATFORM} may specify the binary format of ML heap
wenzelm@61575
   153
  images, which is useful for cross-platform installations. The value of
wenzelm@61575
   154
  @{setting ML_IDENTIFIER} is automatically obtained by composing the values
wenzelm@61575
   155
  of @{setting ML_SYSTEM}, @{setting ML_PLATFORM} and the Isabelle version
wenzelm@61575
   156
  values.
wenzelm@47823
   157
wenzelm@61575
   158
  \<^descr>[@{setting_def ISABELLE_JDK_HOME}] needs to point to a full JDK (Java
wenzelm@61575
   159
  Development Kit) installation with \<^verbatim>\<open>javac\<close> and \<^verbatim>\<open>jar\<close> executables. This is
wenzelm@61575
   160
  essential for Isabelle/Scala and other JVM-based tools to work properly.
wenzelm@61575
   161
  Note that conventional \<^verbatim>\<open>JAVA_HOME\<close> usually points to the JRE (Java Runtime
wenzelm@47823
   162
  Environment), not JDK.
wenzelm@28215
   163
wenzelm@61575
   164
  \<^descr>[@{setting_def ISABELLE_PATH}] is a list of directories (separated by
wenzelm@61575
   165
  colons) where Isabelle logic images may reside. When looking up heaps files,
wenzelm@61575
   166
  the value of @{setting ML_IDENTIFIER} is appended to each component
wenzelm@61575
   167
  internally.
wenzelm@50197
   168
wenzelm@61575
   169
  \<^descr>[@{setting_def ISABELLE_OUTPUT}\<open>\<^sup>*\<close>] is a directory where output heap files
wenzelm@61575
   170
  should be stored by default. The ML system and Isabelle version identifier
wenzelm@61575
   171
  is appended here, too.
wenzelm@54683
   172
wenzelm@61575
   173
  \<^descr>[@{setting_def ISABELLE_BROWSER_INFO}] is the directory where theory
wenzelm@62013
   174
  browser information is stored as HTML and PDF (see also \secref{sec:info}).
wenzelm@63669
   175
  The default value is @{path "$ISABELLE_HOME_USER/browser_info"}.
wenzelm@61575
   176
wenzelm@61575
   177
  \<^descr>[@{setting_def ISABELLE_LOGIC}] specifies the default logic to load if none
wenzelm@61575
   178
  is given explicitely by the user. The default value is \<^verbatim>\<open>HOL\<close>.
wenzelm@61575
   179
wenzelm@62562
   180
  \<^descr>[@{setting_def ISABELLE_LINE_EDITOR}] specifies the line editor for the
wenzelm@62562
   181
  @{tool_ref console} interface.
wenzelm@62562
   182
wenzelm@61575
   183
  \<^descr>[@{setting_def ISABELLE_LATEX}, @{setting_def ISABELLE_PDFLATEX},
wenzelm@61575
   184
  @{setting_def ISABELLE_BIBTEX}] refer to {\LaTeX} related tools for Isabelle
wenzelm@61575
   185
  document preparation (see also \secref{sec:tool-latex}).
wenzelm@61575
   186
wenzelm@61575
   187
  \<^descr>[@{setting_def ISABELLE_TOOLS}] is a colon separated list of directories
wenzelm@61575
   188
  that are scanned by @{executable isabelle} for external utility programs
wenzelm@61575
   189
  (see also \secref{sec:isabelle-tool}).
wenzelm@61575
   190
wenzelm@61575
   191
  \<^descr>[@{setting_def ISABELLE_DOCS}] is a colon separated list of directories
wenzelm@61575
   192
  with documentation files.
wenzelm@61575
   193
wenzelm@61575
   194
  \<^descr>[@{setting_def PDF_VIEWER}] specifies the program to be used for displaying
wenzelm@61575
   195
  \<^verbatim>\<open>pdf\<close> files.
wenzelm@61575
   196
wenzelm@61575
   197
  \<^descr>[@{setting_def DVI_VIEWER}] specifies the program to be used for displaying
wenzelm@61575
   198
  \<^verbatim>\<open>dvi\<close> files.
wenzelm@61575
   199
wenzelm@61575
   200
  \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
wenzelm@62588
   201
  running Isabelle ML process derives an individual directory for temporary
wenzelm@62588
   202
  files.
wenzelm@58618
   203
\<close>
wenzelm@28215
   204
wenzelm@28215
   205
wenzelm@58618
   206
subsection \<open>Additional components \label{sec:components}\<close>
wenzelm@32323
   207
wenzelm@61575
   208
text \<open>
wenzelm@61575
   209
  Any directory may be registered as an explicit \<^emph>\<open>Isabelle component\<close>. The
wenzelm@61575
   210
  general layout conventions are that of the main Isabelle distribution
wenzelm@61575
   211
  itself, and the following two files (both optional) have a special meaning:
wenzelm@32323
   212
wenzelm@61575
   213
    \<^item> \<^verbatim>\<open>etc/settings\<close> holds additional settings that are initialized when
wenzelm@61575
   214
    bootstrapping the overall Isabelle environment, cf.\ \secref{sec:boot}. As
wenzelm@64509
   215
    usual, the content is interpreted as a GNU bash script. It may refer to
wenzelm@64509
   216
    the component's enclosing directory via the \<^verbatim>\<open>COMPONENT\<close> shell variable.
wenzelm@32323
   217
wenzelm@61575
   218
    For example, the following setting allows to refer to files within the
wenzelm@61575
   219
    component later on, without having to hardwire absolute paths:
wenzelm@61575
   220
    @{verbatim [display] \<open>MY_COMPONENT_HOME="$COMPONENT"\<close>}
wenzelm@32323
   221
wenzelm@61575
   222
    Components can also add to existing Isabelle settings such as
wenzelm@61575
   223
    @{setting_def ISABELLE_TOOLS}, in order to provide component-specific
wenzelm@61575
   224
    tools that can be invoked by end-users. For example:
wenzelm@61575
   225
    @{verbatim [display] \<open>ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"\<close>}
wenzelm@32323
   226
wenzelm@61575
   227
    \<^item> \<^verbatim>\<open>etc/components\<close> holds a list of further sub-components of the same
wenzelm@61575
   228
    structure. The directory specifications given here can be either absolute
wenzelm@61575
   229
    (with leading \<^verbatim>\<open>/\<close>) or relative to the component's main directory.
wenzelm@32323
   230
wenzelm@61575
   231
  The root of component initialization is @{setting ISABELLE_HOME} itself.
wenzelm@61575
   232
  After initializing all of its sub-components recursively, @{setting
wenzelm@61575
   233
  ISABELLE_HOME_USER} is included in the same manner (if that directory
wenzelm@63669
   234
  exists). This allows to install private components via @{path
wenzelm@61575
   235
  "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient
wenzelm@61575
   236
  to do that programmatically via the \<^verbatim>\<open>init_component\<close> shell function in the
wenzelm@61575
   237
  \<^verbatim>\<open>etc/settings\<close> script of \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> (or any other component
wenzelm@63669
   238
  directory). For example: @{verbatim [display] \<open>init_component
wenzelm@63669
   239
  "$HOME/screwdriver-2.0"\<close>}
wenzelm@48838
   240
wenzelm@61575
   241
  This is tolerant wrt.\ missing component directories, but might produce a
wenzelm@61575
   242
  warning.
wenzelm@48838
   243
wenzelm@61406
   244
  \<^medskip>
wenzelm@61575
   245
  More complex situations may be addressed by initializing components listed
wenzelm@61575
   246
  in a given catalog file, relatively to some base directory:
wenzelm@61407
   247
  @{verbatim [display] \<open>init_components "$HOME/my_component_store" "some_catalog_file"\<close>}
wenzelm@48838
   248
wenzelm@61575
   249
  The component directories listed in the catalog file are treated as relative
wenzelm@61575
   250
  to the given base directory.
wenzelm@48844
   251
wenzelm@61575
   252
  See also \secref{sec:tool-components} for some tool-support for resolving
wenzelm@61575
   253
  components that are formally initialized but not installed yet.
wenzelm@58618
   254
\<close>
wenzelm@32323
   255
wenzelm@32323
   256
wenzelm@62588
   257
section \<open>The Isabelle tool wrapper \label{sec:isabelle-tool}\<close>
wenzelm@28215
   258
wenzelm@58618
   259
text \<open>
wenzelm@62588
   260
  The main \<^emph>\<open>Isabelle tool wrapper\<close> provides a generic startup environment for
wenzelm@64509
   261
  Isabelle-related utilities, user interfaces, add-on applications etc. Such
wenzelm@64509
   262
  tools automatically benefit from the settings mechanism
wenzelm@64509
   263
  (\secref{sec:settings}). Moreover, this is the standard way to invoke
wenzelm@64509
   264
  Isabelle/Scala functionality as a separate operating-system process.
wenzelm@64509
   265
  Isabelle command-line tools are run uniformly via a common wrapper ---
wenzelm@64509
   266
  @{executable_ref isabelle}:
wenzelm@61407
   267
  @{verbatim [display]
wenzelm@62588
   268
\<open>Usage: isabelle TOOL [ARGS ...]
wenzelm@62588
   269
wenzelm@62829
   270
  Start Isabelle TOOL with ARGS; pass "-?" for tool-specific help.
wenzelm@62588
   271
wenzelm@62588
   272
Available tools:
wenzelm@62588
   273
  ...\<close>}
wenzelm@62588
   274
wenzelm@64509
   275
  Tools may be implemented in Isabelle/Scala or as stand-alone executables
wenzelm@64509
   276
  (usually as GNU bash scripts). In the invocation of ``@{executable
wenzelm@64509
   277
  isabelle}~\<open>tool\<close>'', the named \<open>tool\<close> is resolved as follows (and in the
wenzelm@64509
   278
  given order).
wenzelm@64509
   279
wenzelm@64509
   280
    \<^enum> An external tool found on the directories listed in the @{setting
wenzelm@64509
   281
    ISABELLE_TOOLS} settings variable (colon-separated list in standard POSIX
wenzelm@64509
   282
    notation).
wenzelm@64509
   283
wenzelm@64509
   284
      \<^enum> If a file ``\<open>tool\<close>\<^verbatim>\<open>.scala\<close>'' is found, the source needs to define
wenzelm@64509
   285
      some object that extends the class \<^verbatim>\<open>Isabelle_Tool.Body\<close>. The Scala
wenzelm@64509
   286
      compiler is invoked on the spot (which may take some time), and the body
wenzelm@64509
   287
      function is run with the command-line arguments as \<^verbatim>\<open>List[String]\<close>.
wenzelm@64509
   288
wenzelm@64509
   289
      \<^enum> If an executable file ``\<open>tool\<close>'' is found, it is invoked as
wenzelm@64509
   290
      stand-alone program with the command-line arguments provided as \<^verbatim>\<open>argv\<close>
wenzelm@64509
   291
      array.
wenzelm@64509
   292
wenzelm@64509
   293
    \<^enum> An internal tool that is registered in \<^verbatim>\<open>Isabelle_Tool.internal_tools\<close>
wenzelm@64509
   294
    within the Isabelle/Scala namespace of \<^verbatim>\<open>Pure.jar\<close>. This is the preferred
wenzelm@64509
   295
    entry-point for high-end tools implemented in Isabelle/Scala --- compiled
wenzelm@64509
   296
    once when the Isabelle distribution is built. These tools are provided by
wenzelm@64509
   297
    Isabelle/Pure and cannot be augmented in user-space.
wenzelm@64509
   298
wenzelm@64509
   299
  There are also some administrative tools that are available from a bare
wenzelm@64509
   300
  repository clone of Isabelle, but not in regular distributions.
wenzelm@62588
   301
\<close>
wenzelm@62588
   302
wenzelm@62588
   303
wenzelm@62588
   304
subsubsection \<open>Examples\<close>
wenzelm@62588
   305
wenzelm@62588
   306
text \<open>
wenzelm@62588
   307
  Show the list of available documentation of the Isabelle distribution:
wenzelm@62588
   308
  @{verbatim [display] \<open>isabelle doc\<close>}
wenzelm@62588
   309
wenzelm@62588
   310
  View a certain document as follows:
wenzelm@62588
   311
  @{verbatim [display] \<open>isabelle doc system\<close>}
wenzelm@62588
   312
wenzelm@62588
   313
  Query the Isabelle settings environment:
wenzelm@62588
   314
  @{verbatim [display] \<open>isabelle getenv ISABELLE_HOME_USER\<close>}
wenzelm@62588
   315
\<close>
wenzelm@62588
   316
wenzelm@62588
   317
wenzelm@62588
   318
section \<open>The raw Isabelle ML process\<close>
wenzelm@62588
   319
wenzelm@62588
   320
subsection \<open>Batch mode \label{sec:tool-process}\<close>
wenzelm@62588
   321
wenzelm@62588
   322
text \<open>
wenzelm@62588
   323
  The @{tool_def process} tool runs the raw ML process in batch mode:
wenzelm@62588
   324
  @{verbatim [display]
wenzelm@62634
   325
\<open>Usage: isabelle process [OPTIONS]
wenzelm@28215
   326
wenzelm@28215
   327
  Options are:
wenzelm@62677
   328
    -T THEORY    load theory
wenzelm@62639
   329
    -d DIR       include session directory
wenzelm@62506
   330
    -e ML_EXPR   evaluate ML expression on startup
wenzelm@62506
   331
    -f ML_FILE   evaluate ML file on startup
wenzelm@62634
   332
    -l NAME      logic session name (default ISABELLE_LOGIC="HOL")
wenzelm@28215
   333
    -m MODE      add print mode for output
wenzelm@52056
   334
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@28215
   335
wenzelm@62634
   336
  Run the raw Isabelle ML process in batch mode.\<close>}
wenzelm@28215
   337
wenzelm@62643
   338
  \<^medskip>
wenzelm@62506
   339
  Options \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> allow to evaluate ML code, before the ML process is
wenzelm@62506
   340
  started. The source is either given literally or taken from a file. Multiple
wenzelm@62506
   341
  \<^verbatim>\<open>-e\<close> and \<^verbatim>\<open>-f\<close> options are evaluated in the given order. Errors lead to
wenzelm@62506
   342
  premature exit of the ML process with return code 1.
wenzelm@28215
   343
wenzelm@61406
   344
  \<^medskip>
wenzelm@62677
   345
  Option \<^verbatim>\<open>-T\<close> loads a specified theory file. This is a wrapper for \<^verbatim>\<open>-e\<close> with
wenzelm@62677
   346
  a suitable @{ML use_thy} invocation.
wenzelm@62677
   347
wenzelm@62677
   348
  \<^medskip>
wenzelm@62639
   349
  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. Option \<^verbatim>\<open>-d\<close> specifies
wenzelm@62639
   350
  additional directories for session roots, see also \secref{sec:tool-build}.
wenzelm@62634
   351
wenzelm@62634
   352
  \<^medskip>
wenzelm@61575
   353
  The \<^verbatim>\<open>-m\<close> option adds identifiers of print modes to be made active for this
wenzelm@62573
   354
  session. For example, \<^verbatim>\<open>-m ASCII\<close> prefers ASCII replacement syntax over
wenzelm@62573
   355
  mathematical Isabelle symbols.
wenzelm@28215
   356
wenzelm@61406
   357
  \<^medskip>
wenzelm@61575
   358
  Option \<^verbatim>\<open>-o\<close> allows to override Isabelle system options for this process,
wenzelm@62573
   359
  see also \secref{sec:system-options}.
wenzelm@58618
   360
\<close>
wenzelm@28215
   361
wenzelm@28215
   362
wenzelm@62588
   363
subsubsection \<open>Example\<close>
wenzelm@28215
   364
wenzelm@58618
   365
text \<open>
wenzelm@62588
   366
  The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
wenzelm@62588
   367
  loader within ML:
wenzelm@62634
   368
  @{verbatim [display] \<open>isabelle process -e 'Thy_Info.get_theory "Main"'\<close>}
wenzelm@62588
   369
wenzelm@64509
   370
  Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
wenzelm@62588
   371
  Isabelle/ML and Scala libraries provide functions for that, but here we need
wenzelm@62588
   372
  to do it manually.
wenzelm@58618
   373
\<close>
wenzelm@28238
   374
wenzelm@28238
   375
wenzelm@62588
   376
subsection \<open>Interactive mode\<close>
wenzelm@28238
   377
wenzelm@58618
   378
text \<open>
wenzelm@62588
   379
  The @{tool_def console} tool runs the raw ML process with interactive
wenzelm@62588
   380
  console and line editor:
wenzelm@61407
   381
  @{verbatim [display]
wenzelm@62588
   382
\<open>Usage: isabelle console [OPTIONS]
wenzelm@28238
   383
wenzelm@62588
   384
  Options are:
wenzelm@62588
   385
    -d DIR       include session directory
wenzelm@62588
   386
    -l NAME      logic session name (default ISABELLE_LOGIC)
wenzelm@62588
   387
    -m MODE      add print mode for output
wenzelm@62588
   388
    -n           no build of session image on startup
wenzelm@62588
   389
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@62643
   390
    -r           bootstrap from raw Poly/ML
wenzelm@62588
   391
    -s           system build mode for session image
wenzelm@28238
   392
wenzelm@62588
   393
  Build a logic session image and run the raw Isabelle ML process
wenzelm@62588
   394
  in interactive mode, with line editor ISABELLE_LINE_EDITOR.\<close>}
wenzelm@28238
   395
wenzelm@62643
   396
  \<^medskip>
wenzelm@62588
   397
  Option \<^verbatim>\<open>-l\<close> specifies the logic session name. By default, its heap image is
wenzelm@62643
   398
  checked and built on demand, but the option \<^verbatim>\<open>-n\<close> skips that.
wenzelm@28238
   399
wenzelm@62643
   400
  Option \<^verbatim>\<open>-r\<close> indicates a bootstrap from the raw Poly/ML system, which is
wenzelm@62643
   401
  relevant for Isabelle/Pure development.
wenzelm@62643
   402
wenzelm@62643
   403
  \<^medskip>
wenzelm@62639
   404
  Options \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-m\<close>, \<^verbatim>\<open>-o\<close> have the same meaning as for @{tool process}
wenzelm@62639
   405
  (\secref{sec:tool-process}).
wenzelm@62639
   406
wenzelm@62639
   407
  Option \<^verbatim>\<open>-s\<close> has the same meaning as for @{tool build}
wenzelm@62588
   408
  (\secref{sec:tool-build}).
wenzelm@28238
   409
wenzelm@62588
   410
  \<^medskip>
wenzelm@62588
   411
  The Isabelle/ML process is run through the line editor that is specified via
wenzelm@62588
   412
  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
wenzelm@62588
   413
  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
wenzelm@62588
   414
  standard input/output.
wenzelm@28238
   415
wenzelm@62588
   416
  The user is connected to the raw ML toplevel loop: this is neither
wenzelm@62588
   417
  Isabelle/Isar nor Isabelle/ML within the usual formal context. The most
wenzelm@62847
   418
  relevant ML commands at this stage are @{ML use} (for ML files) and
wenzelm@62847
   419
  @{ML use_thy} (for theory files).
wenzelm@58618
   420
\<close>
wenzelm@28215
   421
wenzelm@62451
   422
wenzelm@63995
   423
section \<open>The raw Isabelle Java process \label{sec:isabelle-java}\<close>
wenzelm@63995
   424
wenzelm@63995
   425
text \<open>
wenzelm@63995
   426
  The @{executable_ref isabelle_java} executable allows to run a Java process
wenzelm@63995
   427
  within the name space of Java and Scala components that are bundled with
wenzelm@63995
   428
  Isabelle, but \<^emph>\<open>without\<close> the Isabelle settings environment
wenzelm@63995
   429
  (\secref{sec:settings}).
wenzelm@63995
   430
wenzelm@63995
   431
  After such a JVM cold-start, the Isabelle environment can be accessed via
wenzelm@63995
   432
  \<^verbatim>\<open>Isabelle_System.getenv\<close> as usual, but the underlying process environment
wenzelm@63995
   433
  remains clean. This is e.g.\ relevant when invoking other processes that
wenzelm@63995
   434
  should remain separate from the current Isabelle installation.
wenzelm@63995
   435
wenzelm@63995
   436
  \<^medskip>
wenzelm@63995
   437
  Note that under normal circumstances, Isabelle command-line tools are run
wenzelm@63995
   438
  \<^emph>\<open>within\<close> the settings environment, as provided by the @{executable
wenzelm@63995
   439
  isabelle} wrapper (\secref{sec:isabelle-tool} and \secref{sec:tool-java}).
wenzelm@63995
   440
\<close>
wenzelm@63995
   441
wenzelm@63995
   442
wenzelm@63995
   443
subsubsection \<open>Example\<close>
wenzelm@63995
   444
wenzelm@63995
   445
text \<open>
wenzelm@63995
   446
  The subsequent example creates a raw Java process on the command-line and
wenzelm@63995
   447
  invokes the main Isabelle application entry point:
wenzelm@63995
   448
  @{verbatim [display] \<open>isabelle_java isabelle.Main\<close>}
wenzelm@63995
   449
\<close>
wenzelm@63995
   450
wenzelm@63995
   451
wenzelm@62451
   452
section \<open>YXML versus XML\<close>
wenzelm@62451
   453
wenzelm@62451
   454
text \<open>
wenzelm@62451
   455
  Isabelle tools often use YXML, which is a simple and efficient syntax for
wenzelm@62451
   456
  untyped XML trees. The YXML format is defined as follows.
wenzelm@62451
   457
wenzelm@62451
   458
    \<^enum> The encoding is always UTF-8.
wenzelm@62451
   459
wenzelm@62451
   460
    \<^enum> Body text is represented verbatim (no escaping, no special treatment of
wenzelm@62451
   461
    white space, no named entities, no CDATA chunks, no comments).
wenzelm@62451
   462
wenzelm@62451
   463
    \<^enum> Markup elements are represented via ASCII control characters \<open>\<^bold>X = 5\<close>
wenzelm@62451
   464
    and \<open>\<^bold>Y = 6\<close> as follows:
wenzelm@62451
   465
wenzelm@62451
   466
    \begin{tabular}{ll}
wenzelm@62451
   467
      XML & YXML \\\hline
wenzelm@62451
   468
      \<^verbatim>\<open><\<close>\<open>name attribute\<close>\<^verbatim>\<open>=\<close>\<open>value \<dots>\<close>\<^verbatim>\<open>>\<close> &
wenzelm@62451
   469
      \<open>\<^bold>X\<^bold>Yname\<^bold>Yattribute\<close>\<^verbatim>\<open>=\<close>\<open>value\<dots>\<^bold>X\<close> \\
wenzelm@62451
   470
      \<^verbatim>\<open></\<close>\<open>name\<close>\<^verbatim>\<open>>\<close> & \<open>\<^bold>X\<^bold>Y\<^bold>X\<close> \\
wenzelm@62451
   471
    \end{tabular}
wenzelm@62451
   472
wenzelm@62451
   473
    There is no special case for empty body text, i.e.\ \<^verbatim>\<open><foo/>\<close> is treated
wenzelm@62451
   474
    like \<^verbatim>\<open><foo></foo>\<close>. Also note that \<open>\<^bold>X\<close> and \<open>\<^bold>Y\<close> may never occur in
wenzelm@62451
   475
    well-formed XML documents.
wenzelm@62451
   476
wenzelm@62451
   477
  Parsing YXML is pretty straight-forward: split the text into chunks
wenzelm@62451
   478
  separated by \<open>\<^bold>X\<close>, then split each chunk into sub-chunks separated by \<open>\<^bold>Y\<close>.
wenzelm@62451
   479
  Markup chunks start with an empty sub-chunk, and a second empty sub-chunk
wenzelm@62451
   480
  indicates close of an element. Any other non-empty chunk consists of plain
wenzelm@63680
   481
  text. For example, see \<^file>\<open>~~/src/Pure/PIDE/yxml.ML\<close> or
wenzelm@63680
   482
  \<^file>\<open>~~/src/Pure/PIDE/yxml.scala\<close>.
wenzelm@62451
   483
wenzelm@62451
   484
  YXML documents may be detected quickly by checking that the first two
wenzelm@62451
   485
  characters are \<open>\<^bold>X\<^bold>Y\<close>.
wenzelm@62451
   486
\<close>
wenzelm@62451
   487
wenzelm@28223
   488
end