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