IT/Description/misc.tex

\chapter{Miscellaneous Features}\label{avramisc}

This section describes some of the features
that exist for managing the interface
%
\index{HOL system@\HOL{} system!adjustment of user interface of}
%
to the \HOL{} system.

\begin{itemize}
\item The help system.
\item The trace system for controlling feedback and printing.
\item \holmake{}: a tool for dependency maintenance in large developments.
\item Functions for counting the number of primitive inferences done in
an evaluation, and timing it.
\item A tool for embedding pretty-printed HOL theorems, terms and
  types in \LaTeX{} documents.
\end{itemize}

\section{Help}

 There are several kinds of help available in \HOL{}, all accessible
 through the same incantation:
 \begin{verbatim}
     help <string>;
 \end{verbatim}

 The kinds of help available are:

 \begin{description}

 \item [Moscow~ML help.] \index{Moscow ML} (When using Moscow~ML~\HOL{})
   This is uniformly excellent.
   Information for library routines is available, whether the library is loaded or not \emph{via} \texttt{help~"Lib"}.

\item [\HOL{} overview.] This is a short summary of important information
  about \HOL{}.

\item [\HOL{} help.] This on-line help is intended to document all
  HOL-specific functions available to the user. It is very detailed
  and often accurate; however, it can be out-of-date, refer to earlier
  versions of the system, or even be missing!

\item [\HOL{} structure information.]  For most structures in the
  \HOL{} source, one can get a listing of the entrypoints found in the
  accompanying signature. This is helpful for locating functions and
  is automatically derived from the system sources, so it is alway
  up-to-date.

\item [Theory facts.] These are automatically derived from theory
  files, so they are always up-to-date. The signature of each theory
  is available (since theories are represented by structures in
  \HOL{}). Also, each axiom, definition, and theorem in the theory can
  be accessed by name in the help system; the theorem itself is given.
\end{description}

Therefore the following example queries can be made:

\begin{table}[h]
  \begin{center}
    \begin{tabular}{|l|l|} \hline
      \verb+help "installPP"+ & Moscow ML help \\
      \verb+help "hol"+ &  \HOL{} overview \\
      \verb+help "aconv"+ &  on-line \HOL{} help \\
      \verb+help "Tactic"+ & \HOL{} source structure information \\
      \verb+help "boolTheory"+ &  theory structure signature \\
      \verb+help "list_Axiom"+ & theory structure signature and theorem
      statement \\ \hline
    \end{tabular}
  \end{center}
\end{table}

\section{The Trace System}
\index{traces, controlling HOL feedback@traces, controlling \HOL{} feedback}
\label{sec:traces}

The trace system gives the user one central interface with which to control most of \HOL's many different flags, though they be scattered all over the system, and defined in different modules.
These flags are typically those that determine the level to which \HOL{} tools provide information to the user while operating.
For example, a trace level of zero will usually make a tool remain completely
silent while it operates.
The tool may still raise an exception when it fails, but it won't also
output any messages saying so.

There are three core functions, all in the \ml{Feedback} structure:
\begin{hol}
\begin{verbatim}
   traces : unit ->
            {default: int, max: int, name: string, trace_level: int} list

   set_trace : string -> int -> unit
   trace     : (string * int) -> ('a -> 'b) -> ('a -> 'b)
\end{verbatim}
\end{hol}

The \ml{traces} function returns a list of all the traces in the system.
The \ml{set\_trace} function allows the user to set a trace directly.
The effect of this might be seen in a subsequent call to \ml{traces()}.
Finally, the \ml{trace} function allows for a trace to be temporarily set while a function executes, restoring the trace to its old value when the function returns (whether normally, or with an exception).


