doc-src/System/Thy/document/Misc.tex
author wenzelm
Sat Apr 28 17:54:50 2012 +0200 (2012-04-28)
changeset 47827 13530d774a21
parent 44799 1fd0a1276a09
child 47828 e6e1b670520b
permissions -rw-r--r--
updated system manual for release;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Misc}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Misc\isanewline
    12 \isakeyword{imports}\ Base\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Miscellaneous tools \label{ch:tools}%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \begin{isamarkuptext}%
    26 Subsequently we describe various Isabelle related utilities, given
    27   in alphabetical order.%
    28 \end{isamarkuptext}%
    29 \isamarkuptrue%
    30 %
    31 \isamarkupsection{Displaying documents%
    32 }
    33 \isamarkuptrue%
    34 %
    35 \begin{isamarkuptext}%
    36 The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatt{display}}}}} utility displays documents in DVI or PDF
    37   format:
    38 \begin{ttbox}
    39 Usage: display [OPTIONS] FILE
    40 
    41   Options are:
    42     -c           cleanup -- remove FILE after use
    43 
    44   Display document FILE (in DVI format).
    45 \end{ttbox}
    46 
    47   \medskip The \verb|-c| option causes the input file to be
    48   removed after use.  The program for viewing \verb|dvi| files is
    49   determined by the \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.%
    50 \end{isamarkuptext}%
    51 \isamarkuptrue%
    52 %
    53 \isamarkupsection{Viewing documentation \label{sec:tool-doc}%
    54 }
    55 \isamarkuptrue%
    56 %
    57 \begin{isamarkuptext}%
    58 The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatt{doc}}}}} utility displays online documentation:
    59 \begin{ttbox}
    60 Usage: doc [DOC]
    61 
    62   View Isabelle documentation DOC, or show list of available documents.
    63 \end{ttbox}
    64   If called without arguments, it lists all available documents. Each
    65   line starts with an identifier, followed by a short description. Any
    66   of these identifiers may be specified as the first argument in order
    67   to have the corresponding document displayed.
    68 
    69   \medskip The \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}DOCS}}}} setting specifies the list of
    70   directories (separated by colons) to be scanned for documentations.
    71   The program for viewing \verb|dvi| files is determined by the
    72   \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isaliteral{5F}{\isacharunderscore}}VIEWER}}}} setting.%
    73 \end{isamarkuptext}%
    74 \isamarkuptrue%
    75 %
    76 \isamarkupsection{Getting logic images%
    77 }
    78 \isamarkuptrue%
    79 %
    80 \begin{isamarkuptext}%
    81 The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatt{findlogics}}}}} utility traverses all directories
    82   specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}}, looking for Isabelle logic
    83   images. Its usage is:
    84 \begin{ttbox}
    85 Usage: findlogics
    86 
    87   Collect heap file names from ISABELLE_PATH.
    88 \end{ttbox}
    89 
    90   The base names of all files found on the path are printed --- sorted
    91   and with duplicates removed. Also note that lookup in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}PATH}}}} includes the current values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}SYSTEM}}}}
    92   and \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}PLATFORM}}}}. Thus switching to another ML compiler
    93   may change the set of logic images available.%
    94 \end{isamarkuptext}%
    95 \isamarkuptrue%
    96 %
    97 \isamarkupsection{Inspecting the settings environment \label{sec:tool-getenv}%
    98 }
    99 \isamarkuptrue%
   100 %
   101 \begin{isamarkuptext}%
   102 The Isabelle settings environment --- as provided by the
   103   site-default and user-specific settings files --- can be inspected
   104   with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}} utility:
   105 \begin{ttbox}
   106 Usage: getenv [OPTIONS] [VARNAMES ...]
   107 
   108   Options are:
   109     -a           display complete environment
   110     -b           print values only (doesn't work for -a)
   111     -d FILE      dump complete environment to FILE
   112                  (null terminated entries)
   113 
   114   Get value of VARNAMES from the Isabelle settings.
   115 \end{ttbox}
   116 
   117   With the \verb|-a| option, one may inspect the full process
   118   environment that Isabelle related programs are run in. This usually
   119   contains much more variables than are actually Isabelle settings.
   120   Normally, output is a list of lines of the form \isa{name}\verb|=|\isa{value}. The \verb|-b| option
   121   causes only the values to be printed.
   122 
   123   Option \verb|-d| produces a dump of the complete environment
   124   to the specified file.  Entries are terminated by the ASCII null
   125   character, i.e.\ the C string terminator.%
   126 \end{isamarkuptext}%
   127 \isamarkuptrue%
   128 %
   129 \isamarkupsubsubsection{Examples%
   130 }
   131 \isamarkuptrue%
   132 %
   133 \begin{isamarkuptext}%
   134 Get the ML system name and the location where the compiler binaries
   135   are supposed to reside as follows:
   136 \begin{ttbox}
   137 isabelle getenv ML_SYSTEM ML_HOME
   138 {\out ML_SYSTEM=polyml}
   139 {\out ML_HOME=/usr/share/polyml/x86-linux}
   140 \end{ttbox}
   141 
   142   The next one peeks at the output directory for Isabelle logic
   143   images:
   144 \begin{ttbox}
   145 isabelle getenv -b ISABELLE_OUTPUT
   146 {\out /home/me/isabelle/heaps/polyml_x86-linux}
   147 \end{ttbox}
   148   Here we have used the \verb|-b| option to suppress the
   149   \verb|ISABELLE_OUTPUT=| prefix.  The value above is what
   150   became of the following assignment in the default settings file:
   151 \begin{ttbox}
   152 ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps"
   153 \end{ttbox}
   154 
   155   Note how the \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isaliteral{5F}{\isacharunderscore}}IDENTIFIER}}}} value got appended
   156   automatically to each path component. This is a special feature of
   157   \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}}.%
   158 \end{isamarkuptext}%
   159 \isamarkuptrue%
   160 %
   161 \isamarkupsection{Installing standalone Isabelle executables \label{sec:tool-install}%
   162 }
   163 \isamarkuptrue%
   164 %
   165 \begin{isamarkuptext}%
   166 By default, the main Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}
   167   etc.)  are just run from their location within the distribution
   168   directory, probably indirectly by the shell through its \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}.  Other schemes of installation are supported by the
   169   \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility:
   170 \begin{ttbox}
   171 Usage: install [OPTIONS]
   172 
   173   Options are:
   174     -d DISTDIR   use DISTDIR as Isabelle distribution
   175                  (default ISABELLE_HOME)
   176     -p DIR       install standalone binaries in DIR
   177 
   178   Install Isabelle executables with absolute references to the current
   179   distribution directory.
   180 \end{ttbox}
   181 
   182   The \verb|-d| option overrides the current Isabelle
   183   distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}}.
   184 
   185   The \verb|-p| option installs executable wrapper scripts for
   186   \hyperlink{executable.isabelle-process}{\mbox{\isa{\isatt{isabelle{\isaliteral{2D}{\isacharminus}}process}}}}, \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}},
   187   \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the
   188   Isabelle distribution directory.  A typical \verb|DIR|
   189   specification would be some directory expected to be in the shell's
   190   \hyperlink{setting.PATH}{\mbox{\isa{\isatt{PATH}}}}, such as \verb|/usr/local/bin|.  It is
   191   important to note that a plain manual copy of the original Isabelle
   192   executables does not work, since it disrupts the integrity of the
   193   Isabelle distribution.%
   194 \end{isamarkuptext}%
   195 \isamarkuptrue%
   196 %
   197 \isamarkupsection{Creating instances of the Isabelle logo%
   198 }
   199 \isamarkuptrue%
   200 %
   201 \begin{isamarkuptext}%
   202 The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}} utility creates any instance of the generic
   203   Isabelle logo as an Encapsuled Postscript file (EPS):
   204 \begin{ttbox}
   205 Usage: logo [OPTIONS] NAME
   206 
   207   Create instance NAME of the Isabelle logo (as EPS).
   208 
   209   Options are:
   210     -o OUTFILE   set output file (default determined from NAME)
   211     -q           quiet mode
   212 \end{ttbox}
   213   You are encouraged to use this to create a derived logo for your
   214   Isabelle project.  For example, \verb|isabelle| \hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}~\verb|Bali| creates \verb|isabelle_bali.eps|.%
   215 \end{isamarkuptext}%
   216 \isamarkuptrue%
   217 %
   218 \isamarkupsection{Isabelle's version of make \label{sec:tool-make}%
   219 }
   220 \isamarkuptrue%
   221 %
   222 \begin{isamarkuptext}%
   223 The Isabelle \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}} utility is a very simple wrapper for
   224   ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}:
   225 \begin{ttbox}
   226 Usage: make [ARGS ...]
   227 
   228   Compile the logic in current directory using IsaMakefile.
   229   ARGS are directly passed to the system make program.
   230 \end{ttbox}
   231 
   232   Note that the Isabelle settings environment is also active. Thus one
   233   may refer to its values within the \verb|IsaMakefile|, e.g.\
   234   \verb|$(ISABELLE_OUTPUT)|. Furthermore, programs started from
   235   the make file also inherit this environment.  Typically, \verb|IsaMakefile|s defer the real work to the \indexref{}{tool}{usedir}\hyperlink{tool.usedir}{\mbox{\isa{\isatt{usedir}}}} utility.
   236 
   237   \medskip The basic \verb|IsaMakefile| convention is that the
   238   default target builds the actual logic, including its parents if
   239   appropriate.  The \verb|images| target is intended to build all
   240   local logic images, while the \verb|test| target shall build
   241   all related examples.  The \verb|all| target shall do
   242   \verb|images| and \verb|test|.%
   243 \end{isamarkuptext}%
   244 \isamarkuptrue%
   245 %
   246 \isamarkupsubsubsection{Examples%
   247 }
   248 \isamarkuptrue%
   249 %
   250 \begin{isamarkuptext}%
   251 Refer to the \verb|IsaMakefile|s of the Isabelle distribution's
   252   object-logics as a model for your own developments.  For example,
   253   see \verb|~~/src/FOL/IsaMakefile|.%
   254 \end{isamarkuptext}%
   255 \isamarkuptrue%
   256 %
   257 \isamarkupsection{Make all logics%
   258 }
   259 \isamarkuptrue%
   260 %
   261 \begin{isamarkuptext}%
   262 The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to any
   263   Isabelle component (cf.\ \secref{sec:components}) that contains an
   264   \verb|IsaMakefile|:
   265 \begin{ttbox}
   266 Usage: makeall [ARGS ...]
   267 
   268   Apply isabelle make to all components with IsaMakefile (passing ARGS).
   269 \end{ttbox}
   270 
   271   The arguments \verb|ARGS| are just passed verbatim to each
   272   \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} invocation.%
   273 \end{isamarkuptext}%
   274 \isamarkuptrue%
   275 %
   276 \isamarkupsection{Printing documents%
   277 }
   278 \isamarkuptrue%
   279 %
   280 \begin{isamarkuptext}%
   281 The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatt{print}}}}} utility prints documents:
   282 \begin{ttbox}
   283 Usage: print [OPTIONS] FILE
   284 
   285   Options are:
   286     -c           cleanup -- remove FILE after use
   287 
   288   Print document FILE.
   289 \end{ttbox}
   290 
   291   The \verb|-c| option causes the input file to be removed
   292   after use.  The printer spool command is determined by the \hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isaliteral{5F}{\isacharunderscore}}COMMAND}}}} setting.%
   293 \end{isamarkuptext}%
   294 \isamarkuptrue%
   295 %
   296 \isamarkupsection{Remove awkward symbol names from theory sources%
   297 }
   298 \isamarkuptrue%
   299 %
   300 \begin{isamarkuptext}%
   301 The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}}} utility tunes Isabelle theory sources to
   302   improve readability for plain ASCII output (e.g.\ in email
   303   communication).  Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}} replaces awkward
   304   arrow symbols such as \verb|\|\verb|<Longrightarrow>|
   305   by \verb|==>|.
   306 \begin{ttbox}
   307 Usage: unsymbolize [FILES|DIRS...]
   308 
   309   Recursively find .thy/.ML files, removing unreadable symbol names.
   310   Note: this is an ad-hoc script; there is no systematic way to replace
   311   symbols independently of the inner syntax of a theory!
   312 
   313   Renames old versions of FILES by appending "~~".
   314 \end{ttbox}%
   315 \end{isamarkuptext}%
   316 \isamarkuptrue%
   317 %
   318 \isamarkupsection{Output the version identifier of the Isabelle distribution%
   319 }
   320 \isamarkuptrue%
   321 %
   322 \begin{isamarkuptext}%
   323 The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility displays Isabelle version information:
   324 \begin{ttbox}
   325 Usage: isabelle version [OPTIONS]
   326 
   327   Options are:
   328     -i           short identification (derived from Mercurial id)
   329 
   330   Display Isabelle version information.
   331 \end{ttbox}
   332 
   333   \medskip The default is to output the full version string of the
   334   Isabelle distribution, e.g.\ ``\verb|Isabelle2012: May 2012|.
   335 
   336   The \verb|-i| option produces a short identification derived
   337   from the Mercurial id of the \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME}}}} directory.%
   338 \end{isamarkuptext}%
   339 \isamarkuptrue%
   340 %
   341 \isamarkupsection{Convert XML to YXML%
   342 }
   343 \isamarkuptrue%
   344 %
   345 \begin{isamarkuptext}%
   346 The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatt{yxml}}}}} tool converts a standard XML document (stdin)
   347   to the much simpler and more efficient YXML format of Isabelle
   348   (stdout).  The YXML format is defined as follows.
   349 
   350   \begin{enumerate}
   351 
   352   \item The encoding is always UTF-8.
   353 
   354   \item Body text is represented verbatim (no escaping, no special
   355   treatment of white space, no named entities, no CDATA chunks, no
   356   comments).
   357 
   358   \item Markup elements are represented via ASCII control characters
   359   \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{5}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isaliteral{22}{\isachardoublequote}}} as follows:
   360 
   361   \begin{tabular}{ll}
   362     XML & YXML \\\hline
   363     \verb|<|\isa{{\isaliteral{22}{\isachardoublequote}}name\ attribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{22}{\isachardoublequote}}}\verb|>| &
   364     \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yname\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Yattribute{\isaliteral{22}{\isachardoublequote}}}\verb|=|\isa{{\isaliteral{22}{\isachardoublequote}}value{\isaliteral{5C3C646F74733E}{\isasymdots}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\
   365     \verb|</|\isa{name}\verb|>| & \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} \\
   366   \end{tabular}
   367 
   368   There is no special case for empty body text, i.e.\ \verb|<foo/>| is treated like \verb|<foo></foo>|.  Also note that
   369   \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}} may never occur in
   370   well-formed XML documents.
   371 
   372   \end{enumerate}
   373 
   374   Parsing YXML is pretty straight-forward: split the text into chunks
   375   separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X{\isaliteral{22}{\isachardoublequote}}}, then split each chunk into
   376   sub-chunks separated by \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.  Markup chunks start
   377   with an empty sub-chunk, and a second empty sub-chunk indicates
   378   close of an element.  Any other non-empty chunk consists of plain
   379   text.  For example, see \verb|~~/src/Pure/PIDE/yxml.ML| or
   380   \verb|~~/src/Pure/PIDE/yxml.scala|.
   381 
   382   YXML documents may be detected quickly by checking that the first
   383   two characters are \isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E626F6C643E}{}\isactrlbold X\isaliteral{5C3C5E626F6C643E}{}\isactrlbold Y{\isaliteral{22}{\isachardoublequote}}}.%
   384 \end{isamarkuptext}%
   385 \isamarkuptrue%
   386 %
   387 \isadelimtheory
   388 %
   389 \endisadelimtheory
   390 %
   391 \isatagtheory
   392 \isacommand{end}\isamarkupfalse%
   393 %
   394 \endisatagtheory
   395 {\isafoldtheory}%
   396 %
   397 \isadelimtheory
   398 %
   399 \endisadelimtheory
   400 \end{isabellebody}%
   401 %%% Local Variables:
   402 %%% mode: latex
   403 %%% TeX-master: "root"
   404 %%% End: