IT/Description/misc.tex

11 \item The help system.
12 \item The trace system for controlling feedback and printing.
28  The kinds of help available are:
51   files, so they are always up-to-date. The signature of each theory
73 \section{The Trace System}
77 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.
81 The tool may still raise an exception when it fails, but it won't also
95 The \ml{traces} function returns a list of all the traces in the system.
96 The \ml{set\_trace} function allows the user to set a trace directly.
97 The effect of this might be seen in a subsequent call to \ml{traces()}.
106 The purpose of \holmake{} is to maintain dependencies in a \HOL{}
123 The development model that \holmake{} is designed to support is that
136 the formalization under development. The user needs to find and
194 The user has to resolve these, either by using the `dot' notation to
199 The following notes may be of some further help.
202 \item The filenames of theory scripts must follow the following
287   The file may be rebuilt anyway if other files you have specified
318   to build any theory files it encounters.  The times are logged in a
319   file in the current directory.  The name of this file includes the
347   fails to prove a theorem, quit the build.  The default is to use
371 all with the \texttt{--holmakefile} command-line option.  The
406 \paragraph{Variable definitions} The text on the RHS of a variable
445 \textsf{make}.  The files specified after the colon (if any) are those
512   left alone.  The modified words are then reassembled into a
516   of the percent~(\texttt{\%}) character.  The percent character
518   literally.  The instantiation for \texttt{\%} is remembered when the
545 The effect is as if the directories specified had all been included on the command-line with \texttt{-I} options.
546 The \texttt{PRE\_INCLUDES} variable works similarly, but the directories specified here are placed before the \mbox{\texttt{-I <sigobj>}} option that is used in invocations of compiler.
553 The \texttt{OPTIONS} variable is used for the specification of just
556 \texttt{QUIT\_ON\_FAILURE}.  The \texttt{OPTIONS} variable should be a
559 command-line options. The \texttt{EXTRA\_CLEANS} variable is used to
566 name of the first dependency of the rule.  The variable \texttt{\$@} is
573   appropriate program to perform a file copy.  The file to be copied
574   is the first argument, the second is the place to copy to.  The
578 \item[\texttt{HOLDIR}] The root of the HOL installation.
590 \item[\texttt{ML\_SYSNAME}] The name of the ML system being used:
605   appropriate program to perform a file movement.  The file to be
607   The second argument can be a directory.  (Under Unix, \texttt{MV}
617   \item[\texttt{UNQUOTE}] The location of the quotation-filter executable.
619 The \texttt{MOSMLLEX} and \texttt{MOSMLYAC} abbreviations are really
644 The versions including the extra `n' character reverse the boolean sense of the test.
648 The following example is a file that only has any content if the \texttt{POLY} variable is defined, which happens when Poly/ML is the underlying \ML{} system.
659 The next example includes chained \texttt{else} commands:
673 The \texttt{ifneq} and \texttt{ifeq} forms test for string equality.
686 The definedness tests \texttt{ifdef} and \texttt{ifndef} test if a name has a non-null expansion in the current environment.
692 The variable \texttt{FOOBAR} is also not defined.
712 The \HOL{} implementation uses this facility to implement the \texttt{hol} executable.
722 The easiest way to generate a \HOL{} heap is to use the \texttt{buildheap} executable that is built as part of the standard build process for (Poly/ML)~\HOL.
732 The use of the special variable \texttt{HOLHEAP} has a number of nice side effects.
762 The fact that this is happening is mentioned as the interactive session begins.
806 \ml{counting\_thms false} disables it.  The default is for counting to
810 are maintained.  The value of this counter is returned by the
882 The result is that one must also keep two copies of \HOL{} texts synchronised: if the \HOL{} development changes, the \LaTeX{} document should change as well.
891 The basic philosophy is that a \LaTeX{} document can be written ``as normal'', but that three new \LaTeX{}-like commands are available to the author.
893 The commands are not really processed by \LaTeX{}: instead the source file must first be passed through the \munge{} filter.
931 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}.}
941 The default behaviours of each command are as follows:
949 The output is suited for inclusion in the normal flow of \LaTeX{} (it is an \texttt{\bs{}mbox}).
967 The argument should be of the form $\langle\mbox{\textit{theory}}\rangle\texttt{.}\langle{\mbox{\textit{theorem-name}}}\rangle$.
979 (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.
980 The \texttt{verbatim} environment does the former, but not the latter.)
1004 The conjuncts are numbered starting at $1$, not $0$.
1015 The turnstiles usually printed in front of theorems are also omitted.
1029 The argument must be the name of a theorem (as per the \holthm{} command), and the theorem should be of the form
1035 The command prints the term $t$.
1039 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.
1058 The default behaviour is to use parentheses, so that
1071 The \texttt{nosp} option prevents this.
1081 The argument is a string that parses to a \emph{term}, not a type.
1083 The behaviour is to print the type of this term.
1106 The term or theorem must be within a \LaTeX{} math-environment (it is typeset as if inline, with the \texttt{tt} option).
1127 The default definition for \texttt{\bs{}HOLinline} is
1135 (The \texttt{\bs{}HOLinline} command is defined in the \texttt{holtexbasic.sty} style file.)
1139 The default width is $63$, which seems to work well with 11pt fonts.
1161 The \texttt{-} option can be useful when complicated notation involving overloads is first introduced in a document.
1167   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.
1181 The \texttt{\indentoption} option lets the pretty-printer know that it is printing with a given indentation, affecting all lines of its output.
1205 The \HOL{} distribution comes with a tool called \mkmunge.
1215 The \mkmunge{} program can also take an optional \texttt{-o} argument that is used to specify the name of the output munger (the default is \munge).  For example
1220 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.
1244 The command-line would then look like
1248 The overrides file is a text file containing lines of the form
1265 The \texttt{2} records the fact that the
1290 \smallskip \noindent The \texttt{-w}, \texttt{--nomergeanalysis} and
1312 auxiliary file called \texttt{article.hix}. The munger is used to
1318 \texttt{article.tde} and \texttt{article.tid}.  The following runs of
1419     ids of the form \texttt{theorem.thmprefix*}. The id
1423 Options are name/value pairs. The value has to be quoted using
1525 The \ml{hol} field specifies the string of the token as \HOL{} prints it.
1527 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).
1535 The \texttt{UChar} structure is a local binding in the script-file that points at the standard list of UTF8-encoded Unicode strings in the distribution (\ml{UnicodeChars}).