\section{Maintaining \HOL{} Formalizations with \holmake}
\label{Holmake}
\index{Holmake@\holmake|(}

The purpose of \holmake{} is to maintain dependencies in a \HOL{}
source directory. A single invocation of \holmake{} will compute
dependencies between files, (re)compile plain ML code, (re)compile and
execute theory scripts, and (re)compile the resulting theory modules.
\holmake{} does not require the user to provide any explicit
dependency information themselves. \holmake{} can be very convenient
to use, but there are some conventions and restrictions on it that
must be followed, described below.


\holmake{} can be accessed through
\begin{verbatim}
   <hol-dir>/bin/Holmake.
\end{verbatim}

The development model that \holmake{} is designed to support is that
there are two modes of work: theory construction and system revision.
In `theory construction' mode, the user builds up a theory by
interacting with HOL, perhaps over many sessions. In `system rebuild'
mode, a component that others depend on has been altered, so all modules
dependent on it have to be brought up to date. System rebuild mode is
simpler so we deal with it first.

\subsection{System rebuild}

A system rebuild happens when an existing theory has been improved in
some way (augmented with a new theorem, a change to a definition,
etc.), or perhaps some support ML code has been modified or added to
the formalization under development. The user needs to find and
recompile just those modules affected by the change. This is what an
invocation of \holmake{} does, by identifying the out-of-date modules
and re-compiling and re-executing them.


\subsection{Theory construction}

To start a theory construction, some context (semantic, and also proof
support) is established, typically by loading parent theories and
useful libraries. In the course of building the theory, the user keeps
track of the ML---which, for example, establishes context, makes
definitions, builds and invokes tactics, and saves theorems---in a
text file. This file is used to achieve inter-session persistence of
the theory being constructed.  For example, the text file resulting
from session $n$ is ``\verb+use+''-d to start session $n+1$; after
that, theory construction resumes.

Once the user finishes the perhaps long and arduous task of constructing
a theory, the user should
\begin{enumerate}
\item make the script separately compilable;
\item invoke \holmake{}. This will (a) compile and execute the
  script file; and (b) compile the resulting theory file. After this,
  the theory file is available for use.
\end{enumerate}

\subsection{Making the script separately compilable}

First, the invocation
\begin{verbatim}
    val _ = export_theory();
\end{verbatim}
should be added at the end of the file. When the script is finally
executed, this call writes the theory to disk.

\index{load (ML function)@\ml{load} (\ML{} function)}
Second, we address a crucial environmental issue: if a theory script
has been constructed using\verb+ <holdir>/bin/hol+, then it has been
developed in an environment where some commonly used structures, \eg,
\verb+Tactic+, have already been loaded and opened for the user's
convenience. When we wish to apply \holmake{} to a script developed
in this way, we have to take some extra steps to ensure that the
compilation environment also provides these structures.  In the common
case, this is simple; one must only add, at the head of the theory
script, the following ``boilerplate'':
\begin{verbatim}
   open HolKernel Parse boolLib;
\end{verbatim}
This will duplicate the starting environment that one obtains with
\verb+hol.bare+ and \linebreak \verb+hol.bare.noquote+.  If the script was
developed interactively with \texttt{hol} or \texttt{hol.noquote},
then one must also add
\begin{verbatim}
   open bossLib
\end{verbatim}
Now the script should be separately compilable. Invoke \holmake{}
to check; the \ML{} compiler will flag any unaccounted-for identifiers it finds.
The user has to resolve these, either by using the `dot' notation to
locate the identifier for the compiler, or by \verb+open+-ing the
relevant module. This ``compile/resolve-identifier'' loop should
continue until \holmake{} succeeds in compiling the module.

The following notes may be of some further help.

\begin{enumerate}
\item The filenames of theory scripts must follow the following
  convention: a HOL theory script for theory ``x'' should be named
  \texttt{xScript.sml}.  When \verb+export_theory+ is called during an
  invocation of \holmake, the files \texttt{xTheory.sig} and
  \texttt{xTheory.sml} will be generated and then compiled.

\item In \ML{}, modules are not allowed to include unbound top-level expressions.
  Hence, something like the following is not allowed:
\begin{verbatim}
   new_theory "ted";
\end{verbatim}
To make \ML{} happy, one must instead write something like
\begin{verbatim}
   val _ = new_theory "ted";
\end{verbatim}
\noindent
This is because (due to restrictions imposed by Moscow~ML\index{Moscow ML}) the script file is required to be an ML structure, and the contents of a structure must be \emph{declarations}, not expressions.
Indeed, one is allowed to (and often will) omit the bracketing \texttt{structure~foo~=~struct} - \texttt{end} lines, but the contents of the file are still interpreted as if belonging to a structure.

\index{load (ML function)@\ml{load} (\ML{} function)}
\item In the interactive system, one has to explicitly \ml{load} modules; on the other hand, the batch compiler will load modules automatically.
For example, in order to execute \ml{open Foo} (or refer to values in structure \ml{Foo}) in the interactive system, one must first have executed \ml{load "Foo"}.
(This is on the assumption that structure \ml{Foo} is defined in a file \texttt{Foo.sml}.)
Contrarily, the batch compiler will reject files having occurrences of \ml{load}, since \ml{load} is only defined for the interactive system.

\item Take care not to have the string ``Theory'' embedded in the name of any of your files.
\HOL{} generates files containing this string, and when it cleans up after itself, it removes such files using a regular expression.
This will also remove other files with names containing ``Theory''.
For example, if, in your development directory, you had a file of \ML{} code named \texttt{MyTheory.sml} and you were also managing a \HOL{} development there with \holmake, then \texttt{MyTheory.sml} would get deleted if \texttt{Holmake~clean} were invoked.

\end{enumerate}

\subsection{Summary}

A complete theory construction might be performed by the following steps:
\begin{itemize}
\item Construct theory script, perhaps over many sessions;
\item Transform script into separately compilable form;
\item Invoke \holmake{} to generate the theory and compile it.
\end{itemize}
After that, the theory is usable as an ML module.
This flow is demonstrated in the Euclid example of \TUTORIAL.

Alternatively, and probably with the help of one of the editor modes,\footnote{There are editor modes for \texttt{emacs} and \texttt{vim}.} one can develop a theory with a script file that is always separately compilable.

\subsection{What \holmake{} doesn't do}

\holmake{} only works properly on the current directory.
\holmake{} will rebuild files in the current directory if something it depends on from another directory is fresher than it is, but it will not do any analysis on files in other directories.

\index{Holmake@\holmake!recursive invocation}%
However, one can indicate that there is a dependency on other directories by using the \texttt{-I} flag, or the \texttt{INCLUDES} variable in a \texttt{Holmakefile}.
Such a specification will cause \holmake{} to look in the specified directories for other theory files that the current directory may depend on.
Moreover, by default \holmake{} will recursively call itself on all those ``include'' directories before doing anything in the current directory.
In this way, one can get a staged application of \holmake{} across multiple directories.\footnote{See \emph{Recursive Make Considered
    Harmful} by Peter Miller for why this is not ideal.}

\subsection{\holmake{}'s command-line arguments}

Like {\tt make}, \holmake{} takes command-line arguments corresponding
to the targets that the user desires to build.  If there are none,
then \holmake{} will attempt to build all ML modules and HOL theories
it can detect in the current directory.  In addition, there are three
special targets that can be used:
\begin{description}
\item[{\tt clean}] Removes all compiled files (unless over-ridden by a
  make-file target of the same name, see
  section~\ref{sec:using-Holmakefiles} below).
\item [{\tt cleanDeps}] Removes all of the pre-computed dependency
  files.  This can be an important thing to do if, for example, you
  have introduced a new {\tt .sig} file on top of an existing {\tt
    .sml} file.
\item [{\tt cleanAll}] Removes all compiled files as well as all of
  the hidden dependency information.
\end{description}

\noindent Finally, users can directly affect the workings of \holmake{}
with the following command-line options:
\begin{description}
\item[\tt -I <directory>] Look in specified directory for additional
  Moscow~ML object files, including other HOL theories.  This option
  can be repeated, with multiple {\tt -I}'s to allow for multiple
  directories to be referenced.  As above, directories specified in
  this way will also be rebuilt before the current targets are built.
\item[\tt -d <file>] Ignore the given file and don't try to build it.
  The file may be rebuilt anyway if other files you have specified
  depend on it.  This is useful to stop Holmake from attempting to
  compile files that are interactive scripts (include use of {\tt
  load} or {\tt use}, for example).
\item[\texttt{-f <theory>}] Toggles whether or not a theory should be
  built in ``fast'' mode.  Fast building causes tactic proofs
  (invocations of \texttt{prove} and \texttt{store\_thm}) to
  automatically succeed.  This lack of soundness is marked by the
  \texttt{fast\_proof} oracle tag.  This tag will appear on all
  theorems proved in this way and all subsequent theorems that depend
  on such theorems.  \holmake's default is not to build in fast mode.
\item[\texttt{-r}]%
\index{Holmake@\holmake!recursive invocation}%
Forces \holmake{} to behave recursively, overriding the \texttt{--no\_prereqs} option, and also causing \holmake{} to clean recursively in the ``includes'' directories (which is not done otherwise).
\item[\texttt{--fast}] Makes \holmake's default be to build in fast
  mode (see above).
\item[{\tt --help} or {\tt -h}] Prints out a useful option summary and
  exits.
\item[\tt --holdir <directory>] Associate this build with the given
  HOL directory, rather than the one this version of \holmake{} was
  configured to use by default.
\item[\tt --holmakefile <file>] Use the given file as a make-file.
  See section~\ref{sec:using-Holmakefiles} below for more on this.
\item[\texttt{--interactive} or \texttt{-i}] Causes the HOL code that
  runs when a theory building file is executed to have the flag
  \texttt{Globals.interactive} set to true.  This will alter the diagnostic
  output of a number of functions within the system.
\item[\texttt{-k} or \texttt{--keep-going}] Causes \holmake{} to try
  to build all specified targets, rather than stopping as soon as one
  fails to build.
\item[\texttt{--logging}] Causes \holmake{} to record the times taken
  to build any theory files it encounters.  The times are logged in a
  file in the current directory.  The name of this file includes the
  time when \holmake{} completed, and when on a Unix system, the name
  of the machine where the job was run.  If \holmake{} exits
  unsuccessfully, the filename is preceded by the string
  ``\texttt{bad-}''. Each line in the log-file is of the form
  \textit{theory-name time-taken}, with the time recorded in seconds.
\item[\texttt{--no\_holmakefile}]  Do not use a make-file, even if a file
  called \texttt{Holmakefile} is present in the current directory.
\item[\texttt{--no\_overlay}] Do not use an overlay file.  All HOL
  builds require the presence of a special overlay file from the
  kernel when compiling scripts and libraries.  This is not
  appropriate for compiling code that has no connection to HOL, so
  this option makes the compilation not use the overlay file.  This
  option is also used in building the kernel before the overlay itself
  has been compiled.
\item[\texttt{--no\_prereqs}]%
\index{Holmake@\holmake!recursive invocation}%
Do not recursively attempt to build ``include'' directories before working in the current directory.
\item[\texttt{--no\_sigobj}] Do not link against HOL system's
  directory of HOL system files.  Use of this option goes some way
  towards turning
  \holmake{} into a general Moscow~ML \textsf{make} system.  However,
  it will still attempt to do ``HOL things'' with files whose names
  end in \texttt{Script} and \texttt{Theory}.  This option implies
  \texttt{--no\_overlay}.
\item[\texttt{--overlay <file>}] Use the given file as the overlay
  rather than the default.
\item[\texttt{--qof}] Standing for ``quit on failure''.  If a tactic
  fails to prove a theorem, quit the build.  The default is to use
  \texttt{mk\_thm} to assert that the failed goal is true so that the
  build can continue and other theorems proved.
\item[\texttt{--quiet}] Minimise the amount of output produced by
  \holmake{}.  Fatal error messages will still be written to the
  standard error stream.  Note that other programs called by \holmake{} will not
  be affected.
\item[{\tt --rebuild\_deps}] Forces \holmake{} to always
  rebuild the dependency information for files it examines, whether or
  not it thinks it needs to.  This option is implemented by having
  \holmake{} wipe all of its dependency cache (as per the
  \texttt{cleanDeps} option above) before proceeding with the build.
\end{description}

\noindent \holmake{} should never exit with the Moscow~ML message ``Uncaught
exception''.  Such behaviour is a bug, please report it!


\subsection{Using a make-file with \holmake}
\label{sec:using-Holmakefiles}

\holmake{} will use a make-file to augment its behaviour if one is
present in the current directory.  By default it will look for a file
called \texttt{Holmakefile}, but it can be made to look at any file at
all with the \texttt{--holmakefile} command-line option.  The
combination of \holmake{} and a make-file is supposed to behave as
much as possible like a standard implementation of \textsf{make}.

A make-file consists of two types of entries, variable definitions and
rules.  Outside of these entries, white-space is insignificant, but
newline and \texttt{TAB} characters are very significant within them.
Comments can be started with hash (\texttt{\#}) characters and last
until the end of the line.  Quoting is generally done with use of the
back-slash (\verb+\+) character.  In particular, a backslash-newline
pair always allows a line to be continued as if the newline wasn't
present at all.

A variable definition is of the form
\[
\textsl{Ident} \texttt{ = } \textsl{text}  \texttt{ <NEWLINE> }
\]
and a rule is of the form
\[
\textsl{text } \texttt{:} \textsl{ text} \texttt{ <NEWLINE>}
(\texttt{<TAB>}\textsl{text}\texttt{ <NEWLINE>})^*
\]
Henceforth, the text following a \texttt{TAB} character in a rule will
be referred to as the \emph{command text}.  Text elsewhere will be
referred to as \emph{normal text}.  Normal text has comments stripped
from it, so hash characters there must be escaped with a back-slash
character.  An \textsl{Ident} is any non-empty sequence of
alpha-numeric characters, including the underscore (\texttt{\_}).

In some contexts, normal text is interpreted as a list of words.
These lists use white-space as element separators.  If a word needs to
include white-space itself, those white-space characters should be
escaped with back-slashes.

\newcommand{\varref}[1]{\texttt{\$(#1)}}
\paragraph{Variable definitions} The text on the RHS of a variable
definition can be substituted into any other context by using a
\emph{variable reference}, of the form \varref{VARNAME}.  References
are evaluated \emph{late}, not at time of definition, so it is quite
permissible to have forward references.  On the other hand, this makes
it impossible to write things like \[ \texttt{VAR = \varref{VAR}
something\_new}
\] because the evaluation of \varref{VAR} would lead to an infinite
loop. GNU \textsf{make}'s facility for immediate
definition of variables with \texttt{:=} is not supported.

Note also that white-space around the equals-sign in a variable
definition is stripped.  This means that
\[
\texttt{VAR =<whitespace><NEWLINE>}
\] gives \texttt{VAR} the empty string as its value.\footnote{It is
  possible to give a variable a value of pure whitespace by writing \[
\begin{array}{l}
\texttt{NOTHING =}\\
\texttt{ONE\_SPACE = \varref{NOTHING}\textvisiblespace\hspace{1mm}\varref{NOTHING}}\\
\end{array}\]}

Finally, note that the text inside a variable reference is itself
evaluated.  This means that one can write something like
\varref{FOO\_\varref{OS}} and have this first expand the \texttt{OS}
variable, presumably giving rise to some useful string (such as
\texttt{unix}), and then have the resulting variable
(\texttt{FOO\_unix}, say) expanded.  This effectively allows the
construction of functions by cases (define variables
\texttt{FOO\_unix}, \texttt{FOO\_macos} etc; then use the nested
variable reference above).  If the internal variable expands to
something containing spaces, this will not turn a normal variable
reference into a function call (see below).  On the other hand,
if the initial reference contains a space, the function name component
\emph{will} be expanded, allowing implementation of a function by
cases determining which text-manipulation function should be called.

\paragraph{Rules}
Make-file rules are interpreted in the same way as by traditional
\textsf{make}.  The files specified after the colon (if any) are those
files that each target (the files before the colon) is said to
``depend'' on.  If any of these are newer than a target, then
\holmake{} rebuilds that target according to the commands.  If there
are no dependencies, then the commands are executed iff the
target doesn't exist.  If there are no commands, and the target is not
of a type that \holmake{} already knows how to build, then it will
just make sure that the dependencies are up to date (this may or
may not create the target).  If there are no commands attached to a
rule, and the target is one that \holmake{} does know how to build,
then the rule's extra dependencies are added to those that \holmake{}
has managed to infer for itself, and \holmake{} will build the target
using its built-in rule.  If commands are provided for a type of file
that \holmake{} knows how to build itself, then the make-file's
commands and dependencies take precedence, and only they will be
executed.

If a command-line is preceded by a hyphen (\verb!-!) character, then
the rest of the line is executed, but its error-code is ignored.
(Normally, a command-line raising an error will cause \holmake{} to
conclude that the target can not be built.)  If a command-line is
preceded by an at-sign (\verb!@!), then that command-line will not be
echoed to the screen when it is run.  These two options can be
combined in either order at the start of a command-line.

Command text is interpreted only minimally by \holmake.  On Unix,
back-slashes are not interpreted at all.  On Windows, back-slashes
followed by newlines are turned into spaces. Otherwise, command text
is passed as is to the underlying command interpreter
(\texttt{/bin/sh} say, on Unix, or \texttt{COMMAND.COM} on Windows).
In particular, this means that hash-characters do \emph{not} start
comments on command-lines, and such ``comments'' will be passed to the
shell, which may or may not treat them as comments when it sees them.

\paragraph{Functions}
\index{Holmake@\holmake!functions for text-manipulation}
\holmake{} supports some simple functions for manipulating text.  All
functions are written with the general form
\texttt{\$(\textsl{function-name}\textvisiblespace{}\hspace{1mm}\textsl{arg}${}_1$,\textsl{arg}${}_2$\dots,\textsl{arg}${}_n$)}.
Arguments can not include commas (use variable references to variables
whose value are commas instead), but can otherwise be arbitrary text.
\begin{description}
\item[\texttt{\$(dprot arg)}] quotes (or ``protects'') the space
  characters that occur in a string so that the string will be treated
  as a unit if it occurs in a rule's dependency list.  For example,
  the file
\begin{verbatim}
   dep = foo bar
   target: $(dep)
      do_something
\end{verbatim}
  will see \texttt{target} as having two dependencies, not one,
  because spaces are used to delimit dependencies.  If a dependency's
  name includes spaces, then this function can be used to quote them
  for \holmake's benefit.  Note that the \texttt{dprot} function
  does \emph{not} do the same thing as \texttt{protect} on either Unix
  or Windows systems.
\item[\texttt{\$(findstring arg1,arg2)}] checks if \texttt{arg1} occurs
  in (is a sub-string of) \texttt{arg2}.  If it does so occur, the
  result is \texttt{arg1}, otherwise the result is the empty string.
\item[\texttt{\$(if arg1,arg2,arg3)}] examines \texttt{arg1}.  If it
  is the empty string, then the value of the whole is equal to the
  value of \texttt{arg3}.  Otherwise, the value is that of \texttt{arg2}.
\item[\texttt{\$(patsubst arg1,arg2,text)}] splits \texttt{text} into component
  words, and then transforms each word by attempting to see if it
  matches the pattern in \texttt{arg1}.  If so, it replaces that word
  with \texttt{arg2} (suitably instantiated).  If not, the word is
  left alone.  The modified words are then reassembled into a
  white-space separated list and returned as the value.

  A pattern is any piece of text including no more than one occurrence
  of the percent~(\texttt{\%}) character.  The percent character
  matches any non-empty string.  All other characters must be matched
  literally.  The instantiation for \texttt{\%} is remembered when the
  replacement is constructed.  Thus, \[
    \texttt{\$(patsubst \%.sml,\%.uo,\$(SMLFILES))}
   \] turns a list of files with suffixes \texttt{.sml} into the same
  list with the suffixes replaced with \texttt{.uo}.
\item[\texttt{\$(protect arg)}] wraps \texttt{arg} in appropriate
  quote characters to ensure that it will pass through the operating
  system's command shell unscathed.  This is important in the presence
  of file-names that include spaces or other shell-significant
  characters like less-than and greater-than.  Those make-file
  variables that point directly at executables (\texttt{MOSMLC},
  \texttt{MOSMLLEX} etc) are automatically protected in this way.
  Others, which might be used in concatenation with other elements,
  are not so protected.  Thus, if \texttt{DIR} might include spaces,
  one should write
\begin{verbatim}
   $(protect $(DIR)/subdirectory/program)
\end{verbatim}
  so that the above will be read as one unit by the underlying shell.
\item[\texttt{\$(subst arg1,arg2,text)}] replaces every occurrence
  of \texttt{arg1} in \texttt{text} with \texttt{arg2}.
\end{description}

\paragraph{Special and pre-defined variables}

\index{Holmake@\holmake!variables in makefiles}
If defined, the \texttt{INCLUDES} variable is used to add directories to the list of directories consulted when files are compiled and linked.
The effect is as if the directories specified had all been included on the command-line with \texttt{-I} options.
The \texttt{PRE\_INCLUDES} variable works similarly, but the directories specified here are placed before the \mbox{\texttt{-I <sigobj>}} option that is used in invocations of compiler.
This option gives the user a way of over-riding code in the core distribution as the compiler will find their code before the distribution's.

\index{Holmake@\holmake!recursive invocation}
By default, directories specified in the \texttt{INCLUDES} and \texttt{PRE\_INCLUDES} directory are also built by \holmake{} before it attempts to build in the current directory.
If the \texttt{-r} (``force recursion'') command-line flag is used, these directories are also ``clean''-ed when a cleaning target is given to \holmake{}.

The \texttt{OPTIONS} variable is used for the specification of just
four possible options (others are ignored): \texttt{NO\_SIGOBJ},
\texttt{NO\_OVERLAY}, \texttt{NO\_PREREQS} and
\texttt{QUIT\_ON\_FAILURE}.  The \texttt{OPTIONS} variable should be a
list of strings, containing some of the above four options.  Those
present are enabled.  These have the same effect as the corresponding
command-line options. The \texttt{EXTRA\_CLEANS} variable is used to
specify the name of additional files that should be deleted when a
\texttt{Holmake clean} command is issued.

Under Poly/ML, the \texttt{POLY\_CLINE\_OPTIONS} variable can be used to pass run-time options to the Poly/ML executable that is run during theory construction.

Within a command, the variable \texttt{\$<} is used to stand for the
name of the first dependency of the rule.  The variable \texttt{\$@} is
used to stand for the target of the rule.

Finally there are variables that expand to program names and other
useful information:
\begin{description}
\item[\texttt{CP}] This variable is replaced by an operating-system
  appropriate program to perform a file copy.  The file to be copied
  is the first argument, the second is the place to copy to.  The
  second argument can be a directory.  (Under Unix, \texttt{CP}
  expands to \texttt{/bin/cp}; under Windows, it expands to
  \texttt{copy}.)
\item[\texttt{HOLDIR}] The root of the HOL installation.
\item[\texttt{HOLMOSMLC}] This variable is replaced by an invocation
  of the Moscow ML compiler along with the \texttt{-q} flag (necessary
  for handling quotations), and the usual \texttt{-I} include
  specifications (pre-includes, the hol-directory include, and the
  normal includes).
\item[\texttt{HOLMOSMLC-C}] This variable is the same as
  \texttt{HOLMOSMLC} except that it finishes with a closing
  \texttt{-c} option (hence the name) followed by the name of the
  system's overlay file.  This is needed for compilation of HOL source
  files, but not for linking of HOL object code, which can be done
  with \texttt{HOLMOSMLC}.
\item[\texttt{ML\_SYSNAME}] The name of the ML system being used:
  either \texttt{mosml} or \texttt{poly}.
\item[\texttt{MLLEX}] This is the path of the \texttt{mllex} tool that
  is built as part of HOL's configuration.
\item[\texttt{MLYACC}] This is the path of the \texttt{mlyacc} tool that
  is built as part of HOL's configuration.
\item[\texttt{MOSMLC}] This is replaced by an invocation of the
  compiler along with just the normal includes.
\item[\texttt{MOSMLLEX}] This is replaced by an invocation of the
  \texttt{mosmllex} program that comes with the Moscow ML
  distribution.
\item[\texttt{MOSMLYAC}] This is replaced by an invocation of the
  \texttt{mosmlyac} program that comes with the Moscow ML
  distribution.
\item[\texttt{MV}] This variable is replaced by an operating-system
  appropriate program to perform a file movement.  The file to be
  moved is the first argument, the second is the place to move to.
  The second argument can be a directory.  (Under Unix, \texttt{MV}
  expands to \texttt{mv}; under Windows, it expands to \texttt{rename}.)
\item[\texttt{OS}] This variable is replaced by the name of the
  current operating system, which will be one of the strings
  \texttt{"linux"}, \texttt{"solaris"}, \texttt{"macosx"},
  \texttt{"unix"} (for all other Unices), or \texttt{"winNT"}, for all
  Microsoft Windows operating systems (those of the 21st century,
  anyway).
\item[\texttt{SIGOBJ}] Effectively \varref{HOLDIR}\texttt{/sigobj},
  where HOL object code is stored.
  \item[\texttt{UNQUOTE}] The location of the quotation-filter executable.
\end{description}
The \texttt{MOSMLLEX} and \texttt{MOSMLYAC} abbreviations are really
only useful if the originals aren't necessarily going to be on the
user's ``path''.  For backwards compatibility, the five variables
above including the sub-string ``\texttt{MOSML}'' in their names can
also be used by simply writing their names directly (i.e., without the
enclosing \varref{\dots}), as long as these references occur first on
a command-line.

Under Poly/ML, commands involving the variable \texttt{MOSMLC} are interpreted ``appropriately''.
If the behaviour is not as desired, we recommend using \texttt{ifdef~POLY}~(see below) to write rules that pertain only to HOL under Poly/ML.
We strongly discourage the use of \texttt{MOSMLYAC} and \texttt{MOSMLLEX}, even when running HOL under Moscow~ML.

If a reference is made to an otherwise undefined string, then it is
treated as a reference to an environment variable.  If there is no
such variable in the environment, then the variable is silently given
the empty string as its value.

\paragraph{Conditional Parts of Makefiles}
\index{Holmake@\holmake!conditional inclusion of sections}
As in GNU~\textsf{make}, parts of a \texttt{Holmakefile} can be included or excluded dynamically, depending on tests that can be performed on strings including variables.
%
This is similar to the way directives such as \texttt{\#ifdef} can be used to control the C~preprocessor.

There are four possible directives in a \texttt{Holmakefile}: \texttt{ifdef}, \texttt{ifndef}, \texttt{ifeq} and \texttt{ifneq}.
%
The versions including the extra `n' character reverse the boolean sense of the test.
%
Conditional directives can be chained together with \texttt{else} directives, and must be terminated by the \texttt{endif} command.
%
The following example is a file that only has any content if the \texttt{POLY} variable is defined, which happens when Poly/ML is the underlying \ML{} system.
\begin{hol}
\begin{verbatim}
ifdef POLY
TARGETS = target1 target2

target1: dependency1
      build_command -o target1 dependency1
endif
\end{verbatim}
\end{hol}
The next example includes chained \texttt{else} commands:
\begin{hol}
\begin{verbatim}
ifeq "$(HOLDIR)" "foo"
VAR = X
else ifneq "$(HOLDIR)" "bar"
VAR = Y
else
VAR = Z
endif
\end{verbatim}
\end{hol}
\index{ifeq (Holmake directive)@\texttt{ifeq} (Holmake directive)}
\index{ifneq (Holmake directive)@\texttt{ifneq} (Holmake directive)}
The \texttt{ifneq} and \texttt{ifeq} forms test for string equality.
%
They can be passed their arguments as in the example, or delimited with apostrophes, or in parentheses with no delimiters, as in:
\begin{hol}
\begin{verbatim}
ifeq ($(HOLDIR),$(OTHERDIR))
VAR = value
endif
\end{verbatim}
\end{hol}

\index{ifdef (Holmake directive)@\texttt{ifdef} (Holmake directive)}
\index{ifndef (Holmake directive)@\texttt{ifndef} (Holmake directive)}
The definedness tests \texttt{ifdef} and \texttt{ifndef} test if a name has a non-null expansion in the current environment.
%
This test is just of one level of expansion.
%
In the following example, \texttt{VAR} is defined even though it ultimately expands to the emptry string, but \texttt{NULL} is not.
%
The variable \texttt{FOOBAR} is also not defined.
\begin{hol}
\begin{verbatim}
NULL =
VAR = $(NULL)
\end{verbatim}
\end{hol}
Note that environment variables with non-empty values are also considered to be defined.

\index{Holmake@\holmake|)}


