Manual/Description/misc.tex

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.
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.
291 Like {\tt make}, \holmake{} takes command-line arguments corresponding to the targets that the user desires to build.
292 As a special case of this, targets ending with the suffix \ml{Theory} are treated as an instruction to build the theory files that lie behind a \HOL{} theory.
294 If there are no command-line targets, then \holmake{} will look for a \texttt{Holmakefile} in the current directory.
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.
298 In addition, there are three special targets that can be used:
333   As above, directories specified in this way will also be rebuilt before the current targets are built.
339   to build all specified targets, rather than stopping as soon as one
384 When building normally, all targets in ``includes'' directories are built; normally only dependencies of targets in the current directory are built.
519 \paragraph{Special targets}
522 \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.
523 For example, targets naming conceptual collections of files such as \texttt{all} should be marked as ``phony''.
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.
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.