# HG changeset patch # User wenzelm # Date 1221502958 -7200 # Node ID 10487d954a8fa89ceaf10fe617be6f9576e6258f # Parent eee194395fdc865eac821ca99493d56cf9fc03a9 converted misc.tex; diff -r eee194395fdc -r 10487d954a8f doc-src/System/IsaMakefile --- a/doc-src/System/IsaMakefile Mon Sep 15 19:43:10 2008 +0200 +++ b/doc-src/System/IsaMakefile Mon Sep 15 20:22:38 2008 +0200 @@ -22,7 +22,7 @@ Pure-System: $(LOG)/Pure-System.gz $(LOG)/Pure-System.gz: Thy/ROOT.ML ../antiquote_setup.ML \ - Thy/Basics.thy Thy/Presentation.thy + Thy/Basics.thy Thy/Misc.thy Thy/Presentation.thy @$(USEDIR) -s System Pure Thy diff -r eee194395fdc -r 10487d954a8f doc-src/System/Makefile --- a/doc-src/System/Makefile Mon Sep 15 19:43:10 2008 +0200 +++ b/doc-src/System/Makefile Mon Sep 15 20:22:38 2008 +0200 @@ -12,9 +12,9 @@ include ../Makefile.in NAME = system -FILES = system.tex Thy/document/Basics.tex misc.tex \ - Thy/document/Presentation.tex symbols.tex ../iman.sty \ - ../extra.sty ../ttbox.sty ../manual.bib +FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \ + Thy/document/Presentation.tex symbols.tex ../iman.sty \ + ../extra.sty ../ttbox.sty ../manual.bib \ OUTPUT = syms.tex diff -r eee194395fdc -r 10487d954a8f doc-src/System/Thy/Misc.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/Misc.thy Mon Sep 15 20:22:38 2008 +0200 @@ -0,0 +1,353 @@ +(* $Id$ *) + +theory Misc +imports Pure +begin + +chapter {* Miscellaneous tools \label{ch:tools} *} + +text {* + Subsequently we describe various Isabelle related utilities, given + in alphabetical order. +*} + + +section {* Displaying documents *} + +text {* + The @{tool_def display} utility displays documents in DVI or PDF + format: +\begin{ttbox} +Usage: 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} utility displays online documentation: +\begin{ttbox} +Usage: 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 {* Getting logic images *} + +text {* + The @{tool_def findlogics} utility traverses all directories + specified in @{setting ISABELLE_PATH}, looking for Isabelle logic + images. Its usage is: +\begin{ttbox} +Usage: 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} utility: +\begin{ttbox} +Usage: getenv [OPTIONS] [VARNAMES ...] + + Options are: + -a display complete environment + -b print values only (doesn't work for -a) + + 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. +*} + + +subsubsection {* Examples *} + +text {* + Get the ML system name and the location where the compiler binaries + are supposed to reside as follows: +\begin{ttbox} +isatool getenv ML_SYSTEM ML_HOME +{\out ML_SYSTEM=polyml} +{\out ML_HOME=/usr/share/polyml/x86-linux} +\end{ttbox} + + The next one peeks at the output directory for Isabelle logic + images: +\begin{ttbox} +isatool getenv -b ISABELLE_OUTPUT +{\out /home/me/isabelle/heaps/polyml_x86-linux} +\end{ttbox} + Here we have used the @{verbatim "-b"} option to suppress the + @{verbatim "ISABELLE_OUTPUT="} prefix. The value above is what + became of the following assignment in the default settings file: +\begin{ttbox} +ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps" +\end{ttbox} + + Note how the @{setting ML_IDENTIFIER} value got appended + automatically to each path component. This is a special feature of + @{setting ISABELLE_OUTPUT}. +*} + + +section {* Installing standalone Isabelle executables \label{sec:tool-install} *} + +text {* + By default, the Isabelle binaries (@{executable isabelle}, + @{executable isatool} etc.) are just run from their location within + the distribution directory, probably indirectly by the shell through + its @{verbatim PATH}. Other schemes of installation are supported + by the @{tool_def install} utility: +\begin{ttbox} +Usage: 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}, @{executable isatool}, @{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 @{verbatim + PATH}, such as @{verbatim "/usr/local/bin"}. It is important to + note that a plain manual copy of the original Isabelle executables + does not work, since it disrupts the integrity of the Isabelle + distribution. +*} + + +section {* Creating instances of the Isabelle logo *} + +text {* + The @{tool_def logo} utility creates any instance of the generic + Isabelle logo as an Encapsuled Postscript file (EPS): +\begin{ttbox} +Usage: logo [OPTIONS] NAME + + Create instance NAME of the Isabelle logo (as EPS). + + Options are: + -o OUTFILE set output file (default determined from NAME) + -q quiet mode +\end{ttbox} + You are encouraged to use this to create a derived logo for your + Isabelle project. For example, @{verbatim "isatool logo Bali"} + creates @{verbatim isabelle_bali.eps}. +*} + + +section {* Isabelle's version of make \label{sec:tool-make} *} + +text {* + The Isabelle @{tool_def make} utility is a very simple wrapper for + ordinary Unix @{executable make}: +\begin{ttbox} +Usage: 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_OUTPUT)"}. Furthermore, programs started from + the make file also inherit this environment. Typically, @{verbatim + IsaMakefile}s defer the real work to the @{tool_ref usedir} utility. + + \medskip The basic @{verbatim IsaMakefile} convention is that the + default target builds the actual logic, including its parents if + appropriate. The @{verbatim images} target is intended to build all + local logic images, while the @{verbatim test} target shall build + all related examples. The @{verbatim all} target shall do + @{verbatim images} and @{verbatim test}. +*} + + +subsubsection {* Examples *} + +text {* + Refer to the @{verbatim IsaMakefile}s of the Isabelle distribution's + object-logics as a model for your own developments. For example, + see @{verbatim "src/FOL/IsaMakefile"}. +*} + + +section {* Make all logics *} + +text {* + The @{tool_def makeall} utility applies Isabelle make to all logic + directories of the distribution: +\begin{ttbox} +Usage: makeall [ARGS ...] + + Apply isatool make to all logics (passing ARGS). +\end{ttbox} + + The arguments @{verbatim ARGS} are just passed verbatim to each + @{tool make} invocation. +*} + + +section {* Printing documents *} + +text {* + The @{tool_def print} utility prints documents: +\begin{ttbox} +Usage: 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 {* Run Isabelle with plain tty interaction \label{sec:tool-tty} *} + +text {* + The @{tool_def tty} utility runs the Isabelle process interactively + within a plain terminal session: +\begin{ttbox} +Usage: tty [OPTIONS] + + Options are: + -l NAME logic image name (default ISABELLE_LOGIC) + -m MODE add print mode for output + -p NAME line editor program name (default ISABELLE_LINE_EDITOR) + + Run Isabelle process with plain tty interaction, and optional line editor. +\end{ttbox} + + The @{verbatim "-l"} option specifies the logic image. The + @{verbatim "-m"} option specifies additional print modes. The The + @{verbatim "-p"} option specifies an alternative line editor (such + as the @{executable rlwrap} wrapper for GNU readline); the fall-back + is to use raw standard input. +*} + + +section {* Remove awkward symbol names from theory sources *} + +text {* + The @{tool_def unsymbolize} utility 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 ""} + by @{verbatim "==>"}. +\begin{ttbox} +Usage: 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 {* Output the version identifier of the Isabelle distribution *} + +text {* + The @{tool_def version} utility outputs the full version string of + the Isabelle distribution being used, e.g.\ ``@{verbatim + "Isabelle2008: June 2008"}. There are no options nor arguments. +*} + + +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 \"}@{verbatim ">"} & + @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\\<^bold>X"} \\ + @{verbatim ""} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\ + \end{tabular} + + There is no special case for empty body text, i.e.\ @{verbatim + ""} is treated like @{verbatim ""}. 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. + + 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 diff -r eee194395fdc -r 10487d954a8f doc-src/System/Thy/ROOT.ML --- a/doc-src/System/Thy/ROOT.ML Mon Sep 15 19:43:10 2008 +0200 +++ b/doc-src/System/Thy/ROOT.ML Mon Sep 15 20:22:38 2008 +0200 @@ -6,3 +6,4 @@ use_thy "Basics"; use_thy "Presentation"; +use_thy "Misc"; diff -r eee194395fdc -r 10487d954a8f doc-src/System/Thy/document/Misc.tex --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/System/Thy/document/Misc.tex Mon Sep 15 20:22:38 2008 +0200 @@ -0,0 +1,411 @@ +% +\begin{isabellebody}% +\def\isabellecontext{Misc}% +% +\isadelimtheory +\isanewline +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ Misc\isanewline +\isakeyword{imports}\ Pure\isanewline +\isakeyword{begin}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\isamarkupchapter{Miscellaneous tools \label{ch:tools}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Subsequently we describe various Isabelle related utilities, given + in alphabetical order.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Displaying documents% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{display}\hypertarget{tool.display}{\hyperlink{tool.display}{\mbox{\isa{\isatt{display}}}}} utility displays documents in DVI or PDF + format: +\begin{ttbox} +Usage: display [OPTIONS] FILE + + Options are: + -c cleanup -- remove FILE after use + + Display document FILE (in DVI format). +\end{ttbox} + + \medskip The \verb|-c| option causes the input file to be + removed after use. The program for viewing \verb|dvi| files is + determined by the \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isacharunderscore}VIEWER}}}} setting.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Viewing documentation \label{sec:tool-doc}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{doc}\hypertarget{tool.doc}{\hyperlink{tool.doc}{\mbox{\isa{\isatt{doc}}}}} utility displays online documentation: +\begin{ttbox} +Usage: 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 \hyperlink{setting.ISABELLE-DOCS}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}DOCS}}}} setting specifies the list of + directories (separated by colons) to be scanned for documentations. + The program for viewing \verb|dvi| files is determined by the + \hyperlink{setting.DVI-VIEWER}{\mbox{\isa{\isatt{DVI{\isacharunderscore}VIEWER}}}} setting.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Getting logic images% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{findlogics}\hypertarget{tool.findlogics}{\hyperlink{tool.findlogics}{\mbox{\isa{\isatt{findlogics}}}}} utility traverses all directories + specified in \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}}, looking for Isabelle logic + images. Its usage is: +\begin{ttbox} +Usage: 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 \hyperlink{setting.ISABELLE-PATH}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}PATH}}}} includes the current values of \hyperlink{setting.ML-SYSTEM}{\mbox{\isa{\isatt{ML{\isacharunderscore}SYSTEM}}}} + and \hyperlink{setting.ML-PLATFORM}{\mbox{\isa{\isatt{ML{\isacharunderscore}PLATFORM}}}}. Thus switching to another ML compiler + may change the set of logic images available.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Inspecting the settings environment \label{sec:tool-getenv}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Isabelle settings environment --- as provided by the + site-default and user-specific settings files --- can be inspected + with the \indexdef{}{tool}{getenv}\hypertarget{tool.getenv}{\hyperlink{tool.getenv}{\mbox{\isa{\isatt{getenv}}}}} utility: +\begin{ttbox} +Usage: getenv [OPTIONS] [VARNAMES ...] + + Options are: + -a display complete environment + -b print values only (doesn't work for -a) + + Get value of VARNAMES from the Isabelle settings. +\end{ttbox} + + With the \verb|-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 \isa{name}\verb|=|\isa{value}. The \verb|-b| option + causes only the values to be printed.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Examples% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Get the ML system name and the location where the compiler binaries + are supposed to reside as follows: +\begin{ttbox} +isatool getenv ML_SYSTEM ML_HOME +{\out ML_SYSTEM=polyml} +{\out ML_HOME=/usr/share/polyml/x86-linux} +\end{ttbox} + + The next one peeks at the output directory for Isabelle logic + images: +\begin{ttbox} +isatool getenv -b ISABELLE_OUTPUT +{\out /home/me/isabelle/heaps/polyml_x86-linux} +\end{ttbox} + Here we have used the \verb|-b| option to suppress the + \verb|ISABELLE_OUTPUT=| prefix. The value above is what + became of the following assignment in the default settings file: +\begin{ttbox} +ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps" +\end{ttbox} + + Note how the \hyperlink{setting.ML-IDENTIFIER}{\mbox{\isa{\isatt{ML{\isacharunderscore}IDENTIFIER}}}} value got appended + automatically to each path component. This is a special feature of + \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}OUTPUT}}}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Installing standalone Isabelle executables \label{sec:tool-install}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +By default, the Isabelle binaries (\hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}, + \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}} etc.) are just run from their location within + the distribution directory, probably indirectly by the shell through + its \verb|PATH|. Other schemes of installation are supported + by the \indexdef{}{tool}{install}\hypertarget{tool.install}{\hyperlink{tool.install}{\mbox{\isa{\isatt{install}}}}} utility: +\begin{ttbox} +Usage: 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 \verb|-d| option overrides the current Isabelle + distribution directory as determined by \hyperlink{setting.ISABELLE-HOME}{\mbox{\isa{\isatt{ISABELLE{\isacharunderscore}HOME}}}}. + + The \verb|-p| option installs executable wrapper scripts for + \hyperlink{executable.isabelle}{\mbox{\isa{\isatt{isabelle}}}}, \hyperlink{executable.isatool}{\mbox{\isa{\isatt{isatool}}}}, \hyperlink{executable.Isabelle}{\mbox{\isa{\isatt{Isabelle}}}}, containing proper absolute references to the Isabelle + distribution directory. A typical \verb|DIR| specification + would be some directory expected to be in the shell's \verb|PATH|, such as \verb|/usr/local/bin|. It is important to + note that a plain manual copy of the original Isabelle executables + does not work, since it disrupts the integrity of the Isabelle + distribution.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Creating instances of the Isabelle logo% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{logo}\hypertarget{tool.logo}{\hyperlink{tool.logo}{\mbox{\isa{\isatt{logo}}}}} utility creates any instance of the generic + Isabelle logo as an Encapsuled Postscript file (EPS): +\begin{ttbox} +Usage: logo [OPTIONS] NAME + + Create instance NAME of the Isabelle logo (as EPS). + + Options are: + -o OUTFILE set output file (default determined from NAME) + -q quiet mode +\end{ttbox} + You are encouraged to use this to create a derived logo for your + Isabelle project. For example, \verb|isatool logo Bali| + creates \verb|isabelle_bali.eps|.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Isabelle's version of make \label{sec:tool-make}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Isabelle \indexdef{}{tool}{make}\hypertarget{tool.make}{\hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}}} utility is a very simple wrapper for + ordinary Unix \hyperlink{executable.make}{\mbox{\isa{\isatt{make}}}}: +\begin{ttbox} +Usage: 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 \verb|IsaMakefile|, e.g.\ + \verb|$(ISABELLE_OUTPUT)|. Furthermore, programs started from + 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. + + \medskip The basic \verb|IsaMakefile| convention is that the + default target builds the actual logic, including its parents if + appropriate. The \verb|images| target is intended to build all + local logic images, while the \verb|test| target shall build + all related examples. The \verb|all| target shall do + \verb|images| and \verb|test|.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsubsection{Examples% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Refer to the \verb|IsaMakefile|s of the Isabelle distribution's + object-logics as a model for your own developments. For example, + see \verb|src/FOL/IsaMakefile|.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Make all logics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{makeall}\hypertarget{tool.makeall}{\hyperlink{tool.makeall}{\mbox{\isa{\isatt{makeall}}}}} utility applies Isabelle make to all logic + directories of the distribution: +\begin{ttbox} +Usage: makeall [ARGS ...] + + Apply isatool make to all logics (passing ARGS). +\end{ttbox} + + The arguments \verb|ARGS| are just passed verbatim to each + \hyperlink{tool.make}{\mbox{\isa{\isatt{make}}}} invocation.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Printing documents% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{print}\hypertarget{tool.print}{\hyperlink{tool.print}{\mbox{\isa{\isatt{print}}}}} utility prints documents: +\begin{ttbox} +Usage: print [OPTIONS] FILE + + Options are: + -c cleanup -- remove FILE after use + + Print document FILE. +\end{ttbox} + + The \verb|-c| option causes the input file to be removed + after use. The printer spool command is determined by the \hyperlink{setting.PRINT-COMMAND}{\mbox{\isa{\isatt{PRINT{\isacharunderscore}COMMAND}}}} setting.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Run Isabelle with plain tty interaction \label{sec:tool-tty}% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{tty}\hypertarget{tool.tty}{\hyperlink{tool.tty}{\mbox{\isa{\isatt{tty}}}}} utility runs the Isabelle process interactively + within a plain terminal session: +\begin{ttbox} +Usage: tty [OPTIONS] + + Options are: + -l NAME logic image name (default ISABELLE_LOGIC) + -m MODE add print mode for output + -p NAME line editor program name (default ISABELLE_LINE_EDITOR) + + Run Isabelle process with plain tty interaction, and optional line editor. +\end{ttbox} + + The \verb|-l| option specifies the logic image. The + \verb|-m| option specifies additional print modes. The The + \verb|-p| option specifies an alternative line editor (such + as the \hyperlink{executable.rlwrap}{\mbox{\isa{\isatt{rlwrap}}}} wrapper for GNU readline); the fall-back + is to use raw standard input.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Remove awkward symbol names from theory sources% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{unsymbolize}\hypertarget{tool.unsymbolize}{\hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}}} utility tunes Isabelle theory sources to + improve readability for plain ASCII output (e.g.\ in email + communication). Most notably, \hyperlink{tool.unsymbolize}{\mbox{\isa{\isatt{unsymbolize}}}} replaces awkward + arrow symbols such as \verb|\|\verb|| + by \verb|==>|. +\begin{ttbox} +Usage: 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}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Output the version identifier of the Isabelle distribution% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{version}\hypertarget{tool.version}{\hyperlink{tool.version}{\mbox{\isa{\isatt{version}}}}} utility outputs the full version string of + the Isabelle distribution being used, e.g.\ ``\verb|Isabelle2008: June 2008|. There are no options nor arguments.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsection{Convert XML to YXML% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The \indexdef{}{tool}{yxml}\hypertarget{tool.yxml}{\hyperlink{tool.yxml}{\mbox{\isa{\isatt{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 + \isa{{\isachardoublequote}\isactrlbold X\ {\isacharequal}\ {\isadigit{5}}{\isachardoublequote}} and \isa{{\isachardoublequote}\isactrlbold Y\ {\isacharequal}\ {\isadigit{6}}{\isachardoublequote}} as follows: + + \begin{tabular}{ll} + XML & YXML \\\hline + \verb|<|\isa{{\isachardoublequote}name\ attribute{\isachardoublequote}}\verb|=|\isa{{\isachardoublequote}value\ {\isasymdots}{\isachardoublequote}}\verb|>| & + \isa{{\isachardoublequote}\isactrlbold X\isactrlbold Yname\isactrlbold Yattribute{\isachardoublequote}}\verb|=|\isa{{\isachardoublequote}value{\isasymdots}\isactrlbold X{\isachardoublequote}} \\ + \verb|| & \isa{{\isachardoublequote}\isactrlbold X\isactrlbold Y\isactrlbold X{\isachardoublequote}} \\ + \end{tabular} + + There is no special case for empty body text, i.e.\ \verb|| is treated like \verb||. Also note that + \isa{{\isachardoublequote}\isactrlbold X{\isachardoublequote}} and \isa{{\isachardoublequote}\isactrlbold Y{\isachardoublequote}} may never occur in + well-formed XML documents. + + \end{enumerate} + + Parsing YXML is pretty straight-forward: split the text into chunks + separated by \isa{{\isachardoublequote}\isactrlbold X{\isachardoublequote}}, then split each chunk into + sub-chunks separated by \isa{{\isachardoublequote}\isactrlbold Y{\isachardoublequote}}. 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. + + YXML documents may be detected quickly by checking that the first + two characters are \isa{{\isachardoublequote}\isactrlbold X\isactrlbold Y{\isachardoublequote}}.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +\end{isabellebody}% +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "root" +%%% End: diff -r eee194395fdc -r 10487d954a8f doc-src/System/misc.tex --- a/doc-src/System/misc.tex Mon Sep 15 19:43:10 2008 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,329 +0,0 @@ - -% $Id$ - -\chapter{Miscellaneous tools} \label{ch:tools} - -Subsequently we describe various Isabelle related utilities, given in -alphabetical order. - - -\section{Converting legacy ML scripts --- \texttt{isatool convert}} - -The \tooldx{convert} utility assists in converting legacy ML proof scripts -into the new-style format of Isabelle/Isar: -\begin{ttbox} -Usage: convert [FILES|DIRS...] - - Recursively find .ML files, converting legacy tactic scripts to - Isabelle/Isar tactic emulation. - Note: conversion is only approximated, based on some heuristics. - - Renames old versions of FILES by appending "~0~". - Creates new versions of FILES by appending ".thy". -\end{ttbox} -The resulting theory text uses the tactic emulation facilities of -Isabelle/Isar (see also \cite{isabelle-ref}, especially the ``Conversion -guide'' in the appendix). Usually there is some manual tuning required to get -an automatically converted script work again --- the success rate is around -99\% for common ML scripts. - - -\section{Displaying documents --- \texttt{isatool display}} - -The \tooldx{display} utility displays documents in DVI format: -\begin{ttbox} -Usage: display [OPTIONS] FILE - - Options are: - -c cleanup -- remove FILE after use - - Display document FILE (in DVI format). -\end{ttbox} - -\medskip The \texttt{-c} option causes the input file to be removed after use. -The program for viewing \texttt{dvi} files is determined by the -\texttt{DVI_VIEWER} setting. - - -\section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc} - -The \tooldx{doc} utility displays online documentation: -\begin{ttbox} -Usage: 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 \texttt{ISABELLE_DOCS} setting specifies the list of directories -(separated by colons) to be scanned for documentations. The program for -viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting. - - -\section{Getting logic images --- \texttt{isatool findlogics}} - -The \tooldx{findlogics} utility traverses all directories specified in -\texttt{ISABELLE_PATH}, looking for Isabelle logic images. Its usage is: -\begin{ttbox} -Usage: 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 \texttt{ISABELLE_PATH} includes -the current values of \texttt{ML_SYSTEM} and \texttt{ML_PLATFORM}. Thus -switching to another {\ML} compiler may change the set of logic images -available. - - -\section{Inspecting the settings environment --- \texttt{isatool getenv}} -\label{sec:tool-getenv} - -The Isabelle settings environment --- as provided by the site-default and -user-specific settings files --- can be inspected with the \tooldx{getenv} -utility: -\begin{ttbox} -Usage: getenv [OPTIONS] [VARNAMES ...] - - Options are: - -a display complete environment - -b print values only (doesn't work for -a) - - Get value of VARNAMES from the Isabelle settings. -\end{ttbox} - -With the \texttt{-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 \mbox{$name$\texttt{=}$value$}. The \texttt{-b} option -causes only the values to be printed. - - -\subsection*{Examples} - -Get the {\ML} system name and the location where the compiler binaries are -supposed to reside as follows: -\begin{ttbox} -isatool getenv ML_SYSTEM ML_HOME -{\out ML_SYSTEM=polyml} -{\out ML_HOME=/usr/share/polyml/x86-linux} -\end{ttbox} - -The next one peeks at the output directory for \texttt{isabelle} logic images: -\begin{ttbox} -isatool getenv -b ISABELLE_OUTPUT -{\out /home/me/isabelle/heaps/polyml_x86-linux} -\end{ttbox} -Here we have used the \texttt{-b} option to suppress the -\texttt{ISABELLE_OUTPUT=} prefix. The value above is what became of the -following assignment in the default settings file: -\begin{ttbox} -ISABELLE_OUTPUT="\$ISABELLE_HOME_USER/heaps" -\end{ttbox} -Note how the \texttt{ML_IDENTIFIER} value got appended automatically to each -path component. This is a special feature of \texttt{ISABELLE_OUTPUT}. - - -\section{Installing standalone Isabelle executables --- \texttt{isatool install}} -\label{sec:tool-install} - -By default, the Isabelle binaries (\texttt{isabelle}, \texttt{isatool} etc.) -are just run from their location within the distribution directory, probably -indirectly by the shell through its \texttt{PATH}. Other schemes of -installation are supported by the \tooldx{install} utility: -\begin{ttbox} -Usage: 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 \texttt{-d} option overrides the current Isabelle distribution directory -as determined by \texttt{ISABELLE_HOME}. - -The \texttt{-p} option installs executable wrapper scripts for -\texttt{isabelle}, \texttt{isatool}, \texttt{Isabelle}, containing proper -absolute references to the Isabelle distribution directory. A typical -\texttt{DIR} specification would be some directory expected to be in the -shell's \texttt{PATH}, such as \texttt{/usr/local/bin}. It is important to -note that a plain manual copy of the original Isabelle executables just would -not work! - - -\section{Creating instances of the Isabelle logo --- \texttt{isatool - logo}} - -The \tooldx{logo} utility creates any instance of the generic Isabelle logo as -an Encapsuled Postscript file (EPS): -\begin{ttbox} -Usage: logo [OPTIONS] NAME - - Create instance NAME of the Isabelle logo (as EPS). - - Options are: - -o OUTFILE set output file (default determined from NAME) - -q quiet mode -\end{ttbox} -You are encouraged to use this to create a derived logo for your Isabelle -project. For example, \texttt{isatool logo Bali} creates -\texttt{isabelle_bali.eps}. - - -\section{Isabelle's version of make --- \texttt{isatool make}} -\label{sec:tool-make} - -The Isabelle \tooldx{make} utility is a very simple wrapper for -ordinary Unix \texttt{make}: -\begin{ttbox} -Usage: 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 \ttindex{IsaMakefile}, e.g.\ -\texttt{\$(ISABELLE_OUTPUT)}. Furthermore, programs started from the -make file also inherit this environment. Typically, -\texttt{IsaMakefile}s defer the real work to the \texttt{usedir} -utility, see \S\ref{sec:tool-usedir}. - -\medskip The basic \texttt{IsaMakefile} convention is that the default -target builds the actual logic, including its parents if appropriate. -The \texttt{images} target is intended to build all local logic -images, while the \texttt{test} target shall build all related -examples. The \texttt{all} target shall do \texttt{images} and -\texttt{test}. - - -\subsection*{Examples} - -Refer to the \texttt{IsaMakefile}s of the Isabelle distribution's -object-logics as a model for your own developments. For example, see -\texttt{src/FOL/IsaMakefile}. - - -\section{Make all logics --- \texttt{isatool makeall}} - -The \tooldx{makeall} utility applies Isabelle make to all logic -directories of the distribution: -\begin{ttbox} -Usage: makeall [ARGS ...] - - Apply isatool make to all logics (passing ARGS). -\end{ttbox} -The arguments \texttt{ARGS} are just passed verbatim to each -\texttt{make} invocation. - - -\section{Printing documents --- \texttt{isatool print}} - -The \tooldx{print} utility prints documents: -\begin{ttbox} -Usage: print [OPTIONS] FILE - - Options are: - -c cleanup -- remove FILE after use - - Print document FILE. -\end{ttbox} - -The \texttt{-c} option causes the input file to be removed after use. The -printer spool command is determined by the \texttt{PRINT_COMMAND} setting. - - -\section{Run Isabelle with plain tty interaction --- \texttt{isatool tty}} \label{sec:tool-tty} - -The \tooldx{tty} utility runs the Isabelle process interactively -within a plain terminal session: -\begin{ttbox} -Usage: tty [OPTIONS] - - Options are: - -l NAME logic image name (default ISABELLE_LOGIC) - -m MODE add print mode for output - -p NAME line editor program name (default ISABELLE_LINE_EDITOR) - - Run Isabelle process with plain tty interaction, and optional line editor. -\end{ttbox} - -The \texttt{-l} option specifies the logic image. The \texttt{-m} -option specifies additional print modes. The The \texttt{-p} option -specifies an alternative line editor (such as the \texttt{rlwrap} -wrapper for GNU readline); the fall-back is to use raw standard input. - - -\section{Remove awkward symbol names from theory sources --- \texttt{isatool unsymbolize}} - -The \tooldx{unsymbolize} utility tunes Isabelle theory sources to improve -readability for plain ASCII output (e.g.\ in email communication). Most -notably, \texttt{unsymbolize} replaces awkward arrow symbols such as -\verb|\| by \verb|==>|. -\begin{ttbox} -Usage: 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{Output the version identifier of the Isabelle distribution --- \texttt{isatool version}} - -The \tooldx{version} utility outputs the full version string of the -Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007: - November 2007}''. There are no options nor arguments. - - -\section{Convert XML to YXML --- \texttt{isatool yxml}} - -The \tooldx{yxml} utility 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 $X - = 5$ and $Y = 6$ as follows: - - \begin{tabular}{ll} - XML & YXML \\\hline - \verb,<,\emph{name}~\emph{attribute}\verb,=,\emph{value}~\dots\verb,>, & - \emph{X\,Y\,name\,Y\,attribute}\verb,=,\emph{value}\dots\emph{X} \\ - \verb,, & \emph{X\,Y\,X} \\ - \end{tabular} - - There is no special case for empty body text, i.e.\ \verb,, is - treated like \verb,,. Also note that \emph{X} and - \emph{Y} may never occur in well-formed XML documents. - -\end{enumerate} - -Parsing YXML is pretty straight-forward: split the text into chunks separated -by \emph{X}, then split each chunk into sub-chunks separated by \emph{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. - -YXML documents may be detected quickly by checking that the first two -characters are \emph{X\,Y}. - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "system" -%%% End: diff -r eee194395fdc -r 10487d954a8f doc-src/System/system.tex --- a/doc-src/System/system.tex Mon Sep 15 19:43:10 2008 +0200 +++ b/doc-src/System/system.tex Mon Sep 15 20:22:38 2008 +0200 @@ -38,7 +38,7 @@ \input{Thy/document/Basics} \input{Thy/document/Presentation} -\input{misc} +\input{Thy/document/Misc} \appendix \let\int\intorig