12 \item The trace system for controlling feedback and printing.
15 an evaluation, and timing it.
16 \item A tool for embedding pretty-printed HOL theorems, terms and
41   and often accurate; however, it can be out-of-date, refer to earlier
46   This is helpful for locating functions and is automatically derived from the system sources, so it is always up-to-date.
51   Also, each axiom, definition, and theorem in the theory can be accessed by name in the help system.
52   As such theorems are pretty-printed into the corresponding \texttt{Theory.sig} file, the help system will find both the declaration in the signature (\eg, \ml{val~nm~:thm}), and the entry for that theorem in the comment-block.
65       \verb+help "list_Axiom"+ & theory structure signature and theorem
75 The trace system gives the user one central interface with which to control most of \HOL's many different flags, though they be scattered all over the system, and defined in different modules.
106 dependencies between files, (re)compile plain ML code, (re)compile and
107 execute theory scripts, and (re)compile the resulting theory modules.
110 to use, but there are some conventions and restrictions on it that
122 there are two modes of work: theory construction and system revision.
134 the formalization under development. The user needs to find and
137 and re-compiling and re-executing them.
142 To start a theory construction, some context (semantic, and also proof
143 support) is established, typically by loading parent theories and
146 definitions, builds and invokes tactics, and saves theorems---in a
152 Once the user finishes the perhaps long and arduous task of constructing
156 \item invoke \holmake{}. This will (a) compile and execute the
157   script file; and (b) compile the resulting theory file. After this,
161 \subsection{Source conventions for script and SML files}
163 \paragraph{Script and theory files}
170 and it can be loaded interactively:
180 This ``boilerplate'' ensures that the standard tactics and SML commands will be in the namespace when the script file is compiled.
181 Interactively, these modules have already been loaded and \texttt{open}-ed, so what can be typed directly at \texttt{hol} cannot necessarily be included as-is in a script file.
217 The calls to \texttt{new_theory} and \texttt{export_theory} must bracket a sequence of SML declarations.
225 This is because (due to restrictions imposed by Moscow~ML\index{Moscow ML}) the script file is required to be an ML structure, and the contents of a structure must be \emph{declarations}, not expressions.
226 Indeed, one is allowed to (and generally should) omit the bracketing
235 \HOL{} generates files containing this string, and when it cleans up after itself, it removes such files using a regular expression.
237 For example, if, in your development directory, you had a file of \ML{} code named \texttt{MyTheory.sml} and you were also managing a \HOL{} development there with \holmake, then \texttt{MyTheory.sml} would get deleted if \texttt{Holmake~clean} were invoked.
241 Most importantly, file names should match \texttt{signature} and \texttt{structure} names.
243 A signature for module \texttt{foo} should always appear in file \texttt{foo.sig}, and should have the form
250 The accompanying implementation of \texttt{foo} should appear in file \texttt{foo.sml}, and should have the form
270 \item Invoke \holmake{} to generate the theory and compile it.
275 Alternatively, and probably with the help of one of the editor modes,\footnote{There are editor modes for \texttt{emacs} and \texttt{vim}.} one can develop a theory with a script file that is always separately compilable.
280 Using a \texttt{Holmakefile} (see Section~\ref{sec:using-Holmakefiles}), it is possible to mention files in other directories, both as dependencies and as explicit targets with rules on how those targets should be built.
286 \holmake{} requires that, just as files must have an acyclic dependency graph, the directories containing those files must have a compatible, and acyclic, \texttt{INCLUDES} graph.
287 With \texttt{INCLUDES} information to hand, \holmake{} will process the entire \texttt{INCLUDES} graph, looking throughout the graph for theory files that the current directory may depend on, and rebuilding those remote targets as necessary.
293 (If successful such a build will enable other script-files to refer to that theory, and for interactive sessions to issue \ml{load~"xTheory";} commands.)
295 If there is none, or if that file specifies no targets, then \holmake{} will attempt to build all \ML{} modules and \HOL{} theories it can detect in the current directory.
316   (invocations of \texttt{prove} and \texttt{store\_thm}) to
319   theorems proved in this way and all subsequent theorems that depend
323 \item[{\tt --help} or {\tt -h}] Prints out a useful option summary and
344   time when \holmake{} completed, and when on a Unix system, the name
353   kernel when compiling scripts and libraries.  This is not
366   However, it will still attempt to do ``\HOL{} things'' with files whose names end in \texttt{Script} and \texttt{Theory}.
374   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.
403 combination of \holmake{} and a make-file is supposed to behave as
406 A make-file consists of two types of entries, variable definitions and
408 newline and \texttt{TAB} characters are very significant within them.
409 Comments can be started with hash (\texttt{\#}) characters and last
419 and a rule is of the form
461 \varref{FOO\_\varref{OS}} and have this first expand the \texttt{OS}
463 \texttt{unix}), and then have the resulting variable
481 target doesn't exist.  If there are no commands, and the target is not
485 rule, and the target is one that \holmake{} does know how to build,
487 has managed to infer for itself, and \holmake{} will build the target
490 commands and dependencies take precedence, and only they will be
499 This indicates that the action of executing the code in \texttt{thyScript.sml} will not only generate the usual \texttt{thyTheory.sig} and \texttt{thyTheory.sml} files, but also the file \texttt{target}.
500 If \holmake{} is asked to build any of these three files, and any is absent or out of date with respect to \texttt{thyScript.sml} (or any other dependency), then the code in \texttt{thyScript.sml} will be run.
516 comments on command-lines, and such ``comments'' will be passed to the
524 If a target is phony, then its dependencies will be built even if a file of that name exists and is newer than the dependencies.
525 \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.
558   words, and then transforms each word by attempting to see if it
562   white-space separated list and returned as the value.
576   characters like less-than and greater-than.  Those make-file
588 \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.
595 \paragraph{Special and pre-defined variables}
598 If defined, the \texttt{INCLUDES} variable is used to add directories to the list of directories consulted when files are compiled and linked.
604 By default, directories specified in the \texttt{INCLUDES} and \texttt{PRE\_INCLUDES} directory are also built by \holmake{} before it attempts to build in the current directory.
629 Finally there are variables that expand to program names and other
640 This variable expands to a list of the targets in the current directory that \holmake{} would build if there was no target in the Holmakefile, and no target was specified on the command-line.
654   for handling quotations), and the usual \texttt{-I} include
655   specifications (pre-includes, the hol-directory include, and the
695 The \texttt{MOSMLLEX} and \texttt{MOSMLYAC} abbreviations are really
705 We strongly discourage the use of \texttt{MOSMLYAC} and \texttt{MOSMLLEX}, even when running HOL under Moscow~ML.
718 There are four possible directives in a \texttt{Holmakefile}: \texttt{ifdef}, \texttt{ifndef}, \texttt{ifeq} and \texttt{ifneq}.
722 Conditional directives can be chained together with \texttt{else} directives, and must be terminated by the \texttt{endif} command.
749 The \texttt{ifneq} and \texttt{ifeq} forms test for string equality.
762 The definedness tests \texttt{ifdef} and \texttt{ifndef} test if a name has a non-null expansion in the current environment.
780 \section{\texorpdfstring{Generating and Using Heaps in Poly/ML \HOL{}}{Generating and Using Heaps in Poly/ML HOL}}
786 Poly/ML has a nice facility whereby the state of one of its interactive sessions can be stored on disk and then reloaded.
790 In Moscow~ML, \texttt{hol} starts up by visibly (and relatively slowly) ``loading'' the various source files that provide the system's functionality (\eg, \ml{bossLib}).
793 Such heaps can be preloaded with source code implementing special-purpose reasoning facilities, and with various necessary background theories.
799 This program takes a list of object files to include in a heap, an optional heap to build upon (use the \texttt{-b} command-line switch; the default is to use the heap behind the core \texttt{hol} executable), and an optional name for the new heap (the default is the traditional Unix \texttt{a.out}).
804 would build a heap in the current directory called \texttt{realheap}, and would preload it with the standard theories of transcendental numbers and real-valued polynomials.
824 If the heap's dependencies are not core \HOL{} theories as they are here, then both the dependency line and the arguments to \texttt{buildheap} will need to be adjusted to link to the directory containing the files.
826 Finally, note how the use of the \texttt{dprot} and \texttt{protect} functions will ensure that \holmake{} will do the right thing even when \texttt{HOLDIR} contains spaces.}
837 If the standard \texttt{hol} executable is invoked in a directory where there is a \texttt{Holmakefile} specifying a heap, the default heap will not be used and the given heap will be used instead.
856 Finally, note that when using the \texttt{HOLHEAP} variable, heaps are required to be built before everything else in a directory, and that such heaps embody theories or \ML{} sources that are \emph{ancestral} to the directory in which the heap occurs.
857 Thus, if one wanted to package up a heap embodying the standard theories for the real numbers, and to do it in \texttt{src/real} (which feels natural), this heap could be built using the method described here, but could only be referred to as a \texttt{HOLHEAP} in the directories that used it, \emph{not} in \texttt{src/real}'s \texttt{Holmakefile}.
864 \section{Timing and Counting Theorems}
872 inferences, axioms, definitions and use of oracles.  Such recording is
885 Calling \ml{counting\_thms true} enables counting, and
928 the argument \ml{x} and performs a count of inferences during this
958 When writing documents in \LaTeX{} about one's favourite \HOL{} development, one frequently wants to include pretty-printed terms, types and theorems from that development.
960 Done manually, this will typically require involved use of the \texttt{alltt} environment, and cutting and pasting from a HOL session or theory file.
967 This manual, and error-prone process is not necessary: the standard \HOL{} distribution comes with a tool called \munge{} to automate the process, and to remove the duplicate copies of \HOL{} text.
977 This document contains instances of the new commands, and cannot be processed as is by \LaTeX{}.
983 and then runs \LaTeX{} on \texttt{article.tex}.
998 There are then three commands for inserting text corresponding to \HOL{} entities into \LaTeX{} documents: \holtm, \holty{} and \holthm.
1008 and one will get \[
1011 or something very close to it, appearing in the resulting document.\footnote{The output is a mixture of typewriter font and math-mode characters embedded in a \texttt{\bs{}texttt} block within an \texttt{\bs{}mbox}.}
1013 Note how the spacing in the input (nothing between the \texttt{P} and the \texttt{SUC n}) is \emph{not} reflected in the output; this is because the input is parsed and pretty-printed with \HOL{}.
1017 Note also how the system knows that \texttt{P}, \texttt{n} and \texttt{q} are variables, and that \texttt{SUC} is not.
1019 This analysis would not be possible without having \HOL{} actually parse and print the term itself.
1027 Parses the string argument as a type (the input must include the leading colon), and prints it.
1034 Parses the string argument as a term, and prints it.
1096 Causes the theorem to be split into its constituent conjuncts, for each conjunct to have any outermost universal quantifiers removed, and for each to be printed on a line of its own.
1098 The turnstiles usually printed in front of theorems are also omitted, and a special form of equality is printed for the top-level (``defining'') equality in each clause.
1130 The argument must be the name of a theorem (as per the \holthm{} command), and the theorem should be of the form
1140 The expectation is that $f$ will be the combinator \holtxt{K} from \theoryimp{combin} (see Section~\ref{sec:combinTheory}), and that $x$ will be truth~(\holtxt{T}), allowing $t$ to be anything at all.
1142 In this way, large complicated terms that are not themselves theorems (or even of boolean type), can be stored in \HOL{} theories, and then printed in \LaTeX{} documents.
1163 \item[\texttt{merge}, \texttt{nomerge}] (For use with \holtm{} and \holthm.)
1164 By default, the HOL pretty-printer is paranoid about token-merging, and will insert spaces between the tokens it emits to try to ensure that what is output can be read in again without error.
1175 \item[\texttt{nodollarparens}] (For use with \holtm{} and \holthm.) Causes the default escaping of syntactic sugar to be suppressed.
1197 If this option is present, the turnstile is not printed (and the theorem will have its left margin three spaces further left).
1212 \item[\texttt{rule}] (Only for use with \holtm{} and \holthm.)
1238 \item[\texttt{showtypes}$n$] (For use with \holthm{} and \holtm.)
1241 The $n$ is optional and defaults to $1$ if omitted (equivalent to having the \ml{show\_types} reference set to \ml{true}).
1243 \item[\texttt{stackedrule}] (For use with \holthm{} and \holtm.)
1260 See Section~\ref{sec:set-syntax} for more on set comprehensions, and Section~\ref{sec:traces} for more on traces.
1272 This is the default for \holtm{} and \holty.
1292 because the underlying constant will no longer map to the string \texttt{"+"} and, in the absence of any other mappings for it, will be printed as a fully qualified name.
1302 \item[\texttt{\indentoption} and \texttt{\indentoption\td}] Indents the argument.
1318 Rather the first line of \HOL{} output will be indented, and the subsequent lines will not.
1330 ensures correct vertical alignment when extra lines are printed, as they will be with the printing of \ml{bool.AND_CLAUSES} and \ml{list.MAP}.
1333   and \holthm{}.)
1337 This will rename both free and bound variables, wherever they occur throughout a term.
1343 If $\mathit{nm}_1$ and $\mathit{nm}_2$ both begin with the colon character then they are parsed as types, and type instantiation is performed on the term or theorem argument instead of variable substitution.
1345 \item[$s\mathtt{//}t$] (For use with \holtm{}, \holthm, and \holty) Causes \LaTeX{} string $s$ to be substituted for token $t$.
1347 The difference between this operation and the ``normal substitution'' done with a single slash (as above) is that it happens as the \HOL{} entity is printed, whereas normal substitution happens before pretty-printing is done.
1413 The theories specified as arguments to \mkmunge{} determine what theorems are in scope for calls to \holthm, and also determine the grammars that will govern the parsing and printing of the \HOL{} types, terms and theorems.
1416 Doing so allows for the incorporation of many theories at once, and will be more efficient than loading the heap's theories separately on top of the default HOL heap.
1425 standard input, and writing to standard output.
1427 It may also write error messages and warnings to its standard error.
1449 giving the width of the \LaTeX{}, and \texttt{tex} is a \LaTeX{}
1489 \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.
1491 \smallskip \noindent The \texttt{-w}, \texttt{--nomergeanalysis} and
1494 \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
1507 Holindex is a \LaTeX{} package that provides genuine \LaTeX{} commands for inserting \HOL{}-theorems, types and terms as well as many related commands.
1508 This allows it to generate an index of all \HOL{}-theorems, types and terms that occur in the document as well as providing citation commands for \HOL{} entities in this index.
1517 and citations. In order to avoid problems,
1527 \texttt{article.tde} and \texttt{article.tid}.  The following runs of
1529 can be rerun to update \texttt{article.tde} and \texttt{article.tid}.
1551    These commands are similar to \texttt{\bs{}blockHOLthm\{id\}}, \texttt{\bs{}blockHOLtm\{id\}} and \texttt{
1552     \bs{}blockHOLty\{id\}}. However, they are intended for inline typesetting and
1564    verbose form used by the \texttt{citeHOL} and \texttt{mciteHOL} commands.
1575    of all theorems, terms and types cited in the document.  There are
1576    two types of entries in the index: long and short ones. Short
1578    type and the pages it is cited.  Long entries contain additionally
1581    Theorems use by default short entries, while terms and types use
1584    the default index with mixed long and short entries.
1585    \texttt{\bs{}printHOLLongIndex} typesets just long entries and
1590 \paragraph{Defining and formatting terms, types and theorems}
1597   \HOL{} definition files can be used for defining and
1612 \item[\texttt{Thm}, \texttt{Theorem}] used to define and format a
1615   \texttt{content} option should be of this form and a new identifier
1620     used to define and format a term.
1622     used to define and format a type.
1644     theorems the label is by default its name and the label given here
1671               with \textbf{formats} and newlines",
1736 The \ml{TeX} field specifies both the string that should be emitted into the \LaTeX{} output, and the width that this string should be considered to have (as in the \texttt{overrides} file).
1750 Bindings for this, and a number of other \LaTeX{} commands are made in the file

Indexes created Sun Jun 23 19:15:37 MDT 2024