1\chapter{Miscellaneous Features} 2 3This section describes some of the features 4that exist for managing the interface 5% 6\index{HOL system@\HOL{} system!adjustment of user interface of} 7% 8to the \HOL{} system. 9 10\begin{itemize} 11\item The help system. 12\item The trace system for controlling feedback and printing. 13\item \holmake{}: a tool for dependency maintenance in large developments. 14\item Functions for counting the number of primitive inferences done in 15an evaluation, and timing it. 16\item A tool for embedding pretty-printed HOL theorems, terms and 17 types in \LaTeX{} documents. 18\end{itemize} 19 20\section{Help} 21 22 There are several kinds of help available in \HOL{}, all accessible 23 through the same incantation: 24 \begin{verbatim} 25 help <string>; 26 \end{verbatim} 27 28 The kinds of help available are: 29 30 \begin{description} 31 32 \item [Moscow~ML help.] \index{Moscow ML} (When using Moscow~ML~\HOL{}) 33 This is uniformly excellent. 34 Information for library routines is available, whether the library is loaded or not \emph{via} \texttt{help~"Lib"}. 35 36\item [\HOL{} overview.] This is a short summary of important information 37 about \HOL{}. 38 39\item [\HOL{} help.] This on-line help is intended to document all 40 HOL-specific functions available to the user. It is very detailed 41 and often accurate; however, it can be out-of-date, refer to earlier 42 versions of the system, or even be missing! 43 44\item [\HOL{} structure information.] For most structures in the 45 \HOL{} source, one can get a listing of the entrypoints found in the 46 accompanying signature. This is helpful for locating functions and 47 is automatically derived from the system sources, so it is alway 48 up-to-date. 49 50\item [Theory facts.] These are automatically derived from theory 51 files, so they are always up-to-date. The signature of each theory 52 is available (since theories are represented by structures in 53 \HOL{}). Also, each axiom, definition, and theorem in the theory can 54 be accessed by name in the help system; the theorem itself is given. 55\end{description} 56 57Therefore the following example queries can be made: 58 59\begin{table}[h] 60 \begin{center} 61 \begin{tabular}{|l|l|} \hline 62 \verb+help "installPP"+ & Moscow ML help \\ 63 \verb+help "hol"+ & \HOL{} overview \\ 64 \verb+help "aconv"+ & on-line \HOL{} help \\ 65 \verb+help "Tactic"+ & \HOL{} source structure information \\ 66 \verb+help "boolTheory"+ & theory structure signature \\ 67 \verb+help "list_Axiom"+ & theory structure signature and theorem 68 statement \\ \hline 69 \end{tabular} 70 \end{center} 71\end{table} 72 73\section{The Trace System} 74\index{traces, controlling HOL feedback@traces, controlling \HOL{} feedback} 75\label{sec:traces} 76 77The 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. 78These flags are typically those that determine the level to which \HOL{} tools provide information to the user while operating. 79For example, a trace level of zero will usually make a tool remain completely 80silent while it operates. 81The tool may still raise an exception when it fails, but it won't also 82output any messages saying so. 83 84There are three core functions, all in the \ml{Feedback} structure: 85\begin{hol} 86\begin{verbatim} 87 traces : unit -> 88 {default: int, max: int, name: string, trace_level: int} list 89 90 set_trace : string -> int -> unit 91 trace : (string * int) -> ('a -> 'b) -> ('a -> 'b) 92\end{verbatim} 93\end{hol} 94 95The \ml{traces} function returns a list of all the traces in the system. 96The \ml{set\_trace} function allows the user to set a trace directly. 97The effect of this might be seen in a subsequent call to \ml{traces()}. 98Finally, 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). 99 100 101 102\section{\texorpdfstring{Maintaining \HOL{} Formalizations with \holmake}{Maintaining HOL Formalizations with \holmake}} 103\label{Holmake} 104\index{Holmake@\holmake|(} 105 106The purpose of \holmake{} is to maintain dependencies in a \HOL{} 107source directory. A single invocation of \holmake{} will compute 108dependencies between files, (re)compile plain ML code, (re)compile and 109execute theory scripts, and (re)compile the resulting theory modules. 110\holmake{} does not require the user to provide any explicit 111dependency information themselves. \holmake{} can be very convenient 112to use, but there are some conventions and restrictions on it that 113must be followed, described below. 114 115 116 117 118\holmake{} can be accessed through 119\begin{verbatim} 120 <hol-dir>/bin/Holmake. 121\end{verbatim} 122 123The development model that \holmake{} is designed to support is that 124there are two modes of work: theory construction and system revision. 125In `theory construction' mode, the user builds up a theory by 126interacting with HOL, perhaps over many sessions. In `system rebuild' 127mode, a component that others depend on has been altered, so all modules 128dependent on it have to be brought up to date. System rebuild mode is 129simpler so we deal with it first. 130 131\subsection{System rebuild} 132 133A system rebuild happens when an existing theory has been improved in 134some way (augmented with a new theorem, a change to a definition, 135etc.), or perhaps some support ML code has been modified or added to 136the formalization under development. The user needs to find and 137recompile just those modules affected by the change. This is what an 138invocation of \holmake{} does, by identifying the out-of-date modules 139and re-compiling and re-executing them. 140 141 142\subsection{Theory construction} 143 144To start a theory construction, some context (semantic, and also proof 145support) is established, typically by loading parent theories and 146useful libraries. In the course of building the theory, the user keeps 147track of the ML---which, for example, establishes context, makes 148definitions, builds and invokes tactics, and saves theorems---in a 149text file. This file is used to achieve inter-session persistence of 150the theory being constructed. For example, the text file resulting 151from session $n$ is ``\verb+use+''-d to start session $n+1$; after 152that, theory construction resumes. 153 154Once the user finishes the perhaps long and arduous task of constructing 155a theory, the user should 156\begin{enumerate} 157\item make the script separately compilable; 158\item invoke \holmake{}. This will (a) compile and execute the 159 script file; and (b) compile the resulting theory file. After this, 160 the theory file is available for use. 161\end{enumerate} 162 163\subsection{Source conventions for script and SML files} 164 165\paragraph{Script and theory files} 166The file that generates the \HOL{} theory \textit{my}\texttt{Theory} must be called \textit{my}\texttt{Script.sml}. 167After the theory has been successfully generated, it can be \texttt{open}-ed at the head of other developments: 168\begin{alltt} 169 open myTheory 170\end{alltt} 171\index{load (ML function)@\ml{load} (\ML{} function)} 172and it can be loaded interactively: 173\begin{alltt} 174 load "myTheory"; 175\end{alltt} 176The file \texttt{myScript.sml} should begin with the standard boilerplate: 177\begin{alltt} 178 open HolKernel Parse boolLib bossLib 179 180 val _ = new_theory "my" 181\end{alltt} 182This ``boilerplate'' ensures that the standard tactics and SML commands will be in the namespace when the script file is compiled. 183Interactively, 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. 184In addition, if \texttt{myTheory} depends on other \HOL{} theories, this ancestry should also be recorded in the script file. 185The easiest way to achieve this is simply to \texttt{open} the relevant theories. 186Conventionally, the \texttt{open} declarations for such theories appear just before the call to \texttt{new_theory}. 187For example: 188\begin{alltt} 189 open HolKernel Parse boolLib bossLib 190 191 open myfirstAncestorTheory OtherAncestorTheory 192 193 val _ = new_theory "my" 194\end{alltt} 195\index{load (ML function)@\ml{load} (\ML{} function)} 196Interactively, these may well be the names of theories that have been explicitly loaded into the context with the \texttt{load} function. 197In the interactive system, one has to explicitly \ml{load} modules; on the other hand, the batch compiler will load modules automatically. 198For 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"}. 199(This is on the assumption that structure \ml{Foo} is defined in a file \texttt{Foo.sml}.) 200Contrarily, the batch compiler will reject files having occurrences of \ml{load}, since \ml{load} is only defined for the interactive system. 201 202In addition, simply referring to a theory's theorems using the `dot-notation' will make that theory an ancestor. 203For example, 204\begin{alltt} 205 val mytheorem = store_thm( 206 "mytheorem", 207 ``...``, 208 SIMP_TAC (srw_ss()) [ThirdAncestorTheory.important_lemma] ...); 209\end{alltt} 210will record a dependency on \texttt{ThirdAncestoryTheory}, making it just as much an ancestor as the theories that have been explicitly \texttt{open}-ed elsewhere. 211 212Finally, all script files should also end with the invocation: 213\begin{verbatim} 214 val _ = export_theory() 215\end{verbatim} 216When the script is finally executed, this call writes the theory to disk. 217 218The calls to \texttt{new_theory} and \texttt{export_theory} must bracket a sequence of SML declarations. 219A 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. 220Declarations are \emph{not} expressions. 221This means that script files should \emph{not} include bare calls to \HOL{} functions like \texttt{Datatype}. 222Instead, declarations such as the following need to be used: 223\begin{alltt} 224 val _ = Datatype`tree = Lf | Nd num tree tree` 225\end{alltt} 226This 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. 227Indeed, one is allowed to (and generally should) omit the bracketing 228\begin{alltt} 229 structure myScript = struct 230 ... 231 end 232\end{alltt} 233lines, but the contents of the file are still interpreted as if belonging to a structure. 234 235Finally, take care not to have the string ``\texttt{Theory}'' appear at the end of the name of any of your files. 236\HOL{} generates files containing this string, and when it cleans up after itself, it removes such files using a regular expression. 237This will also remove other files with names containing ``\texttt{Theory.sml}'' or ``\texttt{Theory.sig}''. 238For 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. 239 240\paragraph{Other SML code} 241When developing \HOL{} libraries, one should again attempt to follow Moscow~ML's conventions. 242Most importantly, file names should match \texttt{signature} and \texttt{structure} names. 243If this can be done, the automatic dependency analysis done by \holmake{} will work ``out of the box''. 244A signature for module \texttt{foo} should always appear in file \texttt{foo.sig}, and should have the form 245\begin{alltt} 246 signature foo = 247 sig 248 ... 249 end 250\end{alltt} 251The accompanying implementation of \texttt{foo} should appear in file \texttt{foo.sml}, and should have the form 252\begin{alltt} 253 structure foo :> foo = 254 struct 255 ... 256 end 257\end{alltt} 258As with theory files, the contents of a \texttt{structure} must be a sequence of declarations only. 259Neither sort of file should have any other declarations within it (before or after the \texttt{signature} or \texttt{structure}). 260 261Deviations from this general pattern are possible, but life is much simpler if such deviations can be avoided. 262The \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. 263Ignoring the guidelines will generally result in the need for quite involved \texttt{Holmakefile}s (see Section~\ref{sec:using-Holmakefiles} below). 264 265\subsection{Summary} 266 267A complete theory construction might be performed by the following steps: 268\begin{itemize} 269\item Construct theory script, perhaps over many sessions; 270\item Transform script into separately compilable form; 271\item Invoke \holmake{} to generate the theory and compile it. 272\end{itemize} 273After that, the theory is usable as an ML module. 274This flow is demonstrated in the Euclid example of \TUTORIAL. 275 276Alternatively, 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. 277 278\subsection{What \holmake{} doesn't do} 279 280\holmake{} only works properly on the current directory. 281\holmake{} will rebuild files in the current directory if something it depends on from another directory is fresher than it is, but it will not do any analysis on files in other directories. 282 283\index{Holmake@\holmake!recursive invocation}% 284However, one can indicate that there is a dependency on other directories by using the \texttt{-I} flag, or the \texttt{INCLUDES} variable in a \texttt{Holmakefile}. 285Such a specification will cause \holmake{} to look in the specified directories for other theory files that the current directory may depend on. 286Moreover, by default \holmake{} will recursively call itself on all those ``include'' directories before doing anything in the current directory. 287In this way, one can get a staged application of \holmake{} across multiple directories.\footnote{See \emph{Recursive Make Considered 288 Harmful} by Peter Miller for why this is not ideal.} 289 290\subsection{\holmake{}'s command-line arguments} 291\index{Holmake@\holmake!command-line arguments} 292Like {\tt make}, \holmake{} takes command-line arguments corresponding to the targets that the user desires to build. 293If there are no command-line targets, then \holmake{} will look for a \texttt{Holmakefile} in the current directory. 294If 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. 295If there is a target in the \texttt{Holmakefile}, then \holmake{} will try to build the first such target (only). 296 297In addition, there are three special targets that can be used: 298\begin{description} 299\item[{\tt clean}] Removes all compiled files (unless over-ridden by a 300 make-file target of the same name, see 301 section~\ref{sec:using-Holmakefiles} below). 302\item [{\tt cleanDeps}] Removes all of the pre-computed dependency 303 files. This can be an important thing to do if, for example, you 304 have introduced a new {\tt .sig} file on top of an existing {\tt 305 .sml} file. 306\item [{\tt cleanAll}] Removes all compiled files as well as all of 307 the hidden dependency information. 308\end{description} 309 310\noindent Finally, users can directly affect the workings of \holmake{} 311with the following command-line options: 312\begin{description} 313\item[\tt -d <file>] Ignore the given file and don't try to build it. 314 The file may be rebuilt anyway if other files you have specified 315 depend on it. This is useful to stop Holmake from attempting to 316 compile files that are interactive scripts (include use of {\tt 317 load} or {\tt use}, for example). 318\item[\texttt{-f <theory>}] Toggles whether or not a theory should be 319 built in ``fast'' mode. Fast building causes tactic proofs 320 (invocations of \texttt{prove} and \texttt{store\_thm}) to 321 automatically succeed. This lack of soundness is marked by the 322 \texttt{fast\_proof} oracle tag. This tag will appear on all 323 theorems proved in this way and all subsequent theorems that depend 324 on such theorems. \holmake's default is not to build in fast mode. 325\item[\texttt{--fast}] Makes \holmake's default be to build in fast 326 mode (see above). 327\item[{\tt --help} or {\tt -h}] Prints out a useful option summary and 328 exits. 329\item[\tt --holdir <directory>] Associate this build with the given 330 HOL directory, rather than the one this version of \holmake{} was 331 configured to use by default. 332\item[\tt --holmakefile <file>] Use the given file as a make-file. 333 See section~\ref{sec:using-Holmakefiles} below for more on this. 334\item[\tt -I <directory>] 335 Look in specified directory for additional object files, including other HOL theories. 336 This option can be repeated, with multiple {\tt -I}'s to allow for multiple directories to be referenced. 337 As above, directories specified in this way will also be rebuilt before the current targets are built. 338\item[\texttt{--interactive} or \texttt{-i}] Causes the HOL code that 339 runs when a theory building file is executed to have the flag 340 \texttt{Globals.interactive} set to true. This will alter the diagnostic 341 output of a number of functions within the system. 342\item[\texttt{-k} or \texttt{--keep-going}] Causes \holmake{} to try 343 to build all specified targets, rather than stopping as soon as one 344 fails to build. 345\item[\texttt{--logging}] Causes \holmake{} to record the times taken 346 to build any theory files it encounters. The times are logged in a 347 file in the current directory. The name of this file includes the 348 time when \holmake{} completed, and when on a Unix system, the name 349 of the machine where the job was run. If \holmake{} exits 350 unsuccessfully, the filename is preceded by the string 351 ``\texttt{bad-}''. Each line in the log-file is of the form 352 \textit{theory-name time-taken}, with the time recorded in seconds. 353\item[\texttt{--no\_holmakefile}] Do not use a make-file, even if a file 354 called \texttt{Holmakefile} is present in the current directory. 355\item[\texttt{--no\_overlay}] Do not use an overlay file. All HOL 356 builds require the presence of a special overlay file from the 357 kernel when compiling scripts and libraries. This is not 358 appropriate for compiling code that has no connection to HOL, so 359 this option makes the compilation not use the overlay file. This 360 option is also used in building the kernel before the overlay itself 361 has been compiled. 362\item[\texttt{--no\_prereqs}]% 363\index{Holmake@\holmake!recursive invocation}% 364Do not recursively attempt to build ``include'' directories before working in the current directory. 365\item[\texttt{--no\_sigobj}] 366 Do not link against \HOL{} system's directory of \HOL{} system files. 367 Use of this option goes some way towards turning \holmake{} into a general \ML{} \textsf{make} system. 368 However, it will still attempt to do ``\HOL{} things'' with files whose names end in \texttt{Script} and \texttt{Theory}. 369 This option implies \texttt{--no\_overlay}. 370\item[\texttt{--overlay <file>}] Use the given file as the overlay 371 rather than the default. 372\item[\texttt{--qof},\texttt{--noqof}] 373 Where q-o-f stands for ``quit on failure''. 374 By default, if a tactic fails to prove a theorem, the running script exits with a failure. 375 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). 376 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. 377\item[\texttt{--quiet}] Minimise the amount of output produced by 378 \holmake{}. Fatal error messages will still be written to the 379 standard error stream. Note that other programs called by \holmake{} will not 380 be affected. 381\item[\texttt{-r}]% 382\index{Holmake@\holmake!recursive invocation}% 383Forces \holmake{} to behave recursively, overriding the \texttt{--no\_prereqs} option, and also causing \holmake{} to clean recursively in the ``includes'' directories (which is not done otherwise). 384\item[{\tt --rebuild\_deps}] Forces \holmake{} to always 385 rebuild the dependency information for files it examines, whether or 386 not it thinks it needs to. This option is implemented by having 387 \holmake{} wipe all of its dependency cache (as per the 388 \texttt{cleanDeps} option above) before proceeding with the build. 389\end{description} 390 391\noindent \holmake{} should never exit with error messages such as ``Uncaught 392exception''. Such behaviour is a bug, please report it! 393 394 395\subsection{Using a make-file with \holmake} 396\label{sec:using-Holmakefiles} 397 398\holmake{} will use a make-file to augment its behaviour if one is 399present in the current directory. By default it will look for a file 400called \texttt{Holmakefile}, but it can be made to look at any file at 401all with the \texttt{--holmakefile} command-line option. The 402combination of \holmake{} and a make-file is supposed to behave as 403much as possible like a standard implementation of \textsf{make}. 404 405A make-file consists of two types of entries, variable definitions and 406rules. Outside of these entries, white-space is insignificant, but 407newline and \texttt{TAB} characters are very significant within them. 408Comments can be started with hash (\texttt{\#}) characters and last 409until the end of the line. Quoting is generally done with use of the 410back-slash (\verb+\+) character. In particular, a backslash-newline 411pair always allows a line to be continued as if the newline wasn't 412present at all. 413 414A variable definition is of the form 415\[ 416\textsl{Ident} \texttt{ = } \textsl{text} \texttt{ <NEWLINE> } 417\] 418and a rule is of the form 419\[ 420\textsl{text } \texttt{:} \textsl{ text} \texttt{ <NEWLINE>} 421(\texttt{<TAB>}\textsl{text}\texttt{ <NEWLINE>})^* 422\] 423Henceforth, the text following a \texttt{TAB} character in a rule will 424be referred to as the \emph{command text}. Text elsewhere will be 425referred to as \emph{normal text}. Normal text has comments stripped 426from it, so hash characters there must be escaped with a back-slash 427character. An \textsl{Ident} is any non-empty sequence of 428alpha-numeric characters, including the underscore (\texttt{\_}). 429 430In some contexts, normal text is interpreted as a list of words. 431These lists use white-space as element separators. If a word needs to 432include white-space itself, those white-space characters should be 433escaped with back-slashes. 434 435\newcommand{\varref}[1]{\texttt{\$(#1)}} 436\paragraph{Variable definitions} The text on the RHS of a variable 437definition can be substituted into any other context by using a 438\emph{variable reference}, of the form \varref{VARNAME}. References 439are evaluated \emph{late}, not at time of definition, so it is quite 440permissible to have forward references. On the other hand, this makes 441it impossible to write things like \[ \texttt{VAR = \varref{VAR} 442something\_new} 443\] because the evaluation of \varref{VAR} would lead to an infinite 444loop. GNU \textsf{make}'s facility for immediate 445definition of variables with \texttt{:=} is not supported. 446 447Note also that white-space around the equals-sign in a variable 448definition is stripped. This means that 449\[ 450\texttt{VAR =<whitespace><NEWLINE>} 451\] gives \texttt{VAR} the empty string as its value.\footnote{It is 452 possible to give a variable a value of pure whitespace by writing \[ 453\begin{array}{l} 454\texttt{NOTHING =}\\ 455\texttt{ONE\_SPACE = \varref{NOTHING}\textvisiblespace\hspace{1mm}\varref{NOTHING}}\\ 456\end{array}\]} 457 458Finally, note that the text inside a variable reference is itself 459evaluated. This means that one can write something like 460\varref{FOO\_\varref{OS}} and have this first expand the \texttt{OS} 461variable, presumably giving rise to some useful string (such as 462\texttt{unix}), and then have the resulting variable 463(\texttt{FOO\_unix}, say) expanded. This effectively allows the 464construction of functions by cases (define variables 465\texttt{FOO\_unix}, \texttt{FOO\_macos} etc.; then use the nested 466variable reference above). If the internal variable expands to 467something containing spaces, this will not turn a normal variable 468reference into a function call (see below). On the other hand, 469if the initial reference contains a space, the function name component 470\emph{will} be expanded, allowing implementation of a function by 471cases determining which text-manipulation function should be called. 472 473\paragraph{Rules} 474Make-file rules are interpreted in the same way as by traditional 475\textsf{make}. The files specified after the colon (if any) are those 476files that each target (the files before the colon) is said to 477``depend'' on. If any of these are newer than a target, then 478\holmake{} rebuilds that target according to the commands. If there 479are no dependencies, then the commands are executed iff the 480target doesn't exist. If there are no commands, and the target is not 481of a type that \holmake{} already knows how to build, then it will 482just make sure that the dependencies are up to date (this may or 483may not create the target). If there are no commands attached to a 484rule, and the target is one that \holmake{} does know how to build, 485then the rule's extra dependencies are added to those that \holmake{} 486has managed to infer for itself, and \holmake{} will build the target 487using its built-in rule. If commands are provided for a type of file 488that \holmake{} knows how to build itself, then the make-file's 489commands and dependencies take precedence, and only they will be 490executed. 491 492In addition, it is possible to indicate that the built-in process of generating theory files from script files generates side products. 493This is done by writing a command-less rule of the form 494\begin{alltt} 495 target : *thyScript.sml 496\end{alltt} 497where an asterisk character precedes the name of the script file. 498This 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}. 499If \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. 500 501If a command-line is preceded by a hyphen (\verb!-!) character, then 502the rest of the line is executed, but its error-code is ignored. 503(Normally, a command-line raising an error will cause \holmake{} to 504conclude that the target can not be built.) If a command-line is 505preceded by an at-sign (\verb!@!), then that command-line will not be 506echoed to the screen when it is run. These two options can be 507combined in either order at the start of a command-line. 508 509Command text is interpreted only minimally by \holmake. On Unix, 510back-slashes are not interpreted at all. On Windows, back-slashes 511followed by newlines are turned into spaces. Otherwise, command text 512is passed as is to the underlying command interpreter 513(\texttt{/bin/sh} say, on Unix, or \texttt{COMMAND.COM} on Windows). 514In particular, this means that hash-characters do \emph{not} start 515comments on command-lines, and such ``comments'' will be passed to the 516shell, which may or may not treat them as comments when it sees them. 517 518\paragraph{Special targets} 519Some target names for rules are handled specially by \holmake{}: 520\begin{itemize} 521\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. 522For example, targets naming conceptual collections of files such as \texttt{all} should be marked as ``phony''. 523If a target is phony, then its dependencies will be built even if a file of that name exists and is newer than the dependencies. 524\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. 525In order to extend cleaning behaviour, use the \texttt{EXTRA\_CLEANS} variable (see below). 526\end{itemize} 527\paragraph{Functions} 528\index{Holmake@\holmake!functions for text-manipulation} 529\holmake{} supports some simple functions for manipulating text. All 530functions are written with the general form 531\texttt{\$(\textsl{function-name}\textvisiblespace{}\hspace{1mm}\textsl{arg}${}_1$,\textsl{arg}${}_2$\dots,\textsl{arg}${}_n$)}. 532Arguments can not include commas (use variable references to variables 533whose value are commas instead), but can otherwise be arbitrary text. 534\begin{description} 535\item[\texttt{\$(dprot arg)}] quotes (or ``protects'') the space 536 characters that occur in a string so that the string will be treated 537 as a unit if it occurs in a rule's dependency list. For example, 538 the file 539\begin{verbatim} 540 dep = foo bar 541 target: $(dep) 542 do_something 543\end{verbatim} 544 will see \texttt{target} as having two dependencies, not one, 545 because spaces are used to delimit dependencies. If a dependency's 546 name includes spaces, then this function can be used to quote them 547 for \holmake's benefit. Note that the \texttt{dprot} function 548 does \emph{not} do the same thing as \texttt{protect} on either Unix 549 or Windows systems. 550\item[\texttt{\$(findstring arg1,arg2)}] checks if \texttt{arg1} occurs 551 in (is a sub-string of) \texttt{arg2}. If it does so occur, the 552 result is \texttt{arg1}, otherwise the result is the empty string. 553\item[\texttt{\$(if arg1,arg2,arg3)}] examines \texttt{arg1}. If it 554 is the empty string, then the value of the whole is equal to the 555 value of \texttt{arg3}. Otherwise, the value is that of \texttt{arg2}. 556\item[\texttt{\$(patsubst arg1,arg2,text)}] splits \texttt{text} into component 557 words, and then transforms each word by attempting to see if it 558 matches the pattern in \texttt{arg1}. If so, it replaces that word 559 with \texttt{arg2} (suitably instantiated). If not, the word is 560 left alone. The modified words are then reassembled into a 561 white-space separated list and returned as the value. 562 563 A pattern is any piece of text including no more than one occurrence 564 of the percent~(\texttt{\%}) character. The percent character 565 matches any non-empty string. All other characters must be matched 566 literally. The instantiation for \texttt{\%} is remembered when the 567 replacement is constructed. Thus, \[ 568 \texttt{\$(patsubst \%.sml,\%.uo,\$(SMLFILES))} 569 \] turns a list of files with suffixes \texttt{.sml} into the same 570 list with the suffixes replaced with \texttt{.uo}. 571\item[\texttt{\$(protect arg)}] wraps \texttt{arg} in appropriate 572 quote characters to ensure that it will pass through the operating 573 system's command shell unscathed. This is important in the presence 574 of file-names that include spaces or other shell-significant 575 characters like less-than and greater-than. Those make-file 576 variables that point directly at executables (\texttt{MOSMLC}, 577 \texttt{MOSMLLEX} etc.) are automatically protected in this way. 578 Others, which might be used in concatenation with other elements, 579 are not so protected. Thus, if \texttt{DIR} might include spaces, 580 one should write 581\begin{verbatim} 582 $(protect $(DIR)/subdirectory/program) 583\end{verbatim} 584 so that the above will be read as one unit by the underlying shell. 585\item[\texttt{\$(subst arg1,arg2,text)}] replaces every occurrence 586 of \texttt{arg1} in \texttt{text} with \texttt{arg2}. 587\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. 588For example \texttt{\$(which cat)} will usually expand to \texttt{/bin/cat} on Unix-like systems. 589If there is no occurrence of \texttt{arg} in any directory in \texttt{PATH}, this function call expands to the empty string. 590\item[\texttt{\$(wildcard pattern)}] expands the shell ``glob'' pattern (\eg, \texttt{*Script.sml}) into the list of matching filenames. 591If the pattern doesn't match any files, then the function returns \texttt{pattern} unchanged. 592\end{description} 593 594\paragraph{Special and pre-defined variables} 595 596\index{Holmake@\holmake!variables in makefiles} 597If defined, the \texttt{INCLUDES} variable is used to add directories to the list of directories consulted when files are compiled and linked. 598The effect is as if the directories specified had all been included on the command-line with \texttt{-I} options. 599The \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. 600This 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. 601 602\index{Holmake@\holmake!recursive invocation} 603By 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. 604If the \texttt{-r} (``force recursion'') command-line flag is used, these directories are also ``clean''-ed when a cleaning target is given to \holmake{}. 605 606\index{CLINE_OPTIONS (Holmakefile variable)@\texttt{CLINE\_OPTIONS} (Holmakefile variable)}% 607The \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. 608The 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. 609For example, a useful \texttt{CLINE\_OPTIONS} line% 610\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. 611In addition, the \texttt{-{}-no\_hmakefile} command-line option will stop the makefile from being consulted at all.} % 612might be 613\begin{alltt} 614 CLINE_OPTIONS = -j1 --noqof 615\end{alltt} 616Under 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. 617 618\index{EXTRA_CLEANS (Holmakefile variable)@\texttt{EXTRA\_CLEANS} (Holmakefile variable)}% 619The \texttt{EXTRA\_CLEANS} variable is used to 620specify the name of additional files that should be deleted when a 621\texttt{Holmake clean} command is issued. 622 623Within a command, the variable \texttt{\$<} is used to stand for the 624name of the first dependency of the rule. The variable \texttt{\$@} is 625used to stand for the target of the rule. 626 627Finally there are variables that expand to program names and other 628useful information: 629\begin{description} 630\item[\texttt{CP}] This variable is replaced by an operating-system 631 appropriate program to perform a file copy. The file to be copied 632 is the first argument, the second is the place to copy to. The 633 second argument can be a directory. (Under Unix, \texttt{CP} 634 expands to \texttt{/bin/cp}; under Windows, it expands to 635 \texttt{copy}.) 636\item[\texttt{DEBUG\_FLAG}] This variable is replaced by \texttt{"-{}-dbg"} if that flag was passed to \holmake, or the empty string if not. 637\item[\texttt{HOLDIR}] The root of the HOL installation. 638\item[\texttt{HOLHEAP}] 639Under 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). 640See Section~\ref{sec:polyml-heaps} below for more on using custom heaps with Poly/ML. 641\item[\texttt{HOLMOSMLC}] This variable is replaced by an invocation 642 of the Moscow ML compiler along with the \texttt{-q} flag (necessary 643 for handling quotations), and the usual \texttt{-I} include 644 specifications (pre-includes, the hol-directory include, and the 645 normal includes). 646\item[\texttt{HOLMOSMLC-C}] This variable is the same as 647 \texttt{HOLMOSMLC} except that it finishes with a closing 648 \texttt{-c} option (hence the name) followed by the name of the 649 system's overlay file. This is needed for compilation of HOL source 650 files, but not for linking of HOL object code, which can be done 651 with \texttt{HOLMOSMLC}. 652\item[\texttt{KERNELID}] 653 The kernel option that was passed to \HOL's \texttt{build} command, stripped of its leading hyphens. 654 This will typically be \texttt{stdknl} (the standard kernel) but may take on other values if other custom kernels are being used. 655\item[\texttt{ML\_SYSNAME}] The name of the ML system being used: 656 either \texttt{mosml} or \texttt{poly}. 657\item[\texttt{MLLEX}] This is the path of the \texttt{mllex} tool that 658 is built as part of HOL's configuration. 659\item[\texttt{MLYACC}] This is the path of the \texttt{mlyacc} tool that 660 is built as part of HOL's configuration. 661\item[\texttt{MOSMLC}] This is replaced by an invocation of the 662 compiler along with just the normal includes. 663\item[\texttt{MOSMLLEX}] This is replaced by an invocation of the 664 \texttt{mosmllex} program that comes with the Moscow ML 665 distribution. 666\item[\texttt{MOSMLYAC}] This is replaced by an invocation of the 667 \texttt{mosmlyac} program that comes with the Moscow ML 668 distribution. 669\item[\texttt{MV}] This variable is replaced by an operating-system 670 appropriate program to perform a file movement. The file to be 671 moved is the first argument, the second is the place to move to. 672 The second argument can be a directory. (Under Unix, \texttt{MV} 673 expands to \texttt{mv}; under Windows, it expands to \texttt{rename}.) 674\item[\texttt{OS}] This variable is replaced by the name of the 675 current operating system, which will be one of the strings 676 \texttt{"linux"}, \texttt{"solaris"}, \texttt{"macosx"}, 677 \texttt{"unix"} (for all other Unices), or \texttt{"winNT"}, for all 678 Microsoft Windows operating systems (those of the 21st century, 679 anyway). 680\item[\texttt{SIGOBJ}] Effectively \varref{HOLDIR}\texttt{/sigobj}, 681 where HOL object code is stored. 682 \item[\texttt{UNQUOTE}] The location of the quotation-filter executable. 683\end{description} 684The \texttt{MOSMLLEX} and \texttt{MOSMLYAC} abbreviations are really 685only useful if the originals aren't necessarily going to be on the 686user's ``path''. For backwards compatibility, the five variables 687above including the sub-string ``\texttt{MOSML}'' in their names can 688also be used by simply writing their names directly (i.e., without the 689enclosing \varref{\dots}), as long as these references occur first on 690a command-line. 691 692Under Poly/ML, commands involving the variable \texttt{MOSMLC} are interpreted ``appropriately''. 693If 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. 694We strongly discourage the use of \texttt{MOSMLYAC} and \texttt{MOSMLLEX}, even when running HOL under Moscow~ML. 695 696If a reference is made to an otherwise undefined string, then it is 697treated as a reference to an environment variable. If there is no 698such variable in the environment, then the variable is silently given 699the empty string as its value. 700 701\paragraph{Conditional parts of makefiles} 702\index{Holmake@\holmake!conditional inclusion of sections} 703As 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. 704% 705This is similar to the way directives such as \texttt{\#ifdef} can be used to control the C~preprocessor. 706 707There are four possible directives in a \texttt{Holmakefile}: \texttt{ifdef}, \texttt{ifndef}, \texttt{ifeq} and \texttt{ifneq}. 708% 709The versions including the extra `n' character reverse the boolean sense of the test. 710% 711Conditional directives can be chained together with \texttt{else} directives, and must be terminated by the \texttt{endif} command. 712% 713The 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. 714\begin{hol} 715\begin{verbatim} 716ifdef POLY 717TARGETS = target1 target2 718 719target1: dependency1 720 build_command -o target1 dependency1 721endif 722\end{verbatim} 723\end{hol} 724The next example includes chained \texttt{else} commands: 725\begin{hol} 726\begin{verbatim} 727ifeq "$(HOLDIR)" "foo" 728VAR = X 729else ifneq "$(HOLDIR)" "bar" 730VAR = Y 731else 732VAR = Z 733endif 734\end{verbatim} 735\end{hol} 736\index{ifeq (Holmake directive)@\texttt{ifeq} (Holmake directive)} 737\index{ifneq (Holmake directive)@\texttt{ifneq} (Holmake directive)} 738The \texttt{ifneq} and \texttt{ifeq} forms test for string equality. 739% 740They can be passed their arguments as in the example, or delimited with apostrophes, or in parentheses with no delimiters, as in: 741\begin{hol} 742\begin{verbatim} 743ifeq ($(HOLDIR),$(OTHERDIR)) 744VAR = value 745endif 746\end{verbatim} 747\end{hol} 748 749\index{ifdef (Holmake directive)@\texttt{ifdef} (Holmake directive)} 750\index{ifndef (Holmake directive)@\texttt{ifndef} (Holmake directive)} 751The definedness tests \texttt{ifdef} and \texttt{ifndef} test if a name has a non-null expansion in the current environment. 752% 753This test is just of one level of expansion. 754% 755In the following example, \texttt{VAR} is defined even though it ultimately expands to the emptry string, but \texttt{NULL} is not. 756% 757The variable \texttt{FOOBAR} is also not defined. 758\begin{hol} 759\begin{verbatim} 760NULL = 761VAR = $(NULL) 762\end{verbatim} 763\end{hol} 764Note that environment variables with non-empty values are also considered to be defined. 765 766\index{Holmake@\holmake|)} 767 768 769\section{\texorpdfstring{Generating and Using Heaps in Poly/ML \HOL{}}{Generating and Using Heaps in Poly/ML HOL}} 770\label{sec:polyml-heaps} 771 772\index{heaps (in Poly/ML)|(} 773\index{Poly/ML} 774\index{Moscow ML} 775Poly/ML has a nice facility whereby the state of one of its interactive sessions can be stored on disk and then reloaded. 776This allows for an efficient resumption of work in a known state. 777The \HOL{} implementation uses this facility to implement the \texttt{hol} executable. 778In Poly/ML, \texttt{hol} starts immediately. 779In 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}). 780 781Users can use the same basic technology to ``dump'' heaps of their own. 782Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories. 783This can make developing big mechanisations considerably more pleasant. 784 785\subsection{\texorpdfstring{Generating \HOL{} heaps}{Generating HOL heaps}} 786 787The 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. 788This 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}). 789Thus the command-line 790\begin{alltt} 791 buildheap -o realheap transcTheory polyTheory 792\end{alltt} 793would 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. 794 795A reasonable way to manage the generation of heaps is to use a \texttt{Holmakefile}. 796For example, the \texttt{realheap} above might be generated with the source in Figure~\ref{fig:realheap-makefile}. 797The use of the special variable \texttt{HOLHEAP} has a number of nice side effects. 798First, it makes the given file a dependency of all other products in the current directory. 799This means that the \HOL{} heap will be built first. 800Secondly, the other products in the current directory will be built on top of that heap, not the default heap behind \texttt{hol}. 801\begin{figure} 802\begin{alltt} 803 ifdef POLY 804 HOLHEAP = realheap 805 OBJNAMES = polyTheory transcTheory 806 DEPS = $(patsubst %,$(dprot $(SIGOBJ)/%),$(OBJNAMES)) 807 808 $(HOLHEAP): $(DEPS) 809 $(protect $(HOLDIR)/bin/buildheap) -o $@ $(OBJNAMES) 810 endif 811\end{alltt} 812\caption{A \texttt{Holmakefile} fragment for building a custom \HOL{} heap embodying the standard real number theories. 813If 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. 814For 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. 815Finally, 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.} 816\label{fig:realheap-makefile} 817\end{figure} 818 819\subsection{\texorpdfstring{Using \HOL{} heaps}{Using HOL heaps}} 820As 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. 821This 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}). 822In 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. 823Again, 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. 824 825It is obviously important to be able to use heaps interactively. 826If 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. 827The fact that this is happening is mentioned as the interactive session begins. 828For example: 829 830\begin{samepage} 831\begin{alltt} 832--------------------------------------------------------------------- 833 HOL-4 [Kananaskis 8 (stdknl, built Tue Jul 24 16:48:44 2012)] 834 835 For introductory HOL help, type: help "hol"; 836--------------------------------------------------------------------- 837 838[extending loadPath with Holmakefile INCLUDES variable] 839[In non-standard heap: computability-heap] 840Poly/ML 5.4.1 Release 841> 842\end{alltt} 843\end{samepage} 844 845Finally, 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. 846Thus, 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}. 847Subsequently, developments in other directories could use this heap by specifying\[ 848 \texttt{\$(HOLDIR)/src/real/realheap} 849\] 850as the value for their \texttt{HOLHEAP} variables. 851 852\index{heaps (in Poly/ML)|)} 853\section{Timing and Counting Theorems} 854 855\index{counting inferences, in HOL proofs@counting inferences, in \HOL{} proofs|(} 856\index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|(} 857\index{timing of HOL evaluations@timing of \HOL{} evaluations|(} 858 859 860\HOL{} can be made to record its use of primitive 861inferences, axioms, definitions and use of oracles. Such recording is 862enabled with the function 863 864\begin{holboxed} 865\index{counting_thms@\ml{counting\_thms}|pin} 866\begin{verbatim} 867 val counting_thms : bool -> unit 868\end{verbatim} 869\end{holboxed} 870 871\noindent (This function as with all the others in this section is 872found in the \texttt{Count} structure.) 873 874Calling \ml{counting\_thms true} enables counting, and 875\ml{counting\_thms false} disables it. The default is for counting to 876be disabled. If it is enabled, whenever \HOL{} performs a primitive 877inference (or accepts an axiom or definition) a counter is 878incremented. A total count as well as counts per primitive inference 879are maintained. The value of this counter is returned by the 880function: 881 882\begin{holboxed} 883\index{thm_count@\ml{thm\_count}|pin} 884\begin{verbatim} 885 val thm_count : unit -> 886 {ASSUME : int, REFL : int, BETA_CONV : int, SUBST : int, 887 ABS : int, DISCH : int, MP : int, INST_TYPE : int, MK_COMB : int, 888 AP_TERM : int, AP_THM : int, ALPHA : int, ETA_CONV : int, 889 SYM : int, TRANS : int, EQ_MP : int, EQ_IMP_RULE : int, 890 INST : int, SPEC : int, GEN : int, EXISTS : int, CHOOSE : int, 891 CONJ : int, CONJUNCT1 : int, CONJUNCT2 : int, DISJ1 : int, 892 DISJ2 : int, DISJ_CASES : int, NOT_INTRO : int, NOT_ELIM : int, 893 CCONTR : int, GEN_ABS : int, definition : int, axiom : int, 894 from_disk : int, oracle :int, total :int } 895\end{verbatim}\end{holboxed} 896 897\noindent This counter can be reset with the function: 898 899\begin{holboxed} 900\index{reset_thm_count@\ml{reset\_thm\_count}|pin} 901\begin{verbatim} 902 val reset_thm_count : unit -> unit 903\end{verbatim}\end{holboxed} 904 905Finally, the \texttt{Count} structure also includes another function 906which easily enables the number of inferences performed by an \ML{} 907procedure to be assessed: 908 909\begin{holboxed} 910\index{Count.apply@\ml{Count.apply}|pin} 911\begin{verbatim} 912 val apply : ('a -> 'b) -> 'a -> 'b 913\end{verbatim} 914\end{holboxed} 915 916An invocation, \ml{Count.apply f x}, applies the function \ml{f} to 917the argument \ml{x} and performs a count of inferences during this 918time. This function also records the total time taken in the 919execution of the application. 920 921For example, timing the action of \ml{numLib}'s \ml{ARITH\_CONV}: 922 923\setcounter{sessioncount}{1} 924\begin{session} 925\begin{verbatim} 926- Count.apply numLib.ARITH_CONV ``x > y ==> 2 * x > y``; 927runtime: 0.010s, gctime: 0.000s, systime: 0.000s. 928Axioms asserted: 0. 929Definitions made: 0. 930Oracle invocations: 0. 931Theorems loaded from disk: 0. 932HOL primitive inference steps: 165. 933Total: 165. 934> val it = |- x > y ==> 2 * x > y = T : thm 935\end{verbatim} 936\end{session} 937 938\index{counting inferences, in HOL proofs@counting inferences, in \HOL{} proofs|)} 939\index{inferences, in HOL logic@inferences, in \HOL{} logic!counting of|)} 940\index{timing of HOL evaluations@timing of \HOL{} evaluations|)} 941 942 943\section{\texorpdfstring{Embedding \HOL{} in \LaTeX{}}{Embedding HOL in \LaTeX{}}} 944 945\index{LaTeX@\LaTeX!embedding HOL@embedding in \HOL{}|(} 946% 947When writing documents in \LaTeX{} about one's favourite \HOL{} development, one frequently wants to include pretty-printed terms, types and theorems from that development. 948% 949Done manually, this will typically require involved use of the \texttt{alltt} environment, and cutting and pasting from a HOL session or theory file. 950% 951The 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. 952 953\newcommand{\munge}{\texttt{munge.exe}} 954\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})} 955% 956This 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. 957% 958(Strictly speaking, the distribution comes with a tool that itself creates \munge{}; see Section~\ref{sec:munger-creation} below.) 959% 960The basic philosophy is that a \LaTeX{} document can be written ``as normal'', but that three new \LaTeX{}-like commands are available to the author. 961 962The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter. 963% 964For example, one might write a document called \texttt{article.htex}. 965% 966This document contains instances of the new commands, and cannot be processed as is by \LaTeX{}. 967% 968Instead one first runs 969\begin{alltt} 970 \munge < article.htex > article.tex 971\end{alltt} 972and then runs \LaTeX{} on \texttt{article.tex}. 973% 974One would probably automate this process with a makefile of course. 975 976\subsection{Munging commands} 977\label{sec:munging-commands} 978% need to get backslashes conveniently obscures the real names, 979% preventing the munger from seeing them, which will be useful when we 980% run the munger over this document! 981\newcommand{\holtm}{\texttt{\bs{}HOLtm}} 982\newcommand{\holty}{\texttt{\bs{}HOLty}} 983\newcommand{\holthm}{\texttt{\bs{}HOLthm}} 984\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}. 985 986\bigskip 987There are then three commands for inserting text corresponding to \HOL{} entities into \LaTeX{} documents: \holtm, \holty{} and \holthm. 988% 989Each takes one argument, specifying something of the corresponding \HOL{} type. 990% 991In addition, options can be specified in square brackets, just as would be done with a genuine \LaTeX{} command. 992% 993For example, one can write 994\begin{alltt} 995 \holtm{}[tt]\{P(SUC n) /\bs{} q\} 996\end{alltt} 997and one will get \[ 998 \texttt{$P$ (SUC $n$) $\land$ $q$} 999\] 1000or 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}.} 1001% 1002Note 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{}. 1003% 1004This means that if the \HOL{} input is malformed, the \munge{} program will report errors. 1005% 1006Note also how the system knows that \texttt{P}, \texttt{n} and \texttt{q} are variables, and that \texttt{SUC} is not. 1007% 1008This analysis would not be possible without having \HOL{} actually parse and print the term itself. 1009 1010The default behaviours of each command are as follows: 1011\begin{description} 1012\item[\holty\{\textit{\mdseries{string}}\}] 1013% 1014\index{HOLty (munging command)@\holty{} (munging command)} 1015% 1016Parses the string argument as a type (the input must include the leading colon), and prints it. 1017% 1018The output is suited for inclusion in the normal flow of \LaTeX{} (it is an \texttt{\bs{}mbox}). 1019\item[\holtm\{\textit{\mdseries{string}}\}] 1020% 1021\index{HOLtm (munging command)@\holtm{} (munging command)} 1022% 1023Parses the string argument as a term, and prints it. 1024% 1025Again, the output is wrapped in an \texttt{\bs{}mbox}. 1026 1027\paragraph{Important:} If the string argument includes a right-brace character 1028(\ie, the character \rb, which has ASCII code 125), then it must be 1029escaped by preceding it with a backslash~(\bs). Otherwise, the 1030munger's lexer will incorrectly determine that the argument ends at 1031that right-brace character rather than at a subsequent one. 1032\item[\holthm\{\textit{\mdseries{thmspecifier}}\}] 1033% 1034\index{HOLthm (munging command)@\holthm{} (munging command)} 1035% 1036The argument should be of the form $\langle\mbox{\textit{theory}}\rangle\texttt{.}\langle{\mbox{\textit{theorem-name}}}\rangle$. 1037% 1038For example, \verb|\HOLthm{bool.AND_CLAUSES}|. 1039% 1040This prints the specified theorem with a leading turnstile. 1041% 1042\index{Datatype@\ml{Datatype}!printing in LaTeX@printing in \LaTeX{}} 1043However, 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. 1044% 1045Datatype theorems with these names are automatically generated when \ml{Datatype} is run. 1046If 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. 1047Also, if the type is a collection of nullary constants (a type consisting of only ``enumerated constants''), then it will always be printed compactly. 1048When not compact, all of a type's constructors will appear on the same line, or each will be on a separate line. 1049 1050By 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}. 1051(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. 1052The \texttt{verbatim} environment does the former, but not the latter.) 1053\end{description} 1054 1055\paragraph{Munging command options} 1056\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!command options} 1057There are a great many options for controlling the behaviour of each of these commands. 1058% 1059Some apply to all three commands, others are specific to a subset. 1060% 1061\newcommand{\indentoption}{\gt\gt} 1062If multiple options are desired, they should be separated by commas. For example: \texttt{\holthm{}[nosp,p/t,\indentoption]\{bool.AND\_CLAUSES\}}. 1063 1064\begin{description} 1065\item[\texttt{alltt}] Makes the argument suitable for inclusion in an \texttt{alltt} environment. 1066% 1067This is the default for \holthm. 1068\item[\texttt{case}] (Only for use with \holtm.) 1069% 1070Causes 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. 1071% 1072This preserves underscore-patterns, for example. 1073 1074\item[\texttt{conj}$n$] (Only for use with \holthm.) 1075Extracts the $n^{\mbox{\scriptsize th}}$ conjunct of a theorem. 1076The conjuncts are numbered starting at $1$, not $0$. 1077For example, 1078\begin{verbatim} 1079 \HOLthm[conj3]{bool.AND_CLAUSES} 1080\end{verbatim} 1081extracts the conjunct $\vdash \texttt{F} \land t \iff \texttt{F}$. 1082 1083\item[\texttt{def}] (Only for use with \holthm.) 1084% 1085Causes 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. 1086% 1087The turnstiles usually printed in front of theorems are also omitted. 1088% 1089This works well with definitions (or characterising theorems) over multiple data type constructors, changing 1090\begin{alltt} 1091\(\vdash\) (FACT 0 = 1) \(\land\) (\(\forall\)\ensuremath{n}. FACT (SUC \ensuremath{n}) = SUC \ensuremath{n} * FACT \ensuremath{n}) 1092\end{alltt} 1093into 1094\begin{alltt} 1095 FACT 0 = 1 1096 FACT (SUC \ensuremath{n}) = SUC \ensuremath{n} * FACT \ensuremath{n} 1097\end{alltt} 1098 1099\item[\texttt{depth}=$n$] 1100Causes printing to be done with a maximum print depth of $n$; see Section~\ref{sec:pretty-print-depth}. 1101 1102\item[\texttt{K}] (Only for use with \holtm.) 1103% 1104The argument must be the name of a theorem (as per the \holthm{} command), and the theorem should be of the form 1105\[ 1106\vdash f\;x\;t 1107\] 1108for some term $t$. 1109% 1110The command prints the term $t$. 1111% 1112\index{combinators, in HOL logic@combinators, in \HOL{} logic}% 1113\index{K, the HOL constant@\ml{K}, the \HOL{} constant}% 1114The 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. 1115% 1116In 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. 1117 1118\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!math mode} 1119\index{math mode (in the LaTeX munger)@math mode (in the \LaTeX{} munger)} 1120\item[\texttt{m}$\mathit{space}$,\texttt{nomath}] The \texttt{m} option makes \HOL{} material be typeset in ``math-mode''. 1121In particular, the output of the pretty-printer will be modified so that newline characters are replaced by \texttt{\bs\bs} commands. 1122This then requires that the surrounding \LaTeX{} environment be array-like, so that the \texttt{\bs\bs} command will have the desired effect. 1123 1124In 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. 1125By 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. 1126 1127For example, if the option is \texttt{m;}, then the spacing command will be \texttt{\bs;}. 1128If the option is \texttt{m;!}, then the spacing command will be \texttt{\bs;\bs!}. 1129The 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,}. 1130 1131The \texttt{m} option can be installed globally with the \texttt{-m} command-line option. 1132If this option is enabled globally, it can be cancelled on a case-by-case basis by using the \texttt{nomath} option. 1133The \texttt{nomath} option also takes precedence over any \texttt{m} options that might occur. 1134 1135See also the discussion about math-mode munging in Section~\ref{sec:math-mode-munging} below. 1136 1137\item[\texttt{merge}, \texttt{nomerge}] (For use with \holtm{} and \holthm.) 1138By 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. 1139% 1140This behaviour can be frustrating when getting one's \LaTeX{} to look ``just so'', so it can be turned off with the \texttt{nomerge} option. 1141 1142Additionally, this behaviour can be turned off globally with the \texttt{--nomergeanalysis} option to the munger. 1143% 1144If 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. 1145% 1146(In interactive HOL, the token-merging analysis is controlled by a trace variable called \texttt{"pp\_avoids\_symbol\_merges"}.) 1147 1148 1149\item[\texttt{nodollarparens}] (For use with \holtm{} and \holthm.) Causes the default escaping of syntactic sugar to be suppressed. 1150\index{ dollar sign, in HOL logic parser@\ml{\$} (dollar sign, in \HOL{} logic parser)!as escape character}% 1151\index{tokens!suppressing parsing behaviour of}% 1152The default behaviour is to use parentheses, so that 1153% encode all the special characters below so that emacs font-locking has a reasonable chance of working 1154\begin{alltt} 1155 \holtm\lb\dol/\bs p\rb 1156\end{alltt} 1157would get printed as $(\land)\;\,p$. 1158Note 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}. 1159However, with the \texttt{nodollarparens} option specified, nothing at all is printed to indicate that the special syntax has been ``escaped''. 1160 1161\item[\texttt{nosp}] (Only for use with \holthm.) 1162% 1163By default, arguments to \holthm{} are fully specialised (\ie, they have \ml{SPEC\_ALL} applied to them), removing outermost universal quantifiers. 1164% 1165The \texttt{nosp} option prevents this. 1166 1167\item[\texttt{nostile}] (Only for use with \holthm.) 1168% 1169By default, arguments to \holthm{} are printed with a turnstile~($\vdash$). 1170% 1171If this option is present, the turnstile is not printed (and the theorem will have its left margin three spaces further left). 1172% 1173For controlling how the turnstile is printed when this option is not present, see the paragraph on Overrides in Section~\ref{sec:running-munger}. 1174 1175\item[\texttt{of}] (Only for use with \holty.) 1176% 1177The argument is a string that parses to a \emph{term}, not a type. 1178% 1179The behaviour is to print the type of this term. 1180% 1181Thus \texttt{\holty{}[of]\{p /\bs{} q\}} will print \texttt{bool}. 1182 1183If the string includes right-braces, they must be escaped with 1184back-slashes, just as with the arguments to \holtm. 1185 1186\item[\texttt{rule}] (Only for use with \holtm{} and \holthm.) 1187Prints a term (or a theorem's conclusion) using the \texttt{\bs{}infer} command (available as part of the \texttt{proof.sty} package). 1188This gives a nice, ``natural deduction'' presentation. 1189\index{natural deduction!presentation style for the LaTeX munger@presentation style for the \LaTeX{} munger} 1190For example, the term 1191\begin{alltt} 1192 (p \bs{}/ q) /\bs{} (p ==> r) /\bs{} (q ==> r) ==> r 1193\end{alltt} 1194will print as 1195\[ 1196\infer{r}{p \lor q & p \Rightarrow r & q \Rightarrow r} 1197\] 1198Conjuncts to the left of the outermost implication (if any) will be split into hypotheses separated by whitespace. 1199For 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. 1200In this situation, the \texttt{stackedrule} option is appropriate. 1201 1202The term or theorem must be within a \LaTeX{} math-environment (it is typeset as if inline, with the \texttt{tt} option). 1203 1204For adding a name to the rule, see the \texttt{rulename} option below. 1205 1206\item[\texttt{rulename=}$\mathit{name}$] (Only has an effect with \texttt{rule} or \texttt{stackedrule}.) 1207Adds \textit{name} as the optional argument to the \texttt{\bs{}infer} command when typesetting the rule. 1208The name is wrapped with \texttt{\bs{}HOLRuleName}, which by default is the same as \texttt{\bs{}textsf}. 1209For ease of parsing options, \textit{name} should not contain braces, brackets, or commas. 1210(A name including such special characters could be typeset by renewing the \texttt{\bs{}HOLRuleName} command.) 1211 1212\item[\texttt{showtypes}$n$] (For use with \holthm{} and \holtm.) 1213% 1214Causes the term or theorem to be printed with the \texttt{types} trace set to level~$n$. 1215The $n$ is optional and defaults to $1$ if omitted (equivalent to having the \ml{show\_types} reference set to \ml{true}). 1216 1217\item[\texttt{stackedrule}] (For use with \holthm{} and \holtm.) 1218This 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. 1219Thus, 1220\begin{alltt} 1221 (p \bs{}/ q) /\bs{} (p ==> r) /\bs{} (q ==> r) ==> r 1222\end{alltt} 1223will print as 1224\[ 1225\infer{r}{\begin{array}{c}p \lor q \\ p \Rightarrow r \\ q \Rightarrow r\end{array}} 1226\] 1227For 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. 1228 1229For adding a name to the rule, see the \texttt{rulename} option. 1230 1231\item[\texttt{tr\apost}$\mathit{tracename}$\texttt{\apost=}$n$] 1232This option allows the temporary setting of the provided trace to the integer value $n$. 1233For example, one can set \texttt{pp\_unambiguous\_comprehensions} to $1$ to ensure that set comprehensions are printed with bound variables explicitly identified. 1234See Section~\ref{sec:set-syntax} for more on set comprehensions, and Section~\ref{sec:traces} for more on traces. 1235\index{traces, controlling HOL feedback@traces, controlling \HOL{} feedback!when munging to LaTeX@when munging to \LaTeX{}} 1236 1237\item[\texttt{tt}] % 1238Causes the term to be type-set as the argument to a \LaTeX{} command \texttt{\bs{}HOLinline}. 1239% 1240The default definition for \texttt{\bs{}HOLinline} is 1241\begin{verbatim} 1242 \newcommand{\HOLinline}[1]{\mbox{\textup{\texttt{#1}}}} 1243\end{verbatim} 1244This makes the argument suitable for inclusion in standard \LaTeX{} positions. 1245% 1246This is the default for \holtm{} and \holty. 1247% 1248(The \texttt{\bs{}HOLinline} command is defined in the \texttt{holtexbasic.sty} style file.) 1249 1250\item[\texttt{width=}$n$] Causes the argument to be typeset in lines of width $n$. 1251% 1252The default width is $63$, which seems to work well with 11pt fonts. 1253% 1254This default can also be changed at the time the \munge{} command is 1255run (see Section~\ref{sec:running-munger} below). 1256 1257\item[\texttt{-}$\mathit{name}$] 1258% 1259\index{parsing, of HOL logic@parsing, of \HOL{} logic!overloading} 1260This 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. 1261When used with \holty, prints the type with all type abbreviations for $\mathit{name}$ removed. 1262For example, the command \texttt{\holtm[-+]\lb{}x + y\rb} will print as 1263\[ 1264\texttt{arithmetic\dol+}\;x\;y 1265\] 1266because 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. 1267 1268\index{integers, the HOL theory of@integers, the \HOL{} theory of} 1269If the theory of integers is loaded, then the command \texttt{\holtm[-+]\lb{}x + y:int\rb} will print as \[ 1270\texttt{int\_add}\;x\;y 1271\] 1272because 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. 1273 1274The \texttt{-} option can be useful when complicated notation involving overloads is first introduced in a document. 1275 1276\item[\texttt{\indentoption} and \texttt{\indentoption\td}] Indents the argument. 1277% 1278 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}). 1279% 1280 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. 1281% 1282 For example, \texttt{\holthm{}[\indentoption10,...]\{...\}} will indent by 10 spaces. 1283 1284 Note that simply placing a command such as \holthm{} within its \texttt{alltt} block with a given indentation, for example 1285\begin{alltt} 1286 \bs{}begin\{alltt\} 1287 \holthm\{bool.AND_CLAUSES\} 1288 \bs{}end\{alltt\} 1289\end{alltt} 1290will not do the right thing if the output spans multiple lines. 1291% 1292Rather the first line of \HOL{} output will be indented, and the subsequent lines will not. 1293% 1294The \texttt{\indentoption} option lets the pretty-printer know that it is printing with a given indentation, affecting all lines of its output. 1295 1296The 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. 1297This allows one to achieve suitable alignment when other non-HOL text has been put onto the same line. 1298For example, 1299\begin{alltt} 1300 AND_CLAUSES \bs{}HOLthm[width=46,>>~12]\lb{}bool.AND_CLAUSES\rb 1301 TRUTH \bs{}HOLthm[>>~12]\lb{}bool.TRUTH\rb 1302 MAP \bs{}HOLthm[>>~12,width=50]\lb{}list.MAP\rb 1303\end{alltt} 1304ensures correct vertical alignment when extra lines are printed, as they will be with the printing of \ml{bool.AND_CLAUSES} and \ml{list.MAP}. 1305 1306\item[$\mathit{nm}_1\mathtt{/}\mathit{nm}_2$] (For use with \holtm{} 1307 and \holthm{}.) 1308% 1309Causes name $\mathit{nm}_1$ to be substituted for name $\mathit{nm}_2$ in the term or theorem. 1310% 1311This will rename both free and bound variables, wherever they occur throughout a term. 1312% 1313Because it uses instantiation, free variables in theorem hypotheses will get renamed, but bound variables in hypotheses are not affected. 1314% 1315(Hypotheses are not printed by default anyway of course.) 1316 1317If $\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. 1318 1319\item[$s\mathtt{//}t$] (For use with \holtm{}, \holthm, and \holty) Causes \LaTeX{} string $s$ to be substituted for token $t$. 1320This allows one-off manipulation of the override map (see Section~\ref{sec:running-munger} below). 1321The 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. 1322If printing depends on particular variable name choices, the ``last minute'' manipulations possible with this form of substitution may be preferable. 1323The width of the \LaTeX{} string is taken to be the width of the original token $t$. 1324\end{description} 1325 1326\subsection{Math-mode munging} 1327\label{sec:math-mode-munging} 1328\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!math mode} 1329\index{math mode (in the LaTeX munger)@math mode (in the \LaTeX{} munger)} 1330 1331There are a few steps needed to make math-mode munging a relatively painless affair. 1332First, there are two \LaTeX{} macros from \texttt{holtexbasic.sty} that should probably be overridden: 1333\begin{description} 1334\item[\texttt{\bs{}HOLConst}] By default this will print names in typewriter font. 1335In math mode, this will probably look better in sans serif, suggesting 1336\begin{verbatim} 1337 \renewcommand{\HOLConst}[1]{\textsf{#1}} 1338\end{verbatim} 1339Depending on personal taste, the \texttt{\bs{}HOLKeyword} macro might be redefined similarly. 1340This macro is used for keywords such as \texttt{if}. 1341\item[\texttt{\bs{}HOLinline}] This macro, used to wrap standard \texttt{\holtm} arguments, puts text into typewriter font. 1342One possibility for its redefinition would be 1343\begin{verbatim} 1344 \renewcommand{\HOLinline}[1]{\ensuremath{#1}} 1345\end{verbatim} 1346Note 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. 1347If necessary, this can be avoided on a case-by-case basis by setting the \texttt{width} option to a larger than normal width. 1348\end{description} 1349 1350When using math-mode munging, one also has to be aware of how larger pieces of text will appear. 1351In non-math-mode munging, material is usually put into \texttt{alltt} environments. 1352The recommended alternative for math-mode is to use the \texttt{\bs{}HOLmath} environment: 1353\begin{alltt} 1354 \textit{article text} 1355 1356 \bs{}begin\lb{}HOLmath\rb 1357 \holthm\lb{}bool.AND_CLAUSES\rb 1358 \bs{}end\lb{}HOLmath\rb 1359\end{alltt} 1360This uses a standard \texttt{array} environment within a \texttt{displaymath}. 1361 1362Occasionally, one will want to arrange blocks of \HOL{} material within a larger math context. 1363The \texttt{HOLarray} environment is a simple alias for a single-column left-aligned array that one can use in these situations. 1364 1365 1366\subsection{Creating a munger} 1367\label{sec:munger-creation} 1368 1369\newcommand{\mkmunge}{\texttt{mkmunge.exe}} 1370\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!creating a munger} 1371% 1372The \HOL{} distribution comes with a tool called \mkmunge. 1373% 1374This executable is used to create munge executables that behave as described in this section. 1375% 1376A typical invocation of \mkmunge{} is 1377\begin{alltt} 1378 \mkmunge \(\langle\mathit{thy}\sb{1}\rangle\)Theory ... \(\langle\mathit{thy}\sb{n}\rangle\)Theory 1379\end{alltt} 1380Each 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}. 1381 1382The \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 1383\begin{alltt} 1384 \mkmunge -o bagtexprocess bagTheory 1385\end{alltt} 1386 1387The 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. 1388 1389Under 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. 1390Doing 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. 1391The use of a base heap argument to \mkmunge{} doesn't affect the efficiency of the resulting munging tool. 1392 1393 1394\subsection{Running a munger} 1395\label{sec:running-munger} 1396 1397\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!running a munger} 1398Once created, a munger can be run as a filter command, consuming its 1399standard input, and writing to standard output. 1400% 1401It may also write error messages and warnings to its standard error. 1402 1403Thus, a standard pattern of use is something like 1404\begin{alltt} 1405 \munge < article.htex > article.tex 1406\end{alltt} 1407 1408However, there are a number of ways of further modifying the behaviour of the munger with command-line options. 1409 1410\paragraph{Overrides} 1411Most importantly, one can specify an ``overrides file'' to provide 1412token-to-\LaTeX{} replacements of what is pretty-printed. 1413% 1414The command-line would then look like 1415\begin{alltt} 1416 \munge overrides_file < article.htex > article.tex 1417\end{alltt} 1418The overrides file is a text file containing lines of the form 1419\begin{alltt} 1420 tok width tex 1421\end{alltt} 1422where \texttt{tok} is a \HOL{} token, \texttt{width} is a number 1423giving the width of the \LaTeX{}, and \texttt{tex} is a \LaTeX{} 1424string. 1425 1426As a very simple example, an overrides file might consist of just one 1427line: 1428\begin{alltt} 1429 pi1 2 \bs{}ensuremath\{\bs{}pi_1\} 1430\end{alltt} 1431This would cause the string \texttt{pi1} (presumably occurring in the 1432various \HOL{} entities as a variable name) to be replaced with the 1433rather prettier $\pi_1$. 1434% 1435The \texttt{2} records the fact that the 1436printer should record the provided \LaTeX{} as being 2 characters 1437wide. 1438% 1439This is important for the generation of reasonable line-breaks. 1440 1441Overrides for \HOL{} tokens can also be provided within \HOL{} 1442theories, using the 1443\texttt{TeX\_notation} command (see 1444Section~\ref{sec:holtheories-tex-ready} below). 1445 1446By overriding the special token \texttt{\$Turnstile\$}, one can control the printing of the turnstile produced by \holthm{}. 1447The default setup is roughly equivalent to overriding \texttt{\$Turnstile\$} to \texttt{\textbackslash{}HOLTokenTurnstile\{\}} followed by a space, giving a total width of \texttt{3}. 1448Overriding the turnstile in this way may will probably be necessary in math-mode printing, where the turnstile character is typically of the same width as 5 \texttt{\bs;} invocations. 1449Providing 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. 1450 1451\paragraph{Default width} 1452A munger can specify the default width in which \HOL{} will print its 1453output with a \texttt{-w} option. 1454% 1455For example, 1456\begin{alltt} 1457 \munge -w70 < article.htex > article.tex 1458\end{alltt} 1459This default width can be overridden on a case-by-case basis with the 1460\texttt{width=} option to any of the commands within a \LaTeX{} 1461document. 1462 1463\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. 1464 1465\smallskip \noindent The \texttt{-w}, \texttt{--nomergeanalysis} and 1466overrides file options can be given in any order. 1467 1468\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 1469enables math-mode typesetting by default. 1470 1471The specification of spacing is with a string of characters, as already described. 1472Note 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. 1473If the \texttt{-m} option appears without any additional characters, the default math-mode spacing will be \texttt{\bs;\bs;}. 1474 1475 1476\subsection{Holindex} 1477 1478\index{munging (producing LaTeX from HOL)@munging (producing \LaTeX{} from \HOL{})!Holindex} 1479Till now, it has been explained how the munger can be used as a preprocessor of \LaTeX{} sources. 1480Sometimes a tighter interaction with \LaTeX{} is beneficial. 1481Holindex is a \LaTeX{} package that provides genuine \LaTeX{} commands for inserting \HOL{}-theorems, types and terms as well as many related commands. 1482This 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. 1483Holindex can be found in \texttt{src/TeX/}. 1484There is also a demonstration file available in this directory. 1485 1486 1487\paragraph{Using Holindex} 1488To use Holindex add \texttt{\bs{}usepackage\{holindex\}} to the header 1489of the \LaTeX{} source file \texttt{article.tex}. Holindex loads the 1490\texttt{underscore} package which might cause trouble with references 1491and citations. In order to avoid problems, 1492\texttt{holindex} should be included after packages 1493like \texttt{natbib}. Holindex is used like BibTex or 1494MakeIndex. A run of \LaTeX{} on \texttt{jobname.tex} creates an 1495auxiliary file called \texttt{article.hix}. The munger is used to 1496process this file via 1497\begin{alltt} 1498 \munge -index article 1499\end{alltt} 1500This call generates two additional auxiliary files, 1501\texttt{article.tde} and \texttt{article.tid}. The following runs of 1502\LaTeX{} use these files. After modifying the source file, the munger 1503can be rerun to update \texttt{article.tde} and \texttt{article.tid}. 1504If you are using emacs with AUCTeX to write your latex files, you might 1505want to add 1506\begin{verbatim} 1507(eval-after-load "tex" '(add-to-list 'TeX-command-list 1508 '("Holindex" "munge.exe -index %s" 1509 TeX-run-background t t :help "Run Holindex") t)) 1510\end{verbatim} 1511to your emacs configuration file. This will allow 1512you to run Holindex using AUCTeX. 1513 1514\paragraph{Holindex commands} 1515\begin{description} 1516\item[\texttt{\bs{}blockHOLthm\{id\}}, \texttt{\bs{}blockHOLtm\{id\}}, \texttt{ 1517 \bs{}blockHOLty\{id\}}] These commands typeset the theorem, term 1518 or type with the given \texttt{id} as the argument to a \LaTeX{} 1519 command \texttt{\bs{}HOLblock}. They are intended for 1520 typesetting multiple lines in a new block. 1521 For theorem ids of the form \texttt{theory.thm} are predefined. All 1522 other ids have to be defined before usage as explained below. 1523% 1524\item[\texttt{\bs{}inlineHOLthm\{id\}}, \texttt{\bs{}inlineHOLtm\{id\}}, \texttt{\bs{}inlineHOLty\{id\}}] 1525 These commands are similar to \texttt{\bs{}blockHOLthm\{id\}}, \texttt{\bs{}blockHOLtm\{id\}} and \texttt{ 1526 \bs{}blockHOLty\{id\}}. However, they are intended for inline typesetting and 1527 use \texttt{\bs{}HOLinline} instead of \texttt{\bs{}HOLblock}. 1528% 1529\item[\texttt{\bs{}citeHOLthm\{id\}}, \texttt{\bs{}citeHOLtm\{id\}}, \texttt{\bs{}citeHOLty\{id\}}] 1530 These commands cite a theorem, term or type. 1531% 1532\item[\texttt{\bs{}mciteHOLthm\{id,id,...id\}}, \texttt{\bs{}mciteHOLtm\{ids\}}, \texttt{\bs{}mciteHOLty\{ids\}}] 1533 These commands cite multiple theorems, terms or types. 1534% 1535\item[\texttt{\bs{}citePureHOLthm\{id\}}, \texttt{\bs{}citePureHOLtm\{id\}}, 1536 \texttt{\bs{}citePureHOLty\{id\}}] These commands\linebreak cite a theorems, terms or types. 1537 They just typeset the number instead of the 1538 verbose form used by the \texttt{citeHOL} and \texttt{mciteHOL} commands. 1539 1540\item[\texttt{\bs{}citeHiddenHOLthm\{id\}}, 1541 \texttt{\bs{}citeHiddenHOLtm\{id\}}, 1542 \texttt{\bs{}citeHiddenHOLty\{id\}}] These commands cite a 1543 theorems, terms or types, but not typeset anything. These commands 1544 can be used to add a page to the list of pages a theorem, term or 1545 type is cited. 1546 1547 \item[\texttt{\bs{}printHOLIndex}, \texttt{\bs{}printHOLShortIndex}, 1548 \texttt{\bs{}printHOLLongIndex}] These commands typeset the index 1549 of all theorems, terms and types cited in the document. There are 1550 two types of entries in the index: long and short ones. Short 1551 entries contain a unique number, the label of the theorem, term or 1552 type and the pages it is cited. Long entries contain additionally 1553 a representation as it would be inserted by 1554 \texttt{\bs{}blockHOL...} as well as an optional description. 1555 Theorems use by default short entries, while terms and types use 1556 long ones. It is possible to change for each item whether a long 1557 or short entry should be used. \texttt{\bs{}printHOLIndex} prints 1558 the default index with mixed long and short entries. 1559 \texttt{\bs{}printHOLLongIndex} typesets just long entries and 1560 \texttt{\bs{}printHOLShortIndex} just short ones. 1561\end{description} 1562 1563 1564\paragraph{Defining and formatting terms, types and theorems} 1565 1566 Most of the Holindex commands require an identifier of a theorem, 1567 term or type as arguments. Theorem identifiers of the form 1568 \texttt{theory.theorem} are predefined. All other identifiers need 1569 defining. Additionally one might want to change the default 1570 formatting options for these new identifiers as well as the old ones. 1571 \HOL{} definition files can be used for defining and 1572 setting the formatting options of identifiers. They are used by 1573 putting the command \texttt{\bs{}useHOLfile\{\textit{filename.hdf}\}} in 1574 the header of your latex source file. These file use a syntax similar to 1575 BibTex. They consist of a list of entries of the form 1576 \begin{verbatim} 1577@EntryType{id, 1578 option = value, 1579 boolFlag, 1580 ... 1581} 1582\end{verbatim} 1583\noindent 1584There are the following entry types 1585\begin{description} 1586\item[\texttt{Thm}, \texttt{Theorem}] used to define and format a 1587 theorem. If the identifier is of the form \texttt{theory.theorem}, 1588 the \texttt{content} option can be skipped. Otherwise, the 1589 \texttt{content} option should be of this form and a new identifier 1590 is defined for the given theorem. This is for example useful if the 1591 theorem name contains special characters or if a theorem should 1592 be printed with different formatting options. 1593 \item[\texttt{Term}] 1594 used to define and format a term. 1595 \item[\texttt{Type}] 1596 used to define and format a type. 1597 \item[\texttt{Thms}, \texttt{Theorems}] used to set formatting options for 1598 a list of theorems. For example one might want to print long index entries 1599 for all theorems in a specific theory. For the \texttt{Theorems} entry 1600 the \texttt{id} part of the entry is given in the form 1601 \texttt{ids = [id,id,...]}. These \texttt{ids} may be theorem ids or special 1602 ids of the form \texttt{theorem.thmprefix*}. 1603 For example, the id 1604 \texttt{arithmetic.LESS\_EQ*} represents all theorems in 1605 theory \texttt{arithmetic} whose name starts with \texttt{LESS\_EQ}. 1606\end{description} 1607Options are name/value pairs. The value has to be quoted using 1608quotation marks or \HOL{}'s quotation syntax. There are the following 1609option names available: 1610\begin{description} 1611 \item[\texttt{content}] 1612 the content. For a term or type that's its \HOL{}\ definition. 1613 For theorems it is of the form \texttt{theory.theorem}. 1614 \item[\texttt{options}] 1615 formatting options for the munger as described in section~\ref{sec:munging-commands}. 1616 Please use the Holindex commands for typsetting inline or as a block instead 1617 of the options \texttt{tt} or \texttt{alltt}. 1618 \item[\texttt{label}] the label that will appear in the index. For 1619 theorems the label is by default its name and the label given here 1620 will be added after the name. 1621 \item[\texttt{comment}] \LaTeX{} code that gets typeset as a comment / description 1622 for long index entries. 1623 \item[\texttt{latex}] the \LaTeX{} code for the item. There are very rare cases, 1624 when it might be useful to provide handwritten \LaTeX{} code instead of the one 1625 generated by the munger. This option overrides the \LaTeX{} produced by the munger. 1626 It is recommended to use it very carefully. 1627\end{description} 1628Besides options, there are also boolean flags that change the formatting of entries: 1629\begin{description} 1630 \item[\texttt{force-index}] 1631 adds the entry to the index, even if it is not cited in the document. 1632 \item[\texttt{long-index}] 1633 use a long index-entry. 1634 \item[\texttt{short-index}] 1635 use a long index-entry. 1636\end{description} 1637Here is an example of such a \HOL{} definition file: 1638 1639\begin{verbatim} 1640@Term{term_id_1, 1641 content = ``SOME_FUN = SUC a < 0 /\ 0 > SUC b``, 1642 options = "width=20", 1643 label = "a short description of term from external file", 1644 comment = "some lengthy\\comment 1645 1646 with \textbf{formats} and newlines", 1647 force_index 1648} 1649 1650@Type{type_id_1, 1651 content = ``:bool`` 1652} 1653 1654@Thm{arithmetic.LESS_SUCC_EQ_COR, 1655 force-index, long-index 1656} 1657 1658@Thm{thm_1, 1659 label = "(second instance)", 1660 content = "arithmetic.LESS_SUC_EQ_COR" 1661} 1662 1663@Theorems{ 1664 ids = [arithmetic.LESS_ADD_SUC, 1665 arithmetic.LESS_EQ*], 1666 force-index 1667} 1668\end{verbatim} 1669 1670 1671\paragraph{Configuring Holindex} 1672 1673There are some commands that can be used to change the overall behaviour 1674of Holindex. They should be used in the header directly after \texttt{holindex} 1675is included. 1676\begin{description} 1677\item[\texttt{\bs{}setHOLlinewidth}] sets the default line-width. This 1678 corresponds to the \texttt{-w} option of the munger. 1679 1680\item[\texttt{\bs{}setHOLoverrides}] sets the ``overrides file'' to provide 1681token-to-\LaTeX{} replacements of what is pretty-printed. 1682 1683\item[\texttt{\bs{}useHOLfile}] 1684is used to include a \HOL{} definition file. Several such files might be 1685included. 1686\end{description} 1687 1688 1689\paragraph{Additional documentation} 1690For more information about Holindex, please refer to 1691the demonstration file \texttt{src/TeX/holindex-demo.tex}. This file contains 1692documentation for rarely used commands as well as explanations of how to 1693customise Holindex. 1694 1695 1696\subsection{\texorpdfstring{Making \HOL{} theories \LaTeX{}-ready}{Making HOL theories \LaTeX{}-ready}} 1697\label{sec:holtheories-tex-ready} 1698 1699Though 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''. 1700% 1701(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.) 1702 1703A token's printing form is given in a script-file with the \ml{TeX\_notation} command (from the \ml{TexTokenMap} module). 1704% 1705This function has type 1706\begin{alltt} 1707 \{ hol : string, TeX : string * int \} -> unit 1708\end{alltt} 1709The \ml{hol} field specifies the string of the token as \HOL{} prints it. 1710% 1711The \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). 1712 1713For example, in \texttt{boolScript.sml}, there are calls: 1714\begin{alltt} 1715 val _ = TeX_notation \{ hol = "!", TeX = ("\bs{}\bs{}HOLTokenForall\{\}", 1)\} 1716 val _ = TeX_notation \{ hol = UChar.forall, 1717 TeX = ("\bs{}\bs{}HOLTokenForall\{\}", 1)\} 1718\end{alltt} 1719The \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}). 1720% 1721Note also how the backslashes that are necessary for the \LaTeX{} command have to be doubled because they are appearing in an SML string. 1722 1723Finally, 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}. 1724% 1725Bindings for this, and a number of other \LaTeX{} commands are made in the file 1726\begin{alltt} 1727 src/TeX/holtexbasic.sty 1728\end{alltt} 1729which will need to be included in the \LaTeX{} source file. 1730% 1731(Such bindings can be overridden with the use of the command \texttt{\bs{}renewcommand}.) 1732 1733Finally, all theory-bindings made with \ml{TeX\_notation} can be overridden with \texttt{overrides} files referenced at the time a munger is run. 1734 1735 1736\index{LaTeX@\LaTeX!embedding HOL@embedding in \HOL{}|)} 1737 1738%%% Local Variables: 1739%%% mode: latex 1740%%% TeX-master: "description" 1741%%% End: 1742 1743% LocalWords: HOL mechanisations HOLHEAP Holmakefile 1744