xref: /seL4-l4v-master/HOL4/Manual/Description/misc.tex

\chapter{Miscellaneous Features}

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 always 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.
  As such theorems are pretty-printed into the corresponding \texttt{Theory.sig} file, the help system will find both the declaration in the signature (\eg, \ml{val~nm~:thm}), and the entry for that theorem in the comment-block.
\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{\texorpdfstring{Maintaining \HOL{} Formalizations with \holmake}{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{Source conventions for script and SML files}

\paragraph{Script and theory files}
The file that generates the \HOL{} theory \textit{my}\texttt{Theory} must be called \textit{my}\texttt{Script.sml}.
After the theory has been successfully generated, it can be \texttt{open}-ed at the head of other developments:
\begin{alltt}
    open myTheory
\end{alltt}
\index{load (ML function)@\ml{load} (\ML{} function)}
and it can be loaded interactively:
\begin{alltt}
    load "myTheory";
\end{alltt}
The file \texttt{myScript.sml} should begin with the standard boilerplate:
\begin{alltt}
    open HolKernel Parse boolLib bossLib

    val _ = new_theory "my"
\end{alltt}
This ``boilerplate'' ensures that the standard tactics and SML commands will be in the namespace when the script file is compiled.
Interactively, these modules have already been loaded and \texttt{open}-ed, so what can be typed directly at \texttt{hol} cannot necessarily be included as-is in a script file.
In addition, if \texttt{myTheory} depends on other \HOL{} theories, this ancestry should also be recorded in the script file.
The easiest way to achieve this is simply to \texttt{open} the relevant theories.
Conventionally, the \texttt{open} declarations for such theories appear just before the call to \texttt{new_theory}.
For example:
\begin{alltt}
    open HolKernel Parse boolLib bossLib

    open myfirstAncestorTheory OtherAncestorTheory

    val _ = new_theory "my"
\end{alltt}
\index{load (ML function)@\ml{load} (\ML{} function)}
Interactively, these may well be the names of theories that have been explicitly loaded into the context with the \texttt{load} function.
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.

In addition, simply referring to a theory's theorems using the `dot-notation' will make that theory an ancestor.
For example,
\begin{alltt}
   Theorem mytheorem:
     ...
   Proof
     simp[ThirdAncestorTheory.important_lemma] ...
   QED
\end{alltt}
will record a dependency on \texttt{ThirdAncestoryTheory}, making it just as much an ancestor as the theories that have been explicitly \texttt{open}-ed elsewhere.

Finally, all script files should also end with the invocation:
\begin{verbatim}
    val _ = export_theory()
\end{verbatim}
When the script is finally executed, this call writes the theory to disk.

The calls to \texttt{new_theory} and \texttt{export_theory} must bracket a sequence of SML declarations.
A declaration will typically be a \texttt{val}-binding, but might also be a function definition (\emph{via} \texttt{fun}), an \texttt{open}, or even a \texttt{structure} declaration.
Declarations are \emph{not} expressions.
This means that script files should \emph{not} include bare calls to \HOL{} functions like \texttt{Datatype}.
Instead, declarations such as the following need to be used:
\begin{alltt}
    val _ = Datatype`tree = Lf | Nd num tree tree`
\end{alltt}
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 generally should) omit the bracketing
\begin{alltt}
  structure myScript = struct
  ...
  end
\end{alltt}
lines, but the contents of the file are still interpreted as if belonging to a structure.

Finally, take care not to have the string ``\texttt{Theory}'' appear at the end of 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 ``\texttt{Theory.sml}'' or ``\texttt{Theory.sig}''.
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.

\paragraph{Other SML code}
When developing \HOL{} libraries, one should again attempt to follow Moscow~ML's conventions.
Most importantly, file names should match \texttt{signature} and \texttt{structure} names.
If this can be done, the automatic dependency analysis done by \holmake{} will work ``out of the box''.
A signature for module \texttt{foo} should always appear in file \texttt{foo.sig}, and should have the form
\begin{alltt}
    signature foo =
    sig
      ...
    end
\end{alltt}
The accompanying implementation of \texttt{foo} should appear in file \texttt{foo.sml}, and should have the form
\begin{alltt}
    structure foo :> foo =
    struct
    ...
    end
\end{alltt}
As with theory files, the contents of a \texttt{structure} must be a sequence of declarations only.
Neither sort of file should have any other declarations within it (before or after the \texttt{signature} or \texttt{structure}).

Deviations from this general pattern are possible, but life is much simpler if such deviations can be avoided.
The \HOL{} distribution\footnote{See, for example, the kernel implementation in \texttt{src/0}.} contains some examples of trickier situations where the guidelines need to be ignored.
Ignoring the guidelines will generally result in the need for quite involved \texttt{Holmakefile}s (see Section~\ref{sec:using-Holmakefiles} below).

\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{\holmake{} Limitations}

Without information to the contrary, \holmake{} assumes that all files of interest are in the current directory or in \HOL{}'s master \texttt{sigobj} directory.
Using a \texttt{Holmakefile} (see Section~\ref{sec:using-Holmakefiles}), it is possible to mention files in other directories, both as dependencies and as explicit targets with rules on how those targets should be built.
However, it is probably impossible (or at least, painfully difficult) to describe how theories are built from script files using the \texttt{Holmakefile} language.
Nor will \holmake{} perform its automatic dependency analysis on such ``remote'' files.

\index{Holmake@\holmake!recursive invocation}%
The right approach when a development spans multiple directories is to indicate that there is a dependency on other directories by using the \texttt{-I} flag, or (better) the \texttt{INCLUDES} variable in a \texttt{Holmakefile}.
\holmake{} requires that, just as files must have an acyclic dependency graph, the directories containing those files must have a compatible, and acyclic, \texttt{INCLUDES} graph.
With \texttt{INCLUDES} information to hand, \holmake{} will process the entire \texttt{INCLUDES} graph, looking throughout the graph for theory files that the current directory may depend on, and rebuilding those remote targets as necessary.

\subsection{\holmake{}'s command-line arguments}
\index{Holmake@\holmake!command-line arguments}
Like {\tt make}, \holmake{} takes command-line arguments corresponding to the targets that the user desires to build.
As a special case of this, targets ending with the suffix \ml{Theory} are treated as an instruction to build the theory files that lie behind a \HOL{} theory.
(If successful such a build will enable other script-files to refer to that theory, and for interactive sessions to issue \ml{load~"xTheory";} commands.)
If there are no command-line targets, then \holmake{} will look for a \texttt{Holmakefile} in the current directory.
If there is none, or if that file specifies no targets, then \holmake{} will attempt to build all \ML{} modules and \HOL{} theories it can detect in the current directory.
If there is a target in the \texttt{Holmakefile}, then \holmake{} will try to build the first such target (only).

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[\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{--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[\tt -I <directory>]
  Look in specified directory for additional 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[\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.
If a target in the current directory depends on something in another directory that does not exist, \holmake{} will fail to build it.
If the remote target exists, but is stale, it will be used in its stale state, come what may.
\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 \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},\texttt{--noqof}]
  Where q-o-f stands for ``quit on failure''.
  By default, if a tactic fails to prove a theorem, the running script exits with a failure.
  Depending on the presence or absence of the \texttt{-k} flag, this failure to build a theory may cause \holmake{} to also exit (with a failure).
  With the \texttt{--noqof} option, \holmake{} will cause the running script to use \texttt{mk\_thm} to assert the failed goal, allowing the build to continue and other theorems to be 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[\texttt{-r}]%
\index{Holmake@\holmake!recursive invocation}%
Forces \holmake{} to behave more recursively than it would otherwise.
This overrides the \texttt{--no\_prereqs} option.
When performing a ``clean'' action (prompted by \texttt{clean}, \texttt{cleanAll} or \texttt{cleanDeps} arguments), this cleaning is done recursively through all ``includes'' directories (which is not done otherwise).
When building normally, all targets in ``includes'' directories are built; normally only dependencies of targets in the current directory are built.
\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 error messages such as ``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.

In addition, it is possible to indicate that the built-in process of generating theory files from script files generates side products.
This is done by writing a command-less rule of the form
\begin{alltt}
   target : *thyScript.sml
\end{alltt}
where an asterisk character precedes the name of the script file.
This indicates that the action of executing the code in \texttt{thyScript.sml} will not only generate the usual \texttt{thyTheory.sig} and \texttt{thyTheory.sml} files, but also the file \texttt{target}.
If \holmake{} is asked to build any of these three files, and any is absent or out of date with respect to \texttt{thyScript.sml} (or any other dependency), then the code in \texttt{thyScript.sml} will be run.

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{Special targets}
Some target names for rules are handled specially by \holmake{}:
\begin{itemize}
\item Dependencies associated with the target name \texttt{.PHONY} are taken to be list of other targets in the make-file that are not actually the name of files to be built.
For example, targets naming conceptual collections of files such as \texttt{all} should be marked as ``phony''.
If a target is phony, then its dependencies will be built even if a file of that name exists and is newer than the dependencies.
\item The special way that command-line arguments \texttt{clean}, \texttt{cleanAll} and \texttt{cleanDeps} are handled means that targets of those names will not work.
In order to extend cleaning behaviour, use the \texttt{EXTRA\_CLEANS} variable (see below).
\end{itemize}
\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}.
\item[\texttt{\$(which arg)}] is replaced by the full path to an executable and readable occurrence of a file called \texttt{arg} within a directory in the list of directories in the \texttt{PATH} environment variable.
For example \texttt{\$(which cat)} will usually expand to \texttt{/bin/cat} on Unix-like systems.
If there is no occurrence of \texttt{arg} in any directory in \texttt{PATH}, this function call expands to the empty string.
\item[\texttt{\$(wildcard pattern)}] expands the shell ``glob'' pattern (\eg, \texttt{*Script.sml}) into the list of matching filenames.
If the pattern doesn't match any files, then the function returns \texttt{pattern} unchanged.
\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{}.

\index{CLINE_OPTIONS (Holmakefile variable)@\texttt{CLINE\_OPTIONS} (Holmakefile variable)}%
The \texttt{CLINE\_OPTIONS} variable is used for the specification of command-line switches that are presumably usually appropriate for calls to \holmake{} in the containing directory.
The options present in \texttt{CLINE\_OPTIONS} are used to build a ``base environment'' of switches; this base environment is then overridden by whatever was actually passed on the command-line.
For example, a useful \texttt{CLINE\_OPTIONS} line%
\footnote{Note that a \texttt{-{}-noqof} option in a makefile might be overridden from the command-line with the otherwise useless seeming \texttt{-{}-qof} option.
In addition, the \texttt{-{}-no\_hmakefile} command-line option will stop the makefile from being consulted at all.} %
might be
\begin{alltt}
    CLINE_OPTIONS = -j1 --noqof
\end{alltt}
Under Poly/ML, the similar \texttt{POLY\_CLINE\_OPTIONS} variable can be used to pass run-time options to the Poly/ML executable that is run during theory construction.


\index{EXTRA_CLEANS (Holmakefile variable)@\texttt{EXTRA\_CLEANS} (Holmakefile variable)}%
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.

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{DEBUG\_FLAG}] This variable is replaced by \texttt{"-{}-dbg"} if that flag was passed to \holmake, or the empty string if not.
\item[\texttt{DEFAULT\_TARGETS}]\index{DEFAULT_TARGETS (Holmakefile variable)@\texttt{DEFAULT\_TARGETS} (Holmakefile variable)}%
This variable expands to a list of the targets in the current directory that \holmake{} would build if there was no target in the Holmakefile, and no target was specified on the command-line.
Thus, if one wishes to continue to have all these defaults built alongside an additional target, an appropriate idiom to use at the head of the file would be
\begin{alltt}
    all: $(DEFAULT_TARGETS) mytarget1 mytarget2
    .PHONY: all
\end{alltt}
followed by rules for building the new target(s).

\item[\texttt{HOLDIR}] The root of the HOL installation.
\item[\texttt{HOLHEAP}]
Under Poly/ML, this variable expands to the name of the heap that should be used to build this directory (to be used instead of the heap that underlies the \texttt{hol} executable).
See Section~\ref{sec:polyml-heaps} below for more on using custom heaps with Poly/ML.
\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{KERNELID}]
  The kernel option that was passed to \HOL's \texttt{build} command, stripped of its leading hyphens.
  This will typically be \texttt{stdknl} (the standard kernel) but may take on other values if other custom kernels are being used.