\section{Generating and Using Heaps in Poly/ML \HOL{}}
\label{sec:polyml-heaps}

\index{heaps (in Poly/ML)|(}
\index{Poly/ML}
\index{Moscow ML}
Poly/ML has a nice facility whereby the state of one of its interactive sessions can be stored on disk and then reloaded.
This allows for an efficient resumption of work in a known state.
The \HOL{} implementation uses this facility to implement the \texttt{hol} executable.
In Poly/ML, \texttt{hol} starts immediately.
In Moscow~ML, \texttt{hol} starts up by visibly (and relatively slowly) ``loading'' the various source files that provide the system's functionality (\eg, \ml{bossLib}).

Users can use the same basic technology to ``dump'' heaps of their own.
Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories.
This can make developing big mechanisations considerably more pleasant.

\subsection{Generating \HOL{} Heaps}

The easiest way to generate a \HOL{} heap is to use the \texttt{buildheap} executable that is built as part of the standard build process for (Poly/ML)~\HOL.
This program takes a list of object files to include in a heap, an optional heap to build upon (use the \texttt{-b} command-line switch; the default is to use the heap behind the core \texttt{hol} executable), and an optional name for the new heap (the default is the traditional Unix \texttt{a.out}).
Thus the command-line
\begin{alltt}
   buildheap -o realheap transcTheory polyTheory
\end{alltt}
would build a heap in the current directory called \texttt{realheap}, and would preload it with the standard theories of transcendental numbers and real-valued polynomials.

A reasonable way to manage the generation of heaps is to use a \texttt{Holmakefile}.
For example, the \texttt{realheap} above might be generated with the source in Figure~\ref{fig:realheap-makefile}.
The use of the special variable \texttt{HOLHEAP} has a number of nice side effects.
First, it makes the given file a dependency of all other products in the current directory.
This means that the \HOL{} heap will be built first.
Secondly, the other products in the current directory will be built on top of that heap, not the default heap behind \texttt{hol}.
\begin{figure}
\begin{alltt}
   ifdef POLY
   HOLHEAP = realheap
   OBJNAMES = polyTheory transcTheory
   DEPS = $(patsubst %,$(dprot $(SIGOBJ)/%),$(OBJNAMES))

   $(HOLHEAP): $(DEPS)
           $(protect $(HOLDIR)/bin/buildheap) -o $@ $(OBJNAMES)
   endif
\end{alltt}
\caption{A \texttt{Holmakefile} fragment for building a custom \HOL{} heap embodying the standard real number theories.
If the heap's dependencies are not core \HOL{} theories as they are here, then both the dependency line and the arguments to \texttt{buildheap} will need to be adjusted to link to the directory containing the files.
For core \HOL{} theories, the dependency has to mention the \texttt{SIGOBJ} directory, but when passing arguments to \texttt{buildheap}, that information doesn't need to be provided as \texttt{SIGOBJ} is always consulted by all \HOL{} builds.
Finally, note how the use of the \texttt{dprot} and \texttt{protect} functions will ensure that \holmake{} will do the right thing even when \texttt{HOLDIR} contains spaces.}
\label{fig:realheap-makefile}
\end{figure}

\subsection{Using \HOL{} Heaps}
As just described, if a \texttt{Holmakefile} specifies a \texttt{HOLHEAP}, then files in that directory will be built on top of that heap rather than the default.
This is also true if the specified heap is in another directory (\ie, the \texttt{HOLHEAP} line might specify a file such as \texttt{otherdir/myheap}).
In this case, the \texttt{Holmakefile} won't (shouldn't) include instructions on how to build that heap, but the advantages of that heap are still available.
Again, that heap is also considered a dependency for all files in the current directory, so that they will be rebuilt if it is newer than they are.

