src/Doc/System/Misc.thy
author wenzelm
Fri May 17 19:04:52 2013 +0200 (2013-05-17)
changeset 52056 fc458f304f93
parent 52052 892061142ba6
child 52444 2cfe6656d6d6
permissions -rw-r--r--
added isabelle-process option -o;
wenzelm@28224
     1
theory Misc
wenzelm@43564
     2
imports Base
wenzelm@28224
     3
begin
wenzelm@28224
     4
wenzelm@28224
     5
chapter {* Miscellaneous tools \label{ch:tools} *}
wenzelm@28224
     6
wenzelm@28224
     7
text {*
wenzelm@28224
     8
  Subsequently we describe various Isabelle related utilities, given
wenzelm@28224
     9
  in alphabetical order.
wenzelm@28224
    10
*}
wenzelm@28224
    11
wenzelm@28224
    12
wenzelm@48844
    13
section {* Resolving Isabelle components \label{sec:tool-components} *}
wenzelm@48844
    14
wenzelm@48844
    15
text {*
wenzelm@48844
    16
  The @{tool_def components} tool resolves Isabelle components:
wenzelm@48844
    17
\begin{ttbox}
wenzelm@48844
    18
Usage: isabelle components [OPTIONS] [COMPONENTS ...]
wenzelm@48844
    19
wenzelm@48844
    20
  Options are:
wenzelm@50653
    21
    -I           init user settings
wenzelm@48844
    22
    -R URL       component repository
wenzelm@48844
    23
                 (default $ISABELLE_COMPONENT_REPOSITORY)
wenzelm@48844
    24
    -a           all missing components
wenzelm@48844
    25
    -l           list status
wenzelm@48844
    26
wenzelm@48844
    27
  Resolve Isabelle components via download and installation.
wenzelm@48844
    28
  COMPONENTS are identified via base name.
wenzelm@48844
    29
wenzelm@48844
    30
  ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
wenzelm@48844
    31
\end{ttbox}
wenzelm@48844
    32
wenzelm@48844
    33
  Components are initialized as described in \secref{sec:components}
wenzelm@48844
    34
  in a permissive manner, which can mark components as ``missing''.
wenzelm@48844
    35
  This state is amended by letting @{tool "components"} download and
wenzelm@48844
    36
  unpack components that are published on the default component
wenzelm@48844
    37
  repository \url{http://isabelle.in.tum.de/components/} in
wenzelm@48844
    38
  particular.
wenzelm@48844
    39
wenzelm@48844
    40
  Option @{verbatim "-R"} specifies an alternative component
wenzelm@48844
    41
  repository.  Note that @{verbatim "file:///"} URLs can be used for
wenzelm@48844
    42
  local directories.
wenzelm@48844
    43
wenzelm@48844
    44
  Option @{verbatim "-a"} selects all missing components to be
wenzelm@48844
    45
  installed.  Explicit components may be named as command
wenzelm@48844
    46
  line-arguments as well.  Note that components are uniquely
wenzelm@48844
    47
  identified by their base name, while the installation takes place in
wenzelm@48844
    48
  the location that was specified in the attempt to initialize the
wenzelm@48844
    49
  component before.
wenzelm@48844
    50
wenzelm@48844
    51
  Option @{verbatim "-l"} lists the current state of available and
wenzelm@48844
    52
  missing components with their location (full name) within the
wenzelm@50653
    53
  file-system.
wenzelm@50653
    54
wenzelm@50653
    55
  Option @{verbatim "-I"} initializes the user settings file to
wenzelm@50653
    56
  subscribe to the standard components specified in the Isabelle
wenzelm@50653
    57
  repository clone --- this does not make any sense for regular
wenzelm@50653
    58
  Isabelle releases.  If the file already exists, it needs to be
wenzelm@50653
    59
  edited manually according to the printed explanation.
wenzelm@50653
    60
*}
wenzelm@48844
    61
wenzelm@48844
    62
wenzelm@28224
    63
section {* Displaying documents *}
wenzelm@28224
    64
wenzelm@48602
    65
text {* The @{tool_def display} tool displays documents in DVI or PDF
wenzelm@28224
    66
  format:
wenzelm@28224
    67
\begin{ttbox}
wenzelm@48602
    68
Usage: isabelle display [OPTIONS] FILE
wenzelm@28224
    69
wenzelm@28224
    70
  Options are:
wenzelm@28224
    71
    -c           cleanup -- remove FILE after use
wenzelm@28224
    72
wenzelm@28224
    73
  Display document FILE (in DVI format).
wenzelm@28224
    74
\end{ttbox}
wenzelm@28224
    75
wenzelm@28224
    76
  \medskip The @{verbatim "-c"} option causes the input file to be
wenzelm@28224
    77
  removed after use.  The program for viewing @{verbatim dvi} files is
wenzelm@28224
    78
  determined by the @{setting DVI_VIEWER} setting.
wenzelm@28224
    79
*}
wenzelm@28224
    80
wenzelm@28224
    81
wenzelm@28224
    82
section {* Viewing documentation \label{sec:tool-doc} *}
wenzelm@28224
    83
wenzelm@28224
    84
text {*
wenzelm@48602
    85
  The @{tool_def doc} tool displays online documentation:
wenzelm@28224
    86
\begin{ttbox}
wenzelm@48602
    87
Usage: isabelle doc [DOC]
wenzelm@28224
    88
wenzelm@28224
    89
  View Isabelle documentation DOC, or show list of available documents.
wenzelm@28224
    90
\end{ttbox}
wenzelm@28224
    91
  If called without arguments, it lists all available documents. Each
wenzelm@28224
    92
  line starts with an identifier, followed by a short description. Any
wenzelm@28224
    93
  of these identifiers may be specified as the first argument in order
wenzelm@28224
    94
  to have the corresponding document displayed.
wenzelm@28224
    95
wenzelm@28224
    96
  \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
wenzelm@28224
    97
  directories (separated by colons) to be scanned for documentations.
wenzelm@28224
    98
  The program for viewing @{verbatim dvi} files is determined by the
wenzelm@28224
    99
  @{setting DVI_VIEWER} setting.
wenzelm@28224
   100
*}
wenzelm@28224
   101
wenzelm@28224
   102
wenzelm@47828
   103
section {* Shell commands within the settings environment \label{sec:tool-env} *}
wenzelm@47828
   104
wenzelm@48602
   105
text {* The @{tool_def env} tool is a direct wrapper for the standard
wenzelm@48602
   106
  @{verbatim "/usr/bin/env"} command on POSIX systems, running within
wenzelm@48602
   107
  the Isabelle settings environment (\secref{sec:settings}).
wenzelm@47828
   108
wenzelm@47828
   109
  The command-line arguments are that of the underlying version of
wenzelm@47828
   110
  @{verbatim env}.  For example, the following invokes an instance of
wenzelm@47828
   111
  the GNU Bash shell within the Isabelle environment:
wenzelm@47828
   112
\begin{alltt}
wenzelm@47828
   113
  isabelle env bash
wenzelm@47828
   114
\end{alltt}
wenzelm@47828
   115
*}
wenzelm@47828
   116
wenzelm@47828
   117
wenzelm@28224
   118
section {* Getting logic images *}
wenzelm@28224
   119
wenzelm@48602
   120
text {* The @{tool_def findlogics} tool traverses all directories
wenzelm@28224
   121
  specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
wenzelm@28224
   122
  images. Its usage is:
wenzelm@28224
   123
\begin{ttbox}
wenzelm@48577
   124
Usage: isabelle findlogics
wenzelm@28224
   125
wenzelm@28224
   126
  Collect heap file names from ISABELLE_PATH.
wenzelm@28224
   127
\end{ttbox}
wenzelm@28224
   128
wenzelm@28224
   129
  The base names of all files found on the path are printed --- sorted
wenzelm@28224
   130
  and with duplicates removed. Also note that lookup in @{setting
wenzelm@28224
   131
  ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
wenzelm@28224
   132
  and @{setting ML_PLATFORM}. Thus switching to another ML compiler
wenzelm@28224
   133
  may change the set of logic images available.
wenzelm@28224
   134
*}
wenzelm@28224
   135
wenzelm@28224
   136
wenzelm@28224
   137
section {* Inspecting the settings environment \label{sec:tool-getenv} *}
wenzelm@28224
   138
wenzelm@48602
   139
text {* The Isabelle settings environment --- as provided by the
wenzelm@28224
   140
  site-default and user-specific settings files --- can be inspected
wenzelm@48602
   141
  with the @{tool_def getenv} tool:
wenzelm@28224
   142
\begin{ttbox}
wenzelm@48602
   143
Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
wenzelm@28224
   144
wenzelm@28224
   145
  Options are:
wenzelm@28224
   146
    -a           display complete environment
wenzelm@28224
   147
    -b           print values only (doesn't work for -a)
wenzelm@31497
   148
    -d FILE      dump complete environment to FILE
wenzelm@31497
   149
                 (null terminated entries)
wenzelm@28224
   150
wenzelm@28224
   151
  Get value of VARNAMES from the Isabelle settings.
wenzelm@28224
   152
\end{ttbox}
wenzelm@28224
   153
wenzelm@28224
   154
  With the @{verbatim "-a"} option, one may inspect the full process
wenzelm@28224
   155
  environment that Isabelle related programs are run in. This usually
wenzelm@28224
   156
  contains much more variables than are actually Isabelle settings.
wenzelm@28224
   157
  Normally, output is a list of lines of the form @{text
wenzelm@28224
   158
  name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
wenzelm@28224
   159
  causes only the values to be printed.
wenzelm@31497
   160
wenzelm@31497
   161
  Option @{verbatim "-d"} produces a dump of the complete environment
wenzelm@31497
   162
  to the specified file.  Entries are terminated by the ASCII null
wenzelm@31497
   163
  character, i.e.\ the C string terminator.
wenzelm@28224
   164
*}
wenzelm@28224
   165
wenzelm@28224
   166
wenzelm@28224
   167
subsubsection {* Examples *}
wenzelm@28224
   168
wenzelm@48815
   169
text {* Get the location of @{setting ISABELLE_HOME_USER} where
wenzelm@48815
   170
  user-specific information is stored:
wenzelm@28224
   171
\begin{ttbox}
wenzelm@48815
   172
isabelle getenv ISABELLE_HOME_USER
wenzelm@28224
   173
\end{ttbox}
wenzelm@28224
   174
wenzelm@48815
   175
  \medskip Get the value only of the same settings variable, which is
wenzelm@48815
   176
particularly useful in shell scripts:
wenzelm@28224
   177
\begin{ttbox}
wenzelm@28504
   178
isabelle getenv -b ISABELLE_OUTPUT
wenzelm@28224
   179
\end{ttbox}
wenzelm@28224
   180
*}
wenzelm@28224
   181
wenzelm@28224
   182
wenzelm@28224
   183
section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
wenzelm@28224
   184
wenzelm@48602
   185
text {* By default, the main Isabelle binaries (@{executable
wenzelm@48602
   186
  "isabelle"} etc.)  are just run from their location within the
wenzelm@48602
   187
  distribution directory, probably indirectly by the shell through its
wenzelm@48602
   188
  @{setting PATH}.  Other schemes of installation are supported by the
wenzelm@48602
   189
  @{tool_def install} tool:
wenzelm@28224
   190
\begin{ttbox}
wenzelm@50132
   191
Usage: isabelle install [OPTIONS] BINDIR
wenzelm@28224
   192
wenzelm@28224
   193
  Options are:
wenzelm@50132
   194
    -d DISTDIR   refer to DISTDIR as Isabelle distribution
wenzelm@28224
   195
                 (default ISABELLE_HOME)
wenzelm@28224
   196
wenzelm@50132
   197
  Install Isabelle executables with absolute references to the
wenzelm@28224
   198
  distribution directory.
wenzelm@28224
   199
\end{ttbox}
wenzelm@28224
   200
wenzelm@28224
   201
  The @{verbatim "-d"} option overrides the current Isabelle
wenzelm@28224
   202
  distribution directory as determined by @{setting ISABELLE_HOME}.
wenzelm@28224
   203
wenzelm@50132
   204
  The @{text BINDIR} argument tells where executable wrapper scripts
wenzelm@50132
   205
  for @{executable "isabelle-process"} and @{executable isabelle}
wenzelm@50132
   206
  should be placed, which is typically a directory in the shell's
wenzelm@50132
   207
  @{setting PATH}, such as @{verbatim "$HOME/bin"}.
wenzelm@48815
   208
wenzelm@50132
   209
  \medskip It is also possible to make symbolic links of the main
wenzelm@50132
   210
  Isabelle executables manually, but making separate copies outside
wenzelm@50132
   211
  the Isabelle distribution directory will not work!  *}
wenzelm@28224
   212
wenzelm@28224
   213
wenzelm@28224
   214
section {* Creating instances of the Isabelle logo *}
wenzelm@28224
   215
wenzelm@49072
   216
text {* The @{tool_def logo} tool creates instances of the generic
wenzelm@49072
   217
  Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
wenzelm@28224
   218
\begin{ttbox}
wenzelm@49072
   219
Usage: isabelle logo [OPTIONS] XYZ
wenzelm@28224
   220
wenzelm@49072
   221
  Create instance XYZ of the Isabelle logo (as EPS and PDF).
wenzelm@28224
   222
wenzelm@28224
   223
  Options are:
wenzelm@49072
   224
    -n NAME      alternative output base name (default "isabelle_xyx")
wenzelm@28224
   225
    -q           quiet mode
wenzelm@28224
   226
\end{ttbox}
wenzelm@48936
   227
wenzelm@49072
   228
  Option @{verbatim "-n"} specifies an altenative (base) name for the
wenzelm@49072
   229
  generated files.  The default is @{verbatim "isabelle_"}@{text xyz}
wenzelm@49072
   230
  in lower-case.
wenzelm@48936
   231
wenzelm@48936
   232
  Option @{verbatim "-q"} omits printing of the result file name.
wenzelm@48936
   233
wenzelm@48936
   234
  \medskip Implementors of Isabelle tools and applications are
wenzelm@48936
   235
  encouraged to make derived Isabelle logos for their own projects
wenzelm@48936
   236
  using this template.  *}
wenzelm@28224
   237
wenzelm@28224
   238
wenzelm@28224
   239
section {* Printing documents *}
wenzelm@28224
   240
wenzelm@28224
   241
text {*
wenzelm@48602
   242
  The @{tool_def print} tool prints documents:
wenzelm@28224
   243
\begin{ttbox}
wenzelm@48602
   244
Usage: isabelle print [OPTIONS] FILE
wenzelm@28224
   245
wenzelm@28224
   246
  Options are:
wenzelm@28224
   247
    -c           cleanup -- remove FILE after use
wenzelm@28224
   248
wenzelm@28224
   249
  Print document FILE.
wenzelm@28224
   250
\end{ttbox}
wenzelm@28224
   251
wenzelm@28224
   252
  The @{verbatim "-c"} option causes the input file to be removed
wenzelm@28224
   253
  after use.  The printer spool command is determined by the @{setting
wenzelm@28224
   254
  PRINT_COMMAND} setting.
wenzelm@28224
   255
*}
wenzelm@28224
   256
wenzelm@28224
   257
wenzelm@28224
   258
section {* Remove awkward symbol names from theory sources *}
wenzelm@28224
   259
wenzelm@28224
   260
text {*
wenzelm@48602
   261
  The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
wenzelm@28224
   262
  improve readability for plain ASCII output (e.g.\ in email
wenzelm@28224
   263
  communication).  Most notably, @{tool unsymbolize} replaces awkward
wenzelm@28224
   264
  arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
wenzelm@28224
   265
  by @{verbatim "==>"}.
wenzelm@28224
   266
\begin{ttbox}
wenzelm@48602
   267
Usage: isabelle unsymbolize [FILES|DIRS...]
wenzelm@28224
   268
wenzelm@28224
   269
  Recursively find .thy/.ML files, removing unreadable symbol names.
wenzelm@28224
   270
  Note: this is an ad-hoc script; there is no systematic way to replace
wenzelm@28224
   271
  symbols independently of the inner syntax of a theory!
wenzelm@28224
   272
wenzelm@28224
   273
  Renames old versions of FILES by appending "~~".
wenzelm@28224
   274
\end{ttbox}
wenzelm@28224
   275
*}
wenzelm@28224
   276
wenzelm@28224
   277
wenzelm@28224
   278
section {* Output the version identifier of the Isabelle distribution *}
wenzelm@28224
   279
wenzelm@28224
   280
text {*
wenzelm@48602
   281
  The @{tool_def version} tool displays Isabelle version information:
wenzelm@41511
   282
\begin{ttbox}
wenzelm@41511
   283
Usage: isabelle version [OPTIONS]
wenzelm@41511
   284
wenzelm@41511
   285
  Options are:
wenzelm@41511
   286
    -i           short identification (derived from Mercurial id)
wenzelm@41511
   287
wenzelm@41511
   288
  Display Isabelle version information.
wenzelm@41511
   289
\end{ttbox}
wenzelm@41511
   290
wenzelm@41511
   291
  \medskip The default is to output the full version string of the
wenzelm@47827
   292
  Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}.
wenzelm@41511
   293
wenzelm@41511
   294
  The @{verbatim "-i"} option produces a short identification derived
wenzelm@41511
   295
  from the Mercurial id of the @{setting ISABELLE_HOME} directory.
wenzelm@28224
   296
*}
wenzelm@28224
   297
wenzelm@28224
   298
wenzelm@28224
   299
section {* Convert XML to YXML *}
wenzelm@28224
   300
wenzelm@28224
   301
text {*
wenzelm@28224
   302
  The @{tool_def yxml} tool converts a standard XML document (stdin)
wenzelm@28224
   303
  to the much simpler and more efficient YXML format of Isabelle
wenzelm@28224
   304
  (stdout).  The YXML format is defined as follows.
wenzelm@28224
   305
wenzelm@28224
   306
  \begin{enumerate}
wenzelm@28224
   307
wenzelm@28224
   308
  \item The encoding is always UTF-8.
wenzelm@28224
   309
wenzelm@28224
   310
  \item Body text is represented verbatim (no escaping, no special
wenzelm@28224
   311
  treatment of white space, no named entities, no CDATA chunks, no
wenzelm@28224
   312
  comments).
wenzelm@28224
   313
wenzelm@28224
   314
  \item Markup elements are represented via ASCII control characters
wenzelm@28224
   315
  @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows:
wenzelm@28224
   316
wenzelm@28224
   317
  \begin{tabular}{ll}
wenzelm@28224
   318
    XML & YXML \\\hline
wenzelm@28224
   319
    @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} &
wenzelm@28224
   320
    @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\
wenzelm@28224
   321
    @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\
wenzelm@28224
   322
  \end{tabular}
wenzelm@28224
   323
wenzelm@28224
   324
  There is no special case for empty body text, i.e.\ @{verbatim
wenzelm@28224
   325
  "<foo/>"} is treated like @{verbatim "<foo></foo>"}.  Also note that
wenzelm@28224
   326
  @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in
wenzelm@28224
   327
  well-formed XML documents.
wenzelm@28224
   328
wenzelm@28224
   329
  \end{enumerate}
wenzelm@28224
   330
wenzelm@28224
   331
  Parsing YXML is pretty straight-forward: split the text into chunks
wenzelm@28224
   332
  separated by @{text "\<^bold>X"}, then split each chunk into
wenzelm@28224
   333
  sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
wenzelm@28224
   334
  with an empty sub-chunk, and a second empty sub-chunk indicates
wenzelm@28224
   335
  close of an element.  Any other non-empty chunk consists of plain
wenzelm@44799
   336
  text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
wenzelm@44799
   337
  @{file "~~/src/Pure/PIDE/yxml.scala"}.
wenzelm@28224
   338
wenzelm@28224
   339
  YXML documents may be detected quickly by checking that the first
wenzelm@28224
   340
  two characters are @{text "\<^bold>X\<^bold>Y"}.
wenzelm@28224
   341
*}
wenzelm@28224
   342
wenzelm@28224
   343
end