\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{\texorpdfstring{Generating and Using Heaps in Poly/ML \HOL{}}{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{\texorpdfstring{Generating \HOL{} heaps}{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{\texorpdfstring{Using \HOL{} heaps}{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 when using the \texttt{HOLHEAP} variable, heaps are required to be built before everything else in a directory, and that such heaps embody theories or \ML{} sources that are \emph{ancestral} to the directory in which the heap occurs.
Thus, if one wanted to package up a heap embodying the standard theories for the real numbers, and to do it in \texttt{src/real} (which feels natural), this heap could be built using the method described here, but could only be referred to as a \texttt{HOLHEAP} in the directories that used it, \emph{not} in \texttt{src/real}'s \texttt{Holmakefile}.
Subsequently, developments in other directories could use this heap by specifying\[
  \texttt{\$(HOLDIR)/src/real/realheap}
\]
as the value for their \texttt{HOLHEAP} variables.

\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{\texorpdfstring{Embedding \HOL{} in \LaTeX{}}{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{Datatype@\ml{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{Datatype}) will be printed.
%
Datatype theorems with these names are automatically generated when \ml{Datatype} is run.
If the trace \texttt{EmitTeX:~print~datatypes~compactly} is set to 1 (see the \texttt{tr} option below) the description is printed in a more compact form.
Also, if the type is a collection of nullary constants (a type consisting of only ``enumerated constants''), then it will always be printed compactly.
When not compact, all of a type's constructors will appear on the same line, or each will be on a separate line.

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, and a special form of equality is printed for the top-level (``defining'') equality in each clause.
%
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 \HOLTokenDefEquality{} 1
   FACT (SUC \ensuremath{n}) \HOLTokenDefEquality{} SUC \ensuremath{n} * FACT \ensuremath{n}
\end{alltt}
If the special equality is not desired, the option \texttt{nodefsym} can be used to turn this off.
The special equality symbol can also be redefined by changing the \LaTeX{} definition of the macro \ml{\bs{}HOLTokenDefEquality}.

There are two variations on the \texttt{def} option:
\begin{description}
\item[\texttt{spaceddef}:]%
\index{spaceddef, HOL in LaTeX option@\ml{spaceddef}, \HOL{} in \LaTeX{} option}%
This option adds extra blank lines between successive conjuncts of a definition.
\item[\ml{aligneddef}:]%
\index{aligneddef, HOL in LaTeX option@\ml{aligneddef}, \HOL{} in \LaTeX{} option}%
This option puts ampersands around the \ml{\bs{}HOLTokenDefEquality} macro call in the emitted \LaTeX{}.
If the \LaTeX{} environment is an \texttt{array} or similar, this can ensure a nice column-based layout for one's definitions.
\end{description}
Both options can be used together, but \ml{aligneddef} will not work if \ml{nodefsym} is also used; if this combination is really required, it would be better to temporarily redefine (use \ml{\bs{}renewcommand}) \ml{\bs{}HOLTokenDefEquality}.


\item[\texttt{depth}=$n$]
Causes printing to be done with a maximum print depth of $n$; see Section~\ref{sec:pretty-print-depth}.

\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.

\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!math mode}
\index{math mode (in the LaTeX munger)@math mode (in the \LaTeX{} munger)}
\item[\texttt{m}$\mathit{space}$,\texttt{nomath}] The \texttt{m} option makes \HOL{} material be typeset in ``math-mode''.
In particular, the output of the pretty-printer will be modified so that newline characters are replaced by \texttt{\bs\bs} commands.
This then requires that the surrounding \LaTeX{} environment be array-like, so that the \texttt{\bs\bs} command will have the desired effect.

In addition, because raw spaces have minimal effect in math-mode (something like \texttt{f\textvisiblespace{}x} will be typeset as $f x$), math-mode munging also replaces spaces with math-mode macros.
By default, the command \texttt{\bs;\bs;} is used, but if the \texttt{m} option is followed by some characters, each is interpreted as a single-letter macro name, with each macro concatenated together to provide the space command that will be used.

For example, if the option is \texttt{m;}, then the spacing command will be \texttt{\bs;}.
If the option is \texttt{m;!}, then the spacing command will be \texttt{\bs;\bs!}.
The comma character cannot be used because it conflicts with parsing the list of options, but one can use \texttt{c} instead, so that the option \texttt{mc} will make the spacing command be \texttt{\bs,}.

The \texttt{m} option can be installed globally with the \texttt{-m} command-line option.
If this option is enabled globally, it can be cancelled on a case-by-case basis by using the \texttt{nomath} option.
The \texttt{nomath} option also takes precedence over any \texttt{m} options that might occur.

See also the discussion about math-mode munging in Section~\ref{sec:math-mode-munging} below.

\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{ dollar sign, in HOL logic parser@\ml{\$} (dollar sign, in \HOL{} logic parser)!as escape character}%
\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).
%
For controlling how the turnstile is printed when this option is not present, see the paragraph on Overrides in Section~\ref{sec:running-munger}.

\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).

For adding a name to the rule, see the \texttt{rulename} option below.

\item[\texttt{rulename=}$\mathit{name}$] (Only has an effect with \texttt{rule} or \texttt{stackedrule}.)
Adds \textit{name} as the optional argument to the \texttt{\bs{}infer} command when typesetting the rule.
The name is wrapped with \texttt{\bs{}HOLRuleName}, which by default is the same as \texttt{\bs{}textsf}.
For ease of parsing options, \textit{name} should not contain braces, brackets, or commas.
(A name including such special characters could be typeset by renewing the \texttt{\bs{}HOLRuleName} command.)

\item[\texttt{showtypes}$n$] (For use with \holthm{} and \holtm.)
%
Causes the term or theorem to be printed with the \texttt{types} trace set to level~$n$.
The $n$ is optional and defaults to $1$ if omitted (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.

For adding a name to the rule, see the \texttt{rulename} option.

\item[\texttt{tr\apost}$\mathit{tracename}$\texttt{\apost=}$n$]
This option allows the temporary setting of the provided trace to the integer value $n$.
For example, one can set \texttt{pp\_unambiguous\_comprehensions} to $1$ to ensure that set comprehensions are printed with bound variables explicitly identified.
See Section~\ref{sec:set-syntax} for more on set comprehensions, and Section~\ref{sec:traces} for more on traces.
\index{traces, controlling HOL feedback@traces, controlling \HOL{} feedback!when munging to LaTeX@when munging to \LaTeX{}}

\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}
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.
When used with \holty, prints the type with all type abbreviations 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} and \texttt{\indentoption\td}] Indents the argument.
%
  These options only make 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.

The version with the tilde character~(\td) does not add indentation to the first line of output, but adds the specified amount (again 2, if no number is provided) to subsequent lines.
This allows one to achieve suitable alignment when other non-HOL text has been put onto the same line.
For example,
\begin{alltt}
  AND_CLAUSES \bs{}HOLthm[width=46,>>~12]\lb{}bool.AND_CLAUSES\rb
  TRUTH       \bs{}HOLthm[>>~12]\lb{}bool.TRUTH\rb
  MAP         \bs{}HOLthm[>>~12,width=50]\lb{}list.MAP\rb
\end{alltt}
ensures correct vertical alignment when extra lines are printed, as they will be with the printing of \ml{bool.AND_CLAUSES} and \ml{list.MAP}.

\item[$\mathit{nm}_1\mathtt{/}\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.

\item[$s\mathtt{//}t$] (For use with \holtm{}, \holthm, and \holty) Causes \LaTeX{} string $s$ to be substituted for token $t$.
This allows one-off manipulation of the override map (see Section~\ref{sec:running-munger} below).
The difference between this operation and the ``normal substitution'' done with a single slash (as above) is that it happens as the \HOL{} entity is printed, whereas normal substitution happens before pretty-printing is done.
If printing depends on particular variable name choices, the ``last minute'' manipulations possible with this form of substitution may be preferable.
The width of the \LaTeX{} string is taken to be the width of the original token $t$.
\end{description}

\subsection{Math-mode munging}
\label{sec:math-mode-munging}
\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!math mode}
\index{math mode (in the LaTeX munger)@math mode (in the \LaTeX{} munger)}

There are a few steps needed to make math-mode munging a relatively painless affair.
First, there are two \LaTeX{} macros from \texttt{holtexbasic.sty} that should probably be overridden:
\begin{description}
\item[\texttt{\bs{}HOLConst}] By default this will print names in typewriter font.
In math mode, this will probably look better in sans serif, suggesting
\begin{verbatim}
   \renewcommand{\HOLConst}[1]{\textsf{#1}}
\end{verbatim}
Depending on personal taste, the \texttt{\bs{}HOLKeyword} macro might be redefined similarly.
This macro is used for keywords such as \texttt{if}.
\item[\texttt{\bs{}HOLinline}] This macro, used to wrap standard \texttt{\holtm} arguments, puts text into typewriter font.
One possibility for its redefinition would be
\begin{verbatim}
   \renewcommand{\HOLinline}[1]{\ensuremath{#1}}
\end{verbatim}
Note that if the term being typeset causes the pretty-printer to break over multiple lines, \LaTeX{} will complain because of the appearance of \texttt{\bs\bs} commands.
If necessary, this can be avoided on a case-by-case basis by setting the \texttt{width} option to a larger than normal width.
\end{description}

When using math-mode munging, one also has to be aware of how larger pieces of text will appear.
In non-math-mode munging, material is usually put into \texttt{alltt} environments.
The recommended alternative for math-mode is to use the \texttt{\bs{}HOLmath} environment:
\begin{alltt}
   \textit{article text}

   \bs{}begin\lb{}HOLmath\rb
   \holthm\lb{}bool.AND_CLAUSES\rb
   \bs{}end\lb{}HOLmath\rb
\end{alltt}
This uses a standard \texttt{array} environment within a \texttt{displaymath}.

Occasionally, one will want to arrange blocks of \HOL{} material within a larger math context.
The \texttt{HOLarray} environment is a simple alias for a single-column left-aligned array that one can use in these situations.


\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.

Under Poly/ML, the \mkmunge{} executable also takes an optional \texttt{-b} option that can be used to specify a heap (see Section~\ref{sec:polyml-heaps}) to use as a base.
Doing so allows for the incorporation of many theories at once, and will be more efficient than loading the heap's theories separately on top of the default HOL heap.
The use of a base heap argument to \mkmunge{} doesn't affect the efficiency of the resulting munging tool.


\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 a number of 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).

By overriding the special token \texttt{\$Turnstile\$}, one can control the printing of the turnstile produced by \holthm{}.
The default setup is roughly equivalent to overriding \texttt{\$Turnstile\$} to \texttt{\textbackslash{}HOLTokenTurnstile\{\}} followed by a space, giving a total width of \texttt{3}.
Overriding the turnstile in this way will probably be necessary in math-mode printing, where the turnstile character is typically of the same width as 5 \texttt{\bs;} invocations.
Providing the correct width is important in order to get lines past the first to line up with the left edge of the mathematical text rather than the turnstile.

\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.

\paragraph{Setting Math-mode Spacing} If one expects to include all of the various \texttt{\bs{}HOL} commands in \LaTeX{} math contexts (as described above), then the \texttt{-m} option both sets the default width for math-mode spaces, and also
enables math-mode typesetting by default.

The specification of spacing is with a string of characters, as already described.
Note that if the command-line option includes any semi-colons or exclamation marks (\eg, \texttt{-mc;}), then they need to be quoted to prevent the shell from getting confused.
If the \texttt{-m} option appears without any additional characters, the default math-mode spacing will be \texttt{\bs;\bs;}.


\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 formatting 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
  formatting options for these new identifiers as well as the old ones.
  \HOL{} definition files can be used for defining and
  setting the formatting 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 formatting 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*}.
    For example, the id
    \texttt{arithmetic.LESS\_EQ*} represents all theorems 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 its \HOL{}\ definition.
    For theorems it is of the form \texttt{theory.theorem}.
  \item[\texttt{options}]
    formatting options for the munger as described in section~\ref{sec:munging-commands}.
    Please use the Holindex commands for typesetting 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 its 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 formatting 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{\texorpdfstring{Making \HOL{} theories \LaTeX{}-ready}{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