It is obviously important to be able to use heaps interactively.
If the standard \texttt{hol} executable is invoked in a directory where there is a \texttt{Holmakefile} specifying a heap, the default heap will not be used and the given heap will be used instead.
The fact that this is happening is mentioned as the interactive session begins.
For example:
\begin{samepage}
\begin{alltt}
---------------------------------------------------------------------
       HOL-4 [Kananaskis 8 (stdknl, built Tue Jul 24 16:48:44 2012)]

       For introductory HOL help, type: help "hol";
---------------------------------------------------------------------

[extending loadPath with Holmakefile INCLUDES variable]
[In non-standard heap: computability-heap]
Poly/ML 5.4.1 Release
>
\end{alltt}
\end{samepage}

Finally, note that heaps are required to be built first in a directory, and that heaps embody theories or \ML{} sources that are \emph{ancestral} to the directory in which the heap occurs.
This has the unfortunate consequence that one cannot package up a heap embodying the standard theories for the real numbers in \texttt{src/real}, but that such a heap has to built in some other directory.
This is counter-intuitive.

\index{heaps (in Poly/ML)|)}
\section{Timing and Counting Theorems}

\index{counting inferences, in HOL proofs@counting inferences, in \HOL{} proofs|(}
\index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|(}
\index{timing of HOL evaluations@timing of \HOL{} evaluations|(}


\HOL{} can be made to record its use of primitive
inferences, axioms, definitions and use of oracles.  Such recording is
enabled with the function

\begin{holboxed}
\index{counting_thms@\ml{counting\_thms}|pin}
\begin{verbatim}
   val counting_thms : bool -> unit
\end{verbatim}
\end{holboxed}

\noindent (This function as with all the others in this section is
found in the \texttt{Count} structure.)

Calling \ml{counting\_thms true} enables counting, and
\ml{counting\_thms false} disables it.  The default is for counting to
be disabled.  If it is enabled, whenever \HOL{} performs a primitive
inference (or accepts an axiom or definition) a counter is
incremented.  A total count as well as counts per primitive inference
are maintained.  The value of this counter is returned by the
function:

\begin{holboxed}
\index{thm_count@\ml{thm\_count}|pin}
\begin{verbatim}
  val thm_count : unit ->
   {ASSUME : int, REFL : int, BETA_CONV : int, SUBST : int,
    ABS : int, DISCH : int, MP : int, INST_TYPE : int, MK_COMB : int,
    AP_TERM : int, AP_THM : int, ALPHA : int, ETA_CONV : int,
    SYM : int, TRANS : int, EQ_MP : int, EQ_IMP_RULE : int,
    INST : int, SPEC : int, GEN : int, EXISTS : int, CHOOSE : int,
    CONJ : int, CONJUNCT1 : int, CONJUNCT2 : int, DISJ1 : int,
    DISJ2 : int, DISJ_CASES : int, NOT_INTRO : int, NOT_ELIM : int,
    CCONTR : int, GEN_ABS : int, definition : int, axiom : int,
    from_disk : int, oracle :int, total :int }
\end{verbatim}\end{holboxed}

\noindent This counter can be reset with the function:

\begin{holboxed}
\index{reset_thm_count@\ml{reset\_thm\_count}|pin}
\begin{verbatim}
   val reset_thm_count : unit -> unit
\end{verbatim}\end{holboxed}

Finally, the \texttt{Count} structure also includes another function
which easily enables the number of inferences performed by an \ML{}
procedure to be assessed:

\begin{holboxed}
\index{Count.apply@\ml{Count.apply}|pin}
\begin{verbatim}
   val apply : ('a -> 'b) -> 'a -> 'b
\end{verbatim}
\end{holboxed}

An invocation, \ml{Count.apply f x}, applies the function \ml{f} to
the argument \ml{x} and performs a count of inferences during this
time.  This function also records the total time taken in the
execution of the application.

For example, timing the action of \ml{numLib}'s \ml{ARITH\_CONV}:

\setcounter{sessioncount}{1}
\begin{session}
\begin{verbatim}
- Count.apply numLib.ARITH_CONV ``x > y ==> 2 * x > y``;
runtime: 0.010s,    gctime: 0.000s,     systime: 0.000s.
Axioms asserted: 0.
Definitions made: 0.
Oracle invocations: 0.
Theorems loaded from disk: 0.
HOL primitive inference steps: 165.
Total: 165.
> val it = |- x > y ==> 2 * x > y = T : thm
\end{verbatim}
\end{session}

\index{counting inferences, in HOL proofs@counting inferences, in \HOL{} proofs|)}
\index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|)}
\index{timing of HOL evaluations@timing of \HOL{} evaluations|)}


\section{Embedding \HOL{} in \LaTeX{}}

\index{LaTeX@\LaTeX!embedding HOL@embedding in \HOL{}|(}
%
When writing documents in \LaTeX{} about one's favourite \HOL{} development, one frequently wants to include pretty-printed terms, types and theorems from that development.
%
Done manually, this will typically require involved use of the \texttt{alltt} environment, and cutting and pasting from a HOL session or theory file.
%
The result is that one must also keep two copies of \HOL{} texts synchronised: if the \HOL{} development changes, the \LaTeX{} document should change as well.

\newcommand{\munge}{\texttt{munge.exe}}
\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})}
%
This manual, and error-prone process is not necessary: the standard \HOL{} distribution comes with a tool called \munge{} to automate the process, and to remove the duplicate copies of \HOL{} text.
%
(Strictly speaking, the distribution comes with a tool that itself creates \munge{}; see Section~\ref{sec:munger-creation} below.)
%
The basic philosophy is that a \LaTeX{} document can be written ``as normal'', but that three new \LaTeX{}-like commands are available to the author.

The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter.
%
For example, one might write a document called \texttt{article.htex}.
%
This document contains instances of the new commands, and cannot be processed as is by \LaTeX{}.
%
Instead one first runs
\begin{alltt}
   \munge < article.htex > article.tex
\end{alltt}
and then runs \LaTeX{} on \texttt{article.tex}.
%
One would probably automate this process with a makefile of course.

\subsection{Munging Commands}
\label{sec:munging-commands}
% need to get backslashes conveniently obscures the real names,
% preventing the munger from seeing them, which will be useful when we
% run the munger over this document!
\newcommand{\holtm}{\texttt{\bs{}HOLtm}}
\newcommand{\holty}{\texttt{\bs{}HOLty}}
\newcommand{\holthm}{\texttt{\bs{}HOLthm}}
\paragraph{Before Starting} In order to use the munger, one must ``include'' (use the \texttt{\bs{}usepackage} command) the \texttt{holtexbasic.sty} style-file, which is found in the HOL source directory \texttt{src/TeX}.

\bigskip
There are then three commands for inserting text corresponding to \HOL{} entities into \LaTeX{} documents: \holtm, \holty{} and \holthm.
%
Each takes one argument, specifying something of the corresponding \HOL{} type.
%
In addition, options can be specified in square brackets, just as would be done with a genuine \LaTeX{} command.
%
For example, one can write
\begin{alltt}
   \holtm{}[tt]\{P(SUC n) /\bs{} q\}
\end{alltt}
and one will get \[
  \texttt{$P$ (SUC $n$) $\land$ $q$}
\]
or something very close to it, appearing in the resulting document.\footnote{The output is a mixture of typewriter font and math-mode characters embedded in a \texttt{\bs{}texttt} block within an \texttt{\bs{}mbox}.}
%
Note how the spacing in the input (nothing between the \texttt{P} and the \texttt{SUC n}) is \emph{not} reflected in the output; this is because the input is parsed and pretty-printed with \HOL{}.
%
This means that if the \HOL{} input is malformed, the \munge{} program will report errors.
%
Note also how the system knows that \texttt{P}, \texttt{n} and \texttt{q} are variables, and that \texttt{SUC} is not.
%
This analysis would not be possible without having \HOL{} actually parse and print the term itself.

The default behaviours of each command are as follows:
\begin{description}
\item[\holty\{\textit{\mdseries{string}}\}]
%
\index{HOLty (munging command)@\holty{} (munging command)}
%
Parses the string argument as a type (the input must include the leading colon), and prints it.
%
The output is suited for inclusion in the normal flow of \LaTeX{} (it is an \texttt{\bs{}mbox}).
\item[\holtm\{\textit{\mdseries{string}}\}]
%
\index{HOLtm (munging command)@\holtm{} (munging command)}
%
Parses the string argument as a term, and prints it.
%
Again, the output is wrapped in an \texttt{\bs{}mbox}.

\paragraph{Important:} If the string argument includes a right-brace character
(\ie, the character \rb, which has ASCII code 125), then it must be
escaped by preceding it with a backslash~(\bs).  Otherwise, the
munger's lexer will incorrectly determine that the argument ends at
that right-brace character rather than at a subsequent one.
\item[\holthm\{\textit{\mdseries{thmspecifier}}\}]
%
\index{HOLthm (munging command)@\holthm{} (munging command)}
%
The argument should be of the form $\langle\mbox{\textit{theory}}\rangle\texttt{.}\langle{\mbox{\textit{theorem-name}}}\rangle$.
%
For example, \verb|\HOLthm{bool.AND_CLAUSES}|.
%
This prints the specified theorem with a leading turnstile.
%
\index{Hol_datatype@\ml{Hol\_datatype}!printing in LaTeX@printing in \LaTeX{}}
However, as a special case, if the theorem specified is a ``datatype theorem'' (with a name of the form \texttt{datatype\_}$\langle$\textit{type-name}$\rangle$), a BNF-style description of the given type (one that has been defined with \ml{Hol\_datatype}) will be printed.
%
Datatype theorems with these names are automatically generated when \ml{Hol\_datatype} is run.

By default, the output is \emph{not} wrapped in an \texttt{\bs{}mbox}, making it best suited for inclusion in an environment such as \texttt{alltt}.
(The important characteristics of the \texttt{alltt} environment are that it respects layout in terms of newlines, while also allowing the insertion of \LaTeX{} commands.
The \texttt{verbatim} environment does the former, but not the latter.)
\end{description}

\paragraph{Munging Command Options}
\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!command options}
There are a great many options for controlling the behaviour of each of these commands.
%
Some apply to all three commands, others are specific to a subset.
%
\newcommand{\indentoption}{\gt\gt}
If multiple options are desired, they should be separated by commas. For example: \texttt{\holthm{}[nosp,p/t,\indentoption]\{bool.AND\_CLAUSES\}}.

\begin{description}
\item[\texttt{alltt}] Makes the argument suitable for inclusion in an \texttt{alltt} environment.
%
This is the default for \holthm.
\item[\texttt{case}] (Only for use with \holtm.)
%
Causes the string to be parsed in such a way that any embedded \texttt{case} terms are only partly parsed, allowing their input form to appear when they are output.
%
This preserves underscore-patterns, for example.

\item[\texttt{conj}$n$] (Only for use with \holthm.)
Extracts the $n^{\mbox{\scriptsize th}}$ conjunct of a theorem.
The conjuncts are numbered starting at $1$, not $0$.
For example,
\begin{verbatim}
  \HOLthm[conj3]{bool.AND_CLAUSES}
\end{verbatim}
extracts the conjunct $\vdash \texttt{F} \land t \iff \texttt{F}$.

\item[\texttt{def}] (Only for use with \holthm.)
%
Causes the theorem to be split into its constituent conjuncts, for each conjunct to have any outermost universal quantifiers removed, and for each to be printed on a line of its own.
%
The turnstiles usually printed in front of theorems are also omitted.
%
This works well with definitions (or characterising theorems) over multiple data type constructors, changing
\begin{alltt}
\(\vdash\) (FACT 0 = 1) \(\land\) (\(\forall\)\ensuremath{n}. FACT (SUC \ensuremath{n}) = SUC \ensuremath{n} * FACT \ensuremath{n})
\end{alltt}
into
\begin{alltt}
   FACT 0 = 1
   FACT (SUC \ensuremath{n}) = SUC \ensuremath{n} * FACT \ensuremath{n}
\end{alltt}

\item[\texttt{K}] (Only for use with \holtm.)
%
The argument must be the name of a theorem (as per the \holthm{} command), and the theorem should be of the form
\[
\vdash f\;x\;t
\]
for some term $t$.
%
The command prints the term $t$.
%
\index{combinators, in HOL logic@combinators, in \HOL{} logic}
\index{K, the HOL constant@\ml{K}, the \HOL{} constant}
The expectation is that $f$ will be the combinator \holtxt{K} from \theoryimp{combin} (see Section~\ref{sec:combinTheory}), and that $x$ will be truth~(\holtxt{T}), allowing $t$ to be anything at all.
%
In this way, large complicated terms that are not themselves theorems (or even of boolean type), can be stored in \HOL{} theories, and then printed in \LaTeX{} documents.

\item[\texttt{merge}, \texttt{nomerge}] (For use with \holtm{} and \holthm.)
By default, the HOL pretty-printer is paranoid about token-merging, and will insert spaces between the tokens it emits to try to ensure that what is output can be read in again without error.
%
This behaviour can be frustrating when getting one's \LaTeX{} to look ``just so'', so it can be turned off with the \texttt{nomerge} option.

Additionally, this behaviour can be turned off globally with the \texttt{--nomergeanalysis} option to the munger.
%
If this has been made the default, it may be useful to occasionally turn the merge analysis back on for a particular term or theorem; this is done with the \texttt{merge} option.
%
(In interactive HOL, the token-merging analysis is controlled by a trace variable called \texttt{"pp\_avoids\_symbol\_merges"}.)


\item[\texttt{nodollarparens}] (For use with \holtm{} and \holthm.) Causes the default escaping of syntactic sugar to be suppressed.
\index{ escape, in HOL logic parser@\ml{\$} (escape, in \HOL{} logic parser)}%
\index{tokens!suppressing parsing behaviour of}
The default behaviour is to use parentheses, so that
% encode all the special characters below so that emacs font-locking has a reasonable chance of working
\begin{alltt}
   \holtm\lb\dol/\bs p\rb
\end{alltt}
would get printed as $(\land)\;\,p$.
Note that this doesn't reflect the default behaviour in the interactive loop, which is to use dollar-signs (as in the input above); see Section~\ref{sec:parser:architecture}.
However, with the \texttt{nodollarparens} option specified, nothing at all is printed to indicate that the special syntax has been ``escaped''.

\item[\texttt{nosp}] (Only for use with \holthm.)
%
By default, arguments to \holthm{} are fully specialised (\ie, they have \ml{SPEC\_ALL} applied to them), removing outermost universal quantifiers.
%
The \texttt{nosp} option prevents this.

\item[\texttt{nostile}] (Only for use with \holthm.)
%
By default, arguments to \holthm{} are printed with a turnstile~($\vdash$).
%
If this option is present, the turnstile is not printed (and the theorem will have its left margin three spaces further left).

\item[\texttt{of}] (Only for use with \holty.)
%
The argument is a string that parses to a \emph{term}, not a type.
%
The behaviour is to print the type of this term.
%
Thus \texttt{\holty{}[of]\{p /\bs{} q\}} will print \texttt{bool}.

If the string includes right-braces, they must be escaped with
back-slashes, just as with the arguments to \holtm.

\item[\texttt{rule}] (Only for use with \holtm{} and \holthm.)
Prints a term (or a theorem's conclusion) using the \texttt{\bs{}infer} command (available as part of the \texttt{proof.sty} package).
This gives a nice, ``natural deduction'' presentation.
\index{natural deduction!presentation style for the LaTeX munger@presentation style for the \LaTeX{} munger}
For example, the term
\begin{alltt}
   (p \bs{}/ q) /\bs{} (p ==> r) /\bs{} (q ==> r) ==> r
\end{alltt}
will print as
\[
\infer{r}{p \lor q & p \Rightarrow r & q \Rightarrow r}
\]
Conjuncts to the left of the outermost implication (if any) will be split into hypotheses separated by whitespace.
For large rules, this style of presentation breaks down, as there may not be enough horizontal space on the page to fit in all the hypotheses.
In this situation, the \texttt{stackedrule} option is appropriate.

The term or theorem must be within a \LaTeX{} math-environment (it is typeset as if inline, with the \texttt{tt} option).

\item[\texttt{showtypes}] (For use with \holthm{} and \holtm.)
%
Causes the term or theorem to be printed with the \texttt{types} trace set to level~1 (equivalent to having the \ml{show\_types} reference set to \ml{true}).

\item[\texttt{stackedrule}] (For use with \holthm{} and \holtm.)
This is similar to the \texttt{rule} option, but causes implication hypotheses to be presented as a ``stack'', centered in a \LaTeX{} array on top of one another.
Thus,
\begin{alltt}
   (p \bs{}/ q) /\bs{} (p ==> r) /\bs{} (q ==> r) ==> r
\end{alltt}
will print as
\[
\infer{r}{\begin{array}{c}p \lor q \\ p \Rightarrow r \\ q \Rightarrow r\end{array}}
\]
For this purely propositional example with single-letter variable names, the result looks a little odd, but if the hypotheses are textually larger, this option is indispensable.

\item[\texttt{tt}] %
Causes the term to be type-set as the argument to a \LaTeX{} command \texttt{\bs{}HOLinline}.
%
The default definition for \texttt{\bs{}HOLinline} is
\begin{verbatim}
   \newcommand{\HOLinline}[1]{\mbox{\textup{\texttt{#1}}}}
\end{verbatim}
This makes the argument suitable for inclusion in standard \LaTeX{} positions.
%
This is the default for \holtm{} and \holty.
%
(The \texttt{\bs{}HOLinline} command is defined in the \texttt{holtexbasic.sty} style file.)

\item[\texttt{width=}$n$] Causes the argument to be typeset in lines of width $n$.
%
The default width is $63$, which seems to work well with 11pt fonts.
%
This default can also be changed at the time the \munge{} command is
run (see Section~\ref{sec:running-munger} below).

\item[\texttt{-}$\mathit{name}$]
%
\index{parsing, of HOL logic@parsing, of \HOL{} logic!overloading}
(Only for use with \holthm{} and \holtm.)
This option causes the printing of the term or theorem to be done with respect to a grammar that has all overloading for $\mathit{name}$ removed.
For example, the command \texttt{\holtm[-+]\lb{}x + y\rb} will print as
\[
\texttt{arithmetic\dol+}\;x\;y
\]
because the underlying constant will no longer map to the string \texttt{"+"} and, in the absence of any other mappings for it, will be printed as a fully qualified name.

\index{integers, the HOL theory of@integers, the \HOL{} theory of}
If the theory of integers is loaded, then the command \texttt{\holtm[-+]\lb{}x + y:int\rb} will print as \[
\texttt{int\_add}\;x\;y
\]
because the mapping from the integer addition constant to \texttt{"+"} is removed, but the mapping to \texttt{"int\_add"} remains, allowing that form to be what is printed.

The \texttt{-} option can be useful when complicated notation involving overloads is first introduced in a document.

\item[\texttt{\indentoption}] Indents the argument.
%
  This option only makes sense when used with the \texttt{alltt} option (the additional spaces will have no effect when inside an \texttt{\bs{}mbox}).
%
  The default indentation is two spaces; if a different indentation is desired, the option can be followed by digits specifying the number of space characters desired.
%
  For example, \texttt{\holthm{}[\indentoption10,...]\{...\}} will indent by 10 spaces.

  Note that simply placing a command such as \holthm{} within its \texttt{alltt} block with a given indentation, for example
\begin{alltt}
   \bs{}begin\{alltt\}
      \holthm\{bool.AND_CLAUSES\}
   \bs{}end\{alltt\}
\end{alltt}
will not do the right thing if the output spans multiple lines.
%
Rather the first line of \HOL{} output will be indented, and the subsequent lines will not.
%
The \texttt{\indentoption} option lets the pretty-printer know that it is printing with a given indentation, affecting all lines of its output.


\item[$\mathit{nm}_1$\texttt{/}$\mathit{nm}_2$] (For use with \holtm{}
  and \holthm{}.)
%
Causes name $\mathit{nm}_1$ to be substituted for name $\mathit{nm}_2$ in the term or theorem.
%
This will rename both free and bound variables, wherever they occur throughout a term.
%
Because it uses instantiation, free variables in theorem hypotheses will get renamed, but bound variables in hypotheses are not affected.
%
(Hypotheses are not printed by default anyway of course.)

If $\mathit{nm}_1$ and $\mathit{nm}_2$ both begin with the colon character then they are parsed as types, and type instantiation is performed on the term or theorem argument instead of variable substitution.
\end{description}


\subsection{Creating a Munger}
\label{sec:munger-creation}

\newcommand{\mkmunge}{\texttt{mkmunge.exe}}
\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!creating a munger}
%
The \HOL{} distribution comes with a tool called \mkmunge.
%
This executable is used to create munge executables that behave as described in this section.
%
A typical invocation of \mkmunge{} is
\begin{alltt}
   \mkmunge \(\langle\mathit{thy}\sb{1}\rangle\)Theory ... \(\langle\mathit{thy}\sb{n}\rangle\)Theory
\end{alltt}
Each commandline argument to \mkmunge{} is the name of a \HOL{} object file, so in addition to theory files, one can also include special purpose SML such as \texttt{monadsyntax}.

The \mkmunge{} program can also take an optional \texttt{-o} argument that is used to specify the name of the output munger (the default is \munge).  For example
\begin{alltt}
   \mkmunge -o bagtexprocess bagTheory
\end{alltt}

The theories specified as arguments to \mkmunge{} determine what theorems are in scope for calls to \holthm, and also determine the grammars that will govern the parsing and printing of the \HOL{} types, terms and theorems.


\subsection{Running a Munger}
\label{sec:running-munger}

\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!running a munger}
Once created, a munger can be run as a filter command, consuming its
standard input, and writing to standard output.
%
It may also write error messages and warnings to its standard error.

Thus, a standard pattern of use is something like
\begin{alltt}
   \munge < article.htex > article.tex
\end{alltt}

However, there are two ways of further modifying the behaviour of the
munger, with command-line options.

\paragraph{Overrides}
Most importantly, one can specify an ``overrides file'' to provide
token-to-\LaTeX{} replacements of what is pretty-printed.
%
The command-line would then look like
\begin{alltt}
   \munge overrides_file < article.htex > article.tex
\end{alltt}
The overrides file is a text file containing lines of the form
\begin{alltt}
   tok width tex
\end{alltt}
where \texttt{tok} is a \HOL{} token, \texttt{width} is a number
giving the width of the \LaTeX{}, and \texttt{tex} is a \LaTeX{}
string.

As a very simple example, an overrides file might consist of just one
line:
\begin{alltt}
   pi1 2 \bs{}ensuremath\{\bs{}pi_1\}
\end{alltt}
This would cause the string \texttt{pi1} (presumably occurring in the
various \HOL{} entities as a variable name) to be replaced with the
rather prettier $\pi_1$.
%
The \texttt{2} records the fact that the
printer should record the provided \LaTeX{} as being 2 characters
wide.
%
This is important for the generation of reasonable line-breaks.

Overrides for \HOL{} tokens can also be provided within \HOL{}
theories, using the
\texttt{TeX\_notation} command (see
Section~\ref{sec:holtheories-tex-ready} below).

\paragraph{Default width}
A munger can specify the default width in which \HOL{} will print its
output with a \texttt{-w} option.
%
For example,
\begin{alltt}
   \munge -w70 < article.htex > article.tex
\end{alltt}
This default width can be overridden on a case-by-case basis with the
\texttt{width=} option to any of the commands within a \LaTeX{}
document.

\paragraph{Preventing Merge Analysis}  As mentioned above in the description of the \texttt{merge} and \texttt{nomerge} options to the \holtm{} and \holthm{} commands, the munger can be configured to not do token-merging avoidance by passing the \texttt{--nomergeanalysis} option to the munger.

\smallskip \noindent The \texttt{-w}, \texttt{--nomergeanalysis} and
overrides file options can be given in any order.

\subsection{Holindex}

\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!Holindex}
Till now, it has been explained how the munger can be used as a preprocessor of \LaTeX{} sources.
Sometimes a tighter interaction with \LaTeX{} is beneficial.
Holindex is a \LaTeX{} package that provides genuine \LaTeX{} commands for inserting \HOL{}-theorems, types and terms as well as many related commands.
This allows it to generate an index of all \HOL{}-theorems, types and terms that occur in the document as well as providing citation commands for \HOL{} entities in this index.
Holindex can be found in \texttt{src/TeX/}.
There is also a demonstration file available in this directory.


\paragraph{Using Holindex}
To use Holindex add \texttt{\bs{}usepackage\{holindex\}} to the header
of the \LaTeX{} source file \texttt{article.tex}. Holindex loads the
\texttt{underscore} package which might cause trouble with references
and citations. In order to avoid problems,
\texttt{holindex} should be included after packages
like \texttt{natbib}. Holindex is used like BibTex or
MakeIndex. A run of \LaTeX{} on \texttt{jobname.tex} creates an
auxiliary file called \texttt{article.hix}. The munger is used to
process this file via
\begin{alltt}
   \munge -index article
\end{alltt}
This call generates two additional auxiliary files,
\texttt{article.tde} and \texttt{article.tid}.  The following runs of
\LaTeX{} use these files. After modifying the source file, the munger
can be rerun to update \texttt{article.tde} and \texttt{article.tid}.
If you are using emacs with AUCTeX to write your latex files, you might
want to add
\begin{verbatim}
(eval-after-load "tex" '(add-to-list 'TeX-command-list
   '("Holindex" "munge.exe -index %s"
     TeX-run-background t t :help "Run Holindex") t))
\end{verbatim}
to your emacs configuration file. This will allow
you to run Holindex using AUCTeX.

\paragraph{Holindex commands}
\begin{description}
\item[\texttt{\bs{}blockHOLthm\{id\}}, \texttt{\bs{}blockHOLtm\{id\}}, \texttt{
    \bs{}blockHOLty\{id\}}] These commands typeset the theorem, term
  or type with the given \texttt{id} as the argument to a \LaTeX{}
  command \texttt{\bs{}HOLblock}. They are intended for
  typesetting multiple lines in a new block.
  For theorem ids of the form \texttt{theory.thm} are predefined. All
  other ids have to be defined before usage as explained below.
%
\item[\texttt{\bs{}inlineHOLthm\{id\}}, \texttt{\bs{}inlineHOLtm\{id\}}, \texttt{\bs{}inlineHOLty\{id\}}]
   These commands are similar to \texttt{\bs{}blockHOLthm\{id\}}, \texttt{\bs{}blockHOLtm\{id\}} and \texttt{
    \bs{}blockHOLty\{id\}}. However, they are intended for inline typesetting and
   use \texttt{\bs{}HOLinline} instead of \texttt{\bs{}HOLblock}.
%
\item[\texttt{\bs{}citeHOLthm\{id\}}, \texttt{\bs{}citeHOLtm\{id\}}, \texttt{\bs{}citeHOLty\{id\}}]
   These commands cite a theorem, term or type.
%
\item[\texttt{\bs{}mciteHOLthm\{id,id,...id\}}, \texttt{\bs{}mciteHOLtm\{ids\}}, \texttt{\bs{}mciteHOLty\{ids\}}]
   These commands cite multiple theorems, terms or types.
%
\item[\texttt{\bs{}citePureHOLthm\{id\}}, \texttt{\bs{}citePureHOLtm\{id\}},
   \texttt{\bs{}citePureHOLty\{id\}}] These commands\linebreak cite a theorems, terms or types.
   They just typeset the number instead of the
   verbose form used by the \texttt{citeHOL} and \texttt{mciteHOL} commands.

\item[\texttt{\bs{}citeHiddenHOLthm\{id\}},
   \texttt{\bs{}citeHiddenHOLtm\{id\}},
   \texttt{\bs{}citeHiddenHOLty\{id\}}] These commands cite a
   theorems, terms or types, but not typeset anything. These commands
   can be used to add a page to the list of pages a theorem, term or
   type is cited.

 \item[\texttt{\bs{}printHOLIndex}, \texttt{\bs{}printHOLShortIndex},
   \texttt{\bs{}printHOLLongIndex}] These commands typeset the index
   of all theorems, terms and types cited in the document.  There are
   two types of entries in the index: long and short ones. Short
   entries contain a unique number, the label of the theorem, term or
   type and the pages it is cited.  Long entries contain additionally
   a representation as it would be inserted by
   \texttt{\bs{}blockHOL...} as well as an optional description.
   Theorems use by default short entries, while terms and types use
   long ones.  It is possible to change for each item whether a long
   or short entry should be used. \texttt{\bs{}printHOLIndex} prints
   the default index with mixed long and short entries.
   \texttt{\bs{}printHOLLongIndex} typesets just long entries and
   \texttt{\bs{}printHOLShortIndex} just short ones.
\end{description}


\paragraph{Defining and formating Terms, Types and Theorems}

  Most of the Holindex commands require an identifier of a theorem,
  term or type as arguments. Theorem identifiers of the form
  \texttt{theory.theorem} are predefined. All other identifiers need
  defining. Additionally one might want to change the default
  formating options for these new identifiers as well as the old ones.
  \HOL{} definition files can be used for defining and
  setting the formating options of identifiers. They are used by
  putting the command \texttt{\bs{}useHOLfile\{\textit{filename.hdf}\}} in
  the header of your latex source file. These file use a syntax similar to
  BibTex. They consist of a list of entries of the form
  \begin{verbatim}
@EntryType{id,
  option = value,
  boolFlag,
  ...
}
\end{verbatim}
\noindent
There are the following entry types
\begin{description}
\item[\texttt{Thm}, \texttt{Theorem}] used to define and format a
  theorem. If the identifier is of the form \texttt{theory.theorem},
  the \texttt{content} option can be skipped. Otherwise, the
  \texttt{content} option should be of this form and a new identifier
  is defined for the given theorem. This is for example useful if the
  theorem name contains special characters or if a theorem should
  be printed with different formatting options.
  \item[\texttt{Term}]
    used to define and format a term.
  \item[\texttt{Type}]
    used to define and format a type.
  \item[\texttt{Thms}, \texttt{Theorems}] used to set formating options for
    a list of theorems. For example one might want to print long index entries
    for all theorems in a specific theory. For the \texttt{Theorems} entry
    the \texttt{id} part of the entry is given in the form
    \texttt{ids = [id,id,...]}. These \texttt{ids} may be theorem ids or special
    ids of the form \texttt{theorem.thmprefix*}. The id
    \texttt{arithmetic.LESS\_EQ*} for example represents all theorem in
    theory \texttt{arithmetic} whose name starts with \texttt{LESS\_EQ}.
\end{description}
Options are name/value pairs. The value has to be quoted using
quotation marks or \HOL{}'s quotation syntax. There are the following
option names available:
\begin{description}
  \item[\texttt{content}]
    the content. For a term or type that's it's \HOL{}\ definition.
    For theorems it is of the form \texttt{theory.theorem}.
  \item[\texttt{options}]
    formating options for the munger as described in section~\ref{sec:munging-commands}.
    Please use the Holindex commands for typsetting inline or as a block instead
    of the options \texttt{tt} or \texttt{alltt}.
  \item[\texttt{label}] the label that will appear in the index. For
    theorems the label is by default it's name and the label given here
    will be added after the name.
  \item[\texttt{comment}] latex code that gets typeset as a comment / description
    for long index entries.
  \item[\texttt{latex}] the latex code for the item. There are very rare cases,
    when it might be useful to provide handwritten \LaTeX{} code instead of the one
    generated by the munger. This option overrides the \LaTeX{} produced by the munger.
    It is recommended to use it very carefully.
\end{description}
Besides options, there are also boolean flags that change the formating of entries:
\begin{description}
  \item[\texttt{force-index}]
    adds the entry to the index, even if it is not cited in the document.
  \item[\texttt{long-index}]
    use a long index-entry.
  \item[\texttt{short-index}]
    use a long index-entry.
\end{description}
Here is an example of such a \HOL{} definition file:

\begin{verbatim}
@Term{term_id_1,
   content = ``SOME_FUN = SUC a < 0 /\ 0 > SUC b``,
   options = "width=20",
   label = "a short description of term from external file",
   comment = "some lengthy\\comment

              with \textbf{formats} and newlines",
   force_index
}

@Type{type_id_1,
   content = ``:bool``
}

@Thm{arithmetic.LESS_SUCC_EQ_COR,
   force-index, long-index
}

@Thm{thm_1,
   label = "(second instance)",
   content = "arithmetic.LESS_SUC_EQ_COR"
}

@Theorems{
   ids = [arithmetic.LESS_ADD_SUC,
          arithmetic.LESS_EQ*],
   force-index
}
\end{verbatim}


\paragraph{Configuring Holindex}

There are some commands that can be used to change the overall behaviour
of Holindex. They should be used in the header directly after \texttt{holindex}
is included.
\begin{description}
\item[\texttt{\bs{}setHOLlinewidth}] sets the default line-width. This
   corresponds to the \texttt{-w} option of the munger.

\item[\texttt{\bs{}setHOLoverrides}] sets the ``overrides file'' to provide
token-to-\LaTeX{} replacements of what is pretty-printed.

\item[\texttt{\bs{}useHOLfile}]
is used to include a \HOL{} definition file. Several such files might be
included.
\end{description}


\paragraph{Additional Documentation}
For more information about Holindex, please refer to
the demonstration file \texttt{src/TeX/holindex-demo.tex}. This file contains
documentation for rarely used commands as well as explanations of how to
customise Holindex.


\subsection{Making \HOL{} Theories \LaTeX{}-ready}
\label{sec:holtheories-tex-ready}

Though one might specify all one's desired token-replacements in an \texttt{overrides} file, there is also support for specifying token replacements in the theory where tokens are first ``defined''.
%
(Of course, \emph{tokens} aren't defined \textit{per se}, but the definition of particular constants will naturally give rise to the generation of corresponding tokens when those constants appear in HOL terms, types or theorems.)

A token's printing form is given in a script-file with the \ml{TeX\_notation} command (from the \ml{TexTokenMap} module).
%
This function has type
\begin{alltt}
   \{ hol : string, TeX : string * int \} -> unit
\end{alltt}
The \ml{hol} field specifies the string of the token as \HOL{} prints it.
%
The \ml{TeX} field specifies both the string that should be emitted into the \LaTeX{} output, and the width that this string should be considered to have (as in the \texttt{overrides} file).

For example, in \texttt{boolScript.sml}, there are calls:
\begin{alltt}
   val _ = TeX_notation \{ hol = "!", TeX = ("\bs{}\bs{}HOLTokenForall\{\}", 1)\}
   val _ = TeX_notation \{ hol = UChar.forall,
                          TeX = ("\bs{}\bs{}HOLTokenForall\{\}", 1)\}
\end{alltt}
The \texttt{UChar} structure is a local binding in the script-file that points at the standard list of UTF8-encoded Unicode strings in the distribution (\ml{UnicodeChars}).
%
Note also how the backslashes that are necessary for the \LaTeX{} command have to be doubled because they are appearing in an SML string.

Finally, rather than mapping the token directly to the string \texttt{\bs{}forall} as one might expect, the mapping introduces another level of indirection by mapping to \texttt{\bs{}HOLTokenForall}.
%
Bindings for this, and a number of other \LaTeX{} commands are made in the file
\begin{alltt}
   src/TeX/holtexbasic.sty
\end{alltt}
which will need to be included in the \LaTeX{} source file.
%
(Such bindings can be overridden with the use of the command \texttt{\bs{}renewcommand}.)

Finally, all theory-bindings made with \ml{TeX\_notation} can be overridden with \texttt{overrides} files referenced at the time a munger is run.


\index{LaTeX@\LaTeX!embedding HOL@embedding in \HOL{}|)}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "description"
%%% End:

%  LocalWords:  HOL mechanisations HOLHEAP Holmakefile