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