--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Doc/System/Misc.thy Tue Aug 28 18:57:32 2012 +0200
@@ -0,0 +1,598 @@
+theory Misc
+imports Base
+begin
+
+chapter {* Miscellaneous tools \label{ch:tools} *}
+
+text {*
+ Subsequently we describe various Isabelle related utilities, given
+ in alphabetical order.
+*}
+
+
+section {* Resolving Isabelle components \label{sec:tool-components} *}
+
+text {*
+ The @{tool_def components} tool resolves Isabelle components:
+\begin{ttbox}
+Usage: isabelle components [OPTIONS] [COMPONENTS ...]
+
+ Options are:
+ -R URL component repository
+ (default $ISABELLE_COMPONENT_REPOSITORY)
+ -a all missing components
+ -l list status
+
+ Resolve Isabelle components via download and installation.
+ COMPONENTS are identified via base name.
+
+ ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
+\end{ttbox}
+
+ Components are initialized as described in \secref{sec:components}
+ in a permissive manner, which can mark components as ``missing''.
+ This state is amended by letting @{tool "components"} download and
+ unpack components that are published on the default component
+ repository \url{http://isabelle.in.tum.de/components/} in
+ particular.
+
+ Option @{verbatim "-R"} specifies an alternative component
+ repository. Note that @{verbatim "file:///"} URLs can be used for
+ local directories.
+
+ Option @{verbatim "-a"} selects all missing components to be
+ installed. Explicit components may be named as command
+ line-arguments as well. Note that components are uniquely
+ identified by their base name, while the installation takes place in
+ the location that was specified in the attempt to initialize the
+ component before.
+
+ Option @{verbatim "-l"} lists the current state of available and
+ missing components with their location (full name) within the
+ file-system. *}
+
+
+section {* Displaying documents *}
+
+text {* The @{tool_def display} tool displays documents in DVI or PDF
+ format:
+\begin{ttbox}
+Usage: isabelle display [OPTIONS] FILE
+
+ Options are:
+ -c cleanup -- remove FILE after use
+
+ Display document FILE (in DVI format).
+\end{ttbox}
+
+ \medskip The @{verbatim "-c"} option causes the input file to be
+ removed after use. The program for viewing @{verbatim dvi} files is
+ determined by the @{setting DVI_VIEWER} setting.
+*}
+
+
+section {* Viewing documentation \label{sec:tool-doc} *}
+
+text {*
+ The @{tool_def doc} tool displays online documentation:
+\begin{ttbox}
+Usage: isabelle doc [DOC]
+
+ View Isabelle documentation DOC, or show list of available documents.
+\end{ttbox}
+ If called without arguments, it lists all available documents. Each
+ line starts with an identifier, followed by a short description. Any
+ of these identifiers may be specified as the first argument in order
+ to have the corresponding document displayed.
+
+ \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
+ directories (separated by colons) to be scanned for documentations.
+ The program for viewing @{verbatim dvi} files is determined by the
+ @{setting DVI_VIEWER} setting.
+*}
+
+
+section {* Shell commands within the settings environment \label{sec:tool-env} *}
+
+text {* The @{tool_def env} tool is a direct wrapper for the standard
+ @{verbatim "/usr/bin/env"} command on POSIX systems, running within
+ the Isabelle settings environment (\secref{sec:settings}).
+
+ The command-line arguments are that of the underlying version of
+ @{verbatim env}. For example, the following invokes an instance of
+ the GNU Bash shell within the Isabelle environment:
+\begin{alltt}
+ isabelle env bash
+\end{alltt}
+*}
+
+
+section {* Getting logic images *}
+
+text {* The @{tool_def findlogics} tool traverses all directories
+ specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
+ images. Its usage is:
+\begin{ttbox}
+Usage: isabelle findlogics
+
+ Collect heap file names from ISABELLE_PATH.
+\end{ttbox}
+
+ The base names of all files found on the path are printed --- sorted
+ and with duplicates removed. Also note that lookup in @{setting
+ ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
+ and @{setting ML_PLATFORM}. Thus switching to another ML compiler
+ may change the set of logic images available.
+*}
+
+
+section {* Inspecting the settings environment \label{sec:tool-getenv} *}
+
+text {* The Isabelle settings environment --- as provided by the
+ site-default and user-specific settings files --- can be inspected
+ with the @{tool_def getenv} tool:
+\begin{ttbox}
+Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
+
+ Options are:
+ -a display complete environment
+ -b print values only (doesn't work for -a)
+ -d FILE dump complete environment to FILE
+ (null terminated entries)
+
+ Get value of VARNAMES from the Isabelle settings.
+\end{ttbox}
+
+ With the @{verbatim "-a"} option, one may inspect the full process
+ environment that Isabelle related programs are run in. This usually
+ contains much more variables than are actually Isabelle settings.
+ Normally, output is a list of lines of the form @{text
+ name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
+ causes only the values to be printed.
+
+ Option @{verbatim "-d"} produces a dump of the complete environment
+ to the specified file. Entries are terminated by the ASCII null
+ character, i.e.\ the C string terminator.
+*}
+
+
+subsubsection {* Examples *}
+
+text {* Get the location of @{setting ISABELLE_HOME_USER} where
+ user-specific information is stored:
+\begin{ttbox}
+isabelle getenv ISABELLE_HOME_USER
+\end{ttbox}
+
+ \medskip Get the value only of the same settings variable, which is
+particularly useful in shell scripts:
+\begin{ttbox}
+isabelle getenv -b ISABELLE_OUTPUT
+\end{ttbox}
+*}
+
+
+section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
+
+text {* By default, the main Isabelle binaries (@{executable
+ "isabelle"} etc.) are just run from their location within the
+ distribution directory, probably indirectly by the shell through its
+ @{setting PATH}. Other schemes of installation are supported by the
+ @{tool_def install} tool:
+\begin{ttbox}
+Usage: isabelle install [OPTIONS]
+
+ Options are:
+ -d DISTDIR use DISTDIR as Isabelle distribution
+ (default ISABELLE_HOME)
+ -p DIR install standalone binaries in DIR
+
+ Install Isabelle executables with absolute references to the current
+ distribution directory.
+\end{ttbox}
+
+ The @{verbatim "-d"} option overrides the current Isabelle
+ distribution directory as determined by @{setting ISABELLE_HOME}.
+
+ The @{verbatim "-p"} option installs executable wrapper scripts for
+ @{executable "isabelle-process"}, @{executable isabelle}, containing
+ proper absolute references to the Isabelle distribution directory.
+ A typical @{verbatim DIR} specification would be some directory
+ expected to be in the shell's @{setting PATH}, such as @{verbatim
+ "$HOME/bin"}.
+
+ It is possible to make symbolic links of the main Isabelle
+ executables, but making separate copies outside the Isabelle
+ distribution directory will not work.
+*}
+
+
+section {* Creating instances of the Isabelle logo *}
+
+text {* The @{tool_def logo} tool creates any instance of the generic
+ Isabelle logo as EPS or PDF.
+\begin{ttbox}
+Usage: isabelle logo [OPTIONS] NAME
+
+ Create instance NAME of the Isabelle logo (as EPS or PDF).
+
+ Options are:
+ -o OUTFILE specify output file and format
+ (default "isabelle_name.pdf")
+ -q quiet mode
+\end{ttbox}
+
+ Option @{verbatim "-o"} specifies an explicit output file name and
+ format, e.g.\ @{verbatim "mylogo.eps"} for an EPS logo. The default
+ is @{verbatim "isabelle_"}@{text name}@{verbatim ".pdf"}, with the
+ lower-case version of the given name and PDF output.
+
+ Option @{verbatim "-q"} omits printing of the result file name.
+
+ \medskip Implementors of Isabelle tools and applications are
+ encouraged to make derived Isabelle logos for their own projects
+ using this template. *}
+
+
+section {* Isabelle wrapper for make \label{sec:tool-make} *}
+
+text {* The old @{tool_def make} tool is a very simple wrapper for
+ ordinary Unix @{executable make}:
+\begin{ttbox}
+Usage: isabelle make [ARGS ...]
+
+ Compile the logic in current directory using IsaMakefile.
+ ARGS are directly passed to the system make program.
+\end{ttbox}
+
+ Note that the Isabelle settings environment is also active. Thus one
+ may refer to its values within the @{verbatim IsaMakefile}, e.g.\
+ @{verbatim "$(ISABELLE_HOME)"}. Furthermore, programs started from
+ the make file also inherit this environment.
+*}
+
+
+section {* Creating Isabelle session directories
+ \label{sec:tool-mkdir} *}
+
+text {* The old @{tool_def mkdir} tool prepares Isabelle session
+ source directories, including a sensible default setup of @{verbatim
+ IsaMakefile}, @{verbatim ROOT.ML}, and a @{verbatim document}
+ directory with a minimal @{verbatim root.tex} that is sufficient to
+ print all theories of the session (in the order of appearance); see
+ \secref{sec:tool-document} for further information on Isabelle
+ document preparation. The usage of @{tool mkdir} is:
+
+\begin{ttbox}
+Usage: isabelle mkdir [OPTIONS] [LOGIC] NAME
+
+ Options are:
+ -I FILE alternative IsaMakefile output
+ -P include parent logic target
+ -b setup build mode (session outputs heap image)
+ -q quiet mode
+
+ Prepare session directory, including IsaMakefile and document source,
+ with parent LOGIC (default ISABELLE_LOGIC=\$ISABELLE_LOGIC)
+\end{ttbox}
+
+ The @{tool mkdir} tool is conservative in the sense that any
+ existing @{verbatim IsaMakefile} etc.\ is left unchanged. Thus it
+ is safe to invoke it multiple times, although later runs may not
+ have the desired effect.
+
+ Note that @{tool mkdir} is unable to change @{verbatim IsaMakefile}
+ incrementally --- manual changes are required for multiple
+ sub-sessions. On order to get an initial working session, the only
+ editing needed is to add appropriate @{ML use_thy} calls to the
+ generated @{verbatim ROOT.ML} file.
+*}
+
+
+subsubsection {* Options *}
+
+text {*
+ The @{verbatim "-I"} option specifies an alternative to @{verbatim
+ IsaMakefile} for dependencies. Note that ``@{verbatim "-"}'' refers
+ to \emph{stdout}, i.e.\ ``@{verbatim "-I-"}'' provides an easy way
+ to peek at @{tool mkdir}'s idea of @{tool make} setup required for
+ some particular of Isabelle session.
+
+ \medskip The @{verbatim "-P"} option includes a target for the
+ parent @{verbatim LOGIC} session in the generated @{verbatim
+ IsaMakefile}. The corresponding sources are assumed to be located
+ within the Isabelle distribution.
+
+ \medskip The @{verbatim "-b"} option sets up the current directory
+ as the base for a new session that provides an actual logic image,
+ as opposed to one that only runs several theories based on an
+ existing image. Note that in the latter case, everything except
+ @{verbatim IsaMakefile} would be placed into a separate directory
+ @{verbatim NAME}, rather than the current one. See
+ \secref{sec:tool-usedir} for further information on \emph{build
+ mode} vs.\ \emph{example mode} of @{tool usedir}.
+
+ \medskip The @{verbatim "-q"} option enables quiet mode, suppressing
+ further notes on how to proceed.
+*}
+
+
+section {* Printing documents *}
+
+text {*
+ The @{tool_def print} tool prints documents:
+\begin{ttbox}
+Usage: isabelle print [OPTIONS] FILE
+
+ Options are:
+ -c cleanup -- remove FILE after use
+
+ Print document FILE.
+\end{ttbox}
+
+ The @{verbatim "-c"} option causes the input file to be removed
+ after use. The printer spool command is determined by the @{setting
+ PRINT_COMMAND} setting.
+*}
+
+
+section {* Remove awkward symbol names from theory sources *}
+
+text {*
+ The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
+ improve readability for plain ASCII output (e.g.\ in email
+ communication). Most notably, @{tool unsymbolize} replaces awkward
+ arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
+ by @{verbatim "==>"}.
+\begin{ttbox}
+Usage: isabelle unsymbolize [FILES|DIRS...]
+
+ Recursively find .thy/.ML files, removing unreadable symbol names.
+ Note: this is an ad-hoc script; there is no systematic way to replace
+ symbols independently of the inner syntax of a theory!
+
+ Renames old versions of FILES by appending "~~".
+\end{ttbox}
+*}
+
+
+section {* Running Isabelle sessions \label{sec:tool-usedir} *}
+
+text {* The old @{tool_def usedir} tool builds object-logic images, or
+ runs example sessions based on existing logics. Its usage is:
+\begin{ttbox}
+Usage: isabelle usedir [OPTIONS] LOGIC NAME
+
+ Options are:
+ -C BOOL copy existing document directory to -D PATH (default true)
+ -D PATH dump generated document sources into PATH
+ -M MAX multithreading: maximum number of worker threads (default 1)
+ -P PATH set path for remote theory browsing information
+ -Q INT set threshold for sub-proof parallelization (default 50)
+ -T LEVEL multithreading: trace level (default 0)
+ -V VARIANT declare alternative document VARIANT
+ -b build mode (output heap image, using current dir)
+ -d FORMAT build document as FORMAT (default false)
+ -f NAME use ML file NAME (default ROOT.ML)
+ -g BOOL generate session graph image for document (default false)
+ -i BOOL generate theory browser information (default false)
+ -m MODE add print mode for output
+ -p LEVEL set level of detail for proof objects (default 0)
+ -q LEVEL set level of parallel proof checking (default 1)
+ -r reset session path
+ -s NAME override session NAME
+ -t BOOL internal session timing (default false)
+ -v BOOL be verbose (default false)
+
+ Build object-logic or run examples. Also creates browsing
+ information (HTML etc.) according to settings.
+
+ ISABELLE_USEDIR_OPTIONS=...
+
+ ML_PLATFORM=...
+ ML_HOME=...
+ ML_SYSTEM=...
+ ML_OPTIONS=...
+\end{ttbox}
+
+ Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
+ setting is implicitly prefixed to \emph{any} @{tool usedir}
+ call. Since the @{verbatim IsaMakefile}s of all object-logics
+ distributed with Isabelle just invoke @{tool usedir} for the real
+ work, one may control compilation options globally via above
+ variable. In particular, generation of \rmindex{HTML} browsing
+ information and document preparation is controlled here.
+*}
+
+
+subsubsection {* Options *}
+
+text {*
+ Basically, there are two different modes of operation: \emph{build
+ mode} (enabled through the @{verbatim "-b"} option) and
+ \emph{example mode} (default).
+
+ Calling @{tool usedir} with @{verbatim "-b"} runs @{executable
+ "isabelle-process"} with input image @{verbatim LOGIC} and output to
+ @{verbatim NAME}, as provided on the command line. This will be a
+ batch session, running @{verbatim ROOT.ML} from the current
+ directory and then quitting. It is assumed that @{verbatim ROOT.ML}
+ contains all ML commands required to build the logic.
+
+ In example mode, @{tool usedir} runs a read-only session of
+ @{verbatim LOGIC} and automatically runs @{verbatim ROOT.ML} from
+ within directory @{verbatim NAME}. It assumes that this file
+ contains appropriate ML commands to run the desired examples.
+
+ \medskip The @{verbatim "-i"} option controls theory browser data
+ generation. It may be explicitly turned on or off --- as usual, the
+ last occurrence of @{verbatim "-i"} on the command line wins.
+
+ The @{verbatim "-P"} option specifies a path (or actual URL) to be
+ prefixed to any \emph{non-local} reference of existing theories.
+ Thus user sessions may easily link to existing Isabelle libraries
+ already present on the WWW.
+
+ The @{verbatim "-m"} options specifies additional print modes to be
+ activated temporarily while the session is processed.
+
+ \medskip The @{verbatim "-d"} option controls document preparation.
+ Valid arguments are @{verbatim false} (do not prepare any document;
+ this is default), or any of @{verbatim dvi}, @{verbatim dvi.gz},
+ @{verbatim ps}, @{verbatim ps.gz}, @{verbatim pdf}. The logic
+ session has to provide a properly setup @{verbatim document}
+ directory. See \secref{sec:tool-document} and
+ \secref{sec:tool-latex} for more details.
+
+ \medskip The @{verbatim "-V"} option declares alternative document
+ variants, consisting of name/tags pairs (cf.\ options @{verbatim
+ "-n"} and @{verbatim "-t"} of @{tool_ref document}). The standard
+ document is equivalent to ``@{verbatim
+ "document=theory,proof,ML"}'', which means that all theory begin/end
+ commands, proof body texts, and ML code will be presented
+ faithfully.
+
+ An alternative variant ``@{verbatim "outline=/proof/ML"}'' would
+ fold proof and ML parts, replacing the original text by a short
+ place-holder. The form ``@{text name}@{verbatim "=-"},'' means to
+ remove document @{text name} from the list of variants to be
+ processed. Any number of @{verbatim "-V"} options may be given;
+ later declarations have precedence over earlier ones.
+
+ Some document variant @{text name} may use an alternative {\LaTeX}
+ entry point called @{verbatim "document/root_"}@{text
+ "name"}@{verbatim ".tex"} if that file exists; otherwise the common
+ @{verbatim "document/root.tex"} is used.
+
+ \medskip The @{verbatim "-g"} option produces images of the theory
+ dependency graph (cf.\ \secref{sec:browse}) for inclusion in the
+ generated document, both as @{verbatim session_graph.eps} and
+ @{verbatim session_graph.pdf} at the same time. To include this in
+ the final {\LaTeX} document one could say @{verbatim
+ "\\includegraphics{session_graph}"} in @{verbatim
+ "document/root.tex"} (omitting the file-name extension enables
+ {\LaTeX} to select to correct version, either for the DVI or PDF
+ output path).
+
+ \medskip The @{verbatim "-D"} option causes the generated document
+ sources to be dumped at location @{verbatim PATH}; this path is
+ relative to the session's main directory. If the @{verbatim "-C"}
+ option is true, this will include a copy of an existing @{verbatim
+ document} directory as provided by the user. For example, @{tool
+ usedir}~@{verbatim "-D generated HOL Foo"} produces a complete set
+ of document sources at @{verbatim "Foo/generated"}. Subsequent
+ invocation of @{tool document}~@{verbatim "Foo/generated"} (see also
+ \secref{sec:tool-document}) will process the final result
+ independently of an Isabelle job. This decoupled mode of operation
+ facilitates debugging of serious {\LaTeX} errors, for example.
+
+ \medskip The @{verbatim "-p"} option determines the level of detail
+ for internal proof objects, see also the \emph{Isabelle Reference
+ Manual}~\cite{isabelle-ref}.
+
+ \medskip The @{verbatim "-q"} option specifies the level of parallel
+ proof checking: @{verbatim 0} no proofs, @{verbatim 1} toplevel
+ proofs (default), @{verbatim 2} toplevel and nested Isar proofs.
+ The option @{verbatim "-Q"} specifies a threshold for @{verbatim
+ "-q2"}: nested proofs are only parallelized when the current number
+ of forked proofs falls below the given value (default 50),
+ multiplied by the number of worker threads (see option @{verbatim
+ "-M"}).
+
+ \medskip The @{verbatim "-t"} option produces a more detailed
+ internal timing report of the session.
+
+ \medskip The @{verbatim "-v"} option causes additional information
+ to be printed while running the session, notably the location of
+ prepared documents.
+
+ \medskip The @{verbatim "-M"} option specifies the maximum number of
+ parallel worker threads used for processing independent tasks when
+ checking theory sources (multithreading only works on suitable ML
+ platforms). The special value of @{verbatim 0} or @{verbatim max}
+ refers to the number of actual CPU cores of the underlying machine,
+ which is a good starting point for optimal performance tuning. The
+ @{verbatim "-T"} option determines the level of detail in tracing
+ output concerning the internal locking and scheduling in
+ multithreaded operation. This may be helpful in isolating
+ performance bottle-necks, e.g.\ due to excessive wait states when
+ locking critical code sections.
+
+ \medskip Any @{tool usedir} session is named by some \emph{session
+ identifier}. These accumulate, documenting the way sessions depend
+ on others. For example, consider @{verbatim "Pure/FOL/ex"}, which
+ refers to the examples of FOL, which in turn is built upon Pure.
+
+ The current session's identifier is by default just the base name of
+ the @{verbatim LOGIC} argument (in build mode), or of the @{verbatim
+ NAME} argument (in example mode). This may be overridden explicitly
+ via the @{verbatim "-s"} option.
+*}
+
+
+section {* Output the version identifier of the Isabelle distribution *}
+
+text {*
+ The @{tool_def version} tool displays Isabelle version information:
+\begin{ttbox}
+Usage: isabelle version [OPTIONS]
+
+ Options are:
+ -i short identification (derived from Mercurial id)
+
+ Display Isabelle version information.
+\end{ttbox}
+
+ \medskip The default is to output the full version string of the
+ Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}.
+
+ The @{verbatim "-i"} option produces a short identification derived
+ from the Mercurial id of the @{setting ISABELLE_HOME} directory.
+*}
+
+
+section {* Convert XML to YXML *}
+
+text {*
+ The @{tool_def yxml} tool converts a standard XML document (stdin)
+ to the much simpler and more efficient YXML format of Isabelle
+ (stdout). The YXML format is defined as follows.
+
+ \begin{enumerate}
+
+ \item The encoding is always UTF-8.
+
+ \item Body text is represented verbatim (no escaping, no special
+ treatment of white space, no named entities, no CDATA chunks, no
+ comments).
+
+ \item Markup elements are represented via ASCII control characters
+ @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows:
+
+ \begin{tabular}{ll}
+ XML & YXML \\\hline
+ @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} &
+ @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\
+ @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\
+ \end{tabular}
+
+ There is no special case for empty body text, i.e.\ @{verbatim
+ "<foo/>"} is treated like @{verbatim "<foo></foo>"}. Also note that
+ @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in
+ well-formed XML documents.
+
+ \end{enumerate}
+
+ Parsing YXML is pretty straight-forward: split the text into chunks
+ separated by @{text "\<^bold>X"}, then split each chunk into
+ sub-chunks separated by @{text "\<^bold>Y"}. Markup chunks start
+ with an empty sub-chunk, and a second empty sub-chunk indicates
+ close of an element. Any other non-empty chunk consists of plain
+ text. For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
+ @{file "~~/src/Pure/PIDE/yxml.scala"}.
+
+ YXML documents may be detected quickly by checking that the first
+ two characters are @{text "\<^bold>X\<^bold>Y"}.
+*}
+
+end
\ No newline at end of file