Permalink
Browse files

Implement recursive cleaning for Holmake.

Closes #125; not extensively tested.
  • Loading branch information...
1 parent 25c45b9 commit e63d42fcb4f24d0a5102646264826428737d1278 @mn200 mn200 committed Jul 17, 2013
@@ -249,6 +249,7 @@ \subsection{What \holmake{} doesn't do}
\holmake{} only works properly on the current directory.
\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.
+\index{Holmake@\holmake!recursive invocation}%
However, 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}.
Such a specification will cause \holmake{} to look in the specified directories for other theory files that the current directory may depend on.
Moreover, by default \holmake{} will recursively call itself on all those ``include'' directories before doing anything in the current directory.
@@ -294,6 +295,9 @@ \subsection{\holmake{}'s command-line arguments}
\texttt{fast\_proof} oracle tag. This tag will appear on all
theorems proved in this way and all subsequent theorems that depend
on such theorems. \holmake's default is not to build in fast mode.
+\item[\texttt{-r}]%
+\index{Holmake@\holmake!recursive invocation}%
+Forces \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).
\item[\texttt{--fast}] Makes \holmake's default be to build in fast
mode (see above).
\item[{\tt --help} or {\tt -h}] Prints out a useful option summary and
@@ -327,8 +331,9 @@ \subsection{\holmake{}'s command-line arguments}
this option makes the compilation not use the overlay file. This
option is also used in building the kernel before the overlay itself
has been compiled.
-\item[\texttt{--no\_prereqs}] Do not recursively attempt to build
- ``include'' directories before working in the current directory.
+\item[\texttt{--no\_prereqs}]%
+\index{Holmake@\holmake!recursive invocation}%
+Do not recursively attempt to build ``include'' directories before working in the current directory.
\item[\texttt{--no\_sigobj}] Do not link against HOL system's
directory of HOL system files. Use of this option goes some way
towards turning
@@ -346,7 +351,7 @@ \subsection{\holmake{}'s command-line arguments}
\holmake{}. Fatal error messages will still be written to the
standard error stream. Note that other programs called by \holmake{} will not
be affected.
-\item[{\tt --rebuild\_deps} or {\tt -r}] Forces \holmake{} to always
+\item[{\tt --rebuild\_deps}] Forces \holmake{} to always
rebuild the dependency information for files it examines, whether or
not it thinks it needs to. This option is implemented by having
\holmake{} wipe all of its dependency cache (as per the
@@ -536,16 +541,14 @@ \subsection{Using a make-file with \holmake}
\paragraph{Special and pre-defined variables}
\index{Holmake@\holmake!variables in makefiles}
-If defined, the \texttt{INCLUDES} variable is used to add directories
-to the list of directories consulted when files are compiled and
-linked. The effect is as if the directories specified had all been
-included on the command-line with \texttt{-I} options. The
-\texttt{PRE\_INCLUDES} variable works similarly, but the directories
-specified here are placed before the \mbox{\texttt{-I <holdir>}}
-option that is used in invocations of compiler. This
-option gives the user a way of over-riding code in the core
-distribution as the compiler will find their code
-before the distribution's.
+If defined, the \texttt{INCLUDES} variable is used to add directories to the list of directories consulted when files are compiled and linked.
+The effect is as if the directories specified had all been included on the command-line with \texttt{-I} options.
+The \texttt{PRE\_INCLUDES} variable works similarly, but the directories specified here are placed before the \mbox{\texttt{-I <sigobj>}} option that is used in invocations of compiler.
+This option gives the user a way of over-riding code in the core distribution as the compiler will find their code before the distribution's.
+
+\index{Holmake@\holmake!recursive invocation}
+By default, directories specified in the \texttt{INCLUDES} and \texttt{PRE\_INCLUDES} directory are also built by \holmake{} before it attempts to build in the current directory.
+If the \texttt{-r} (``force recursion'') command-line flag is used, these directories are also ``clean''-ed when a cleaning target is given to \holmake{}.
The \texttt{OPTIONS} variable is used for the specification of just
four possible options (others are ignored): \texttt{NO\_SIGOBJ},
@@ -269,7 +269,7 @@ fun parse_command_line list = let
val (rem, dontmakes) = find_pairs "-d" rem
val (rem, debug) = find_toggle "--d" rem
val (rem, help) = find_alternative_tags ["--help", "-h"] rem
- val (rem, rebuild_deps) = find_alternative_tags ["--rebuild_deps","-r"] rem
+ val (rem, rebuild_deps) = find_toggle "--rebuild_deps" rem
val (rem, cmdl_HOLDIRs) = find_pairs "--holdir" rem
val (rem, no_sigobj) = find_alternative_tags ["--no_sigobj", "-n"] rem
val (rem, allfast) = find_toggle "--fast" rem
@@ -278,6 +278,7 @@ fun parse_command_line list = let
val (rem, ot) = find_toggle "--ot" rem
val (rem, no_hmakefile) = find_toggle "--no_holmakefile" rem
val (rem, no_prereqs) = find_toggle "--no_prereqs" rem
+ val (rem, recursive) = find_toggle "-r" rem
val (rem, user_hmakefile) =
find_one_pairtag "--holmakefile" NONE SOME rem
val (rem, no_overlay) = find_toggle "--no_overlay" rem
@@ -297,7 +298,9 @@ in
always_rebuild_deps=rebuild_deps,
additional_includes=includes,
dontmakes=dontmakes, no_sigobj = no_sigobj,
- quit_on_failure = qofp, no_prereqs = no_prereqs,
+ quit_on_failure = qofp,
+ no_prereqs = no_prereqs,
+ cline_recursive = recursive,
opentheory = ot, no_hmakefile = no_hmakefile,
allfast = allfast, fastfiles = fastfiles,
user_hmakefile = user_hmakefile,
@@ -347,7 +350,7 @@ val {targets, debug, dontmakes, show_usage, allfast, fastfiles,
no_sigobj = cline_no_sigobj, no_prereqs,
quit_on_failure, no_hmakefile, user_hmakefile, no_overlay,
no_lastmakercheck, user_overlay, keep_going_flag, quiet_flag,
- do_logging_flag} =
+ do_logging_flag, cline_recursive} =
parse_command_line (CommandLine.arguments())
val (outputfunctions as {warn,info,tgtfatal,diag}) =
@@ -542,7 +545,12 @@ val EXE_POLY =
else POLY
val quit_on_failure = quit_on_failure orelse hmake_qof
-val no_prereqs = no_prereqs orelse hmake_noprereqs
+
+val _ = if cline_recursive andalso no_prereqs then
+ warn("-r forces recursion, taking precedence over --no_prereqs")
+ else ()
+val no_prereqs = (no_prereqs orelse hmake_noprereqs) andalso not cline_recursive
+
val _ =
if quit_on_failure andalso allfast then
warn "quit on (tactic) failure ignored for fast built theories"
@@ -1326,14 +1334,14 @@ in
if keep_going_flag then keep_going tgts else stop_on_failure tgts
end
-fun hm_recur k =
+fun hm_recur ctgt k =
maybe_recurse
{warn = warn, no_prereqs = no_prereqs, hm = Holmake,
visited = visiteddirs,
includes =
cline_additional_includes @ envlist "PRE_INCLUDES" @ hmake_includes,
dir = {abspath = dir, relpath = dirnm},
- local_build = k}
+ local_build = k, cleantgt = ctgt}
in
case targets of
@@ -1350,16 +1358,21 @@ in
end
else ()
in
- hm_recur (fn () => finish_logging (strategy targets))
+ hm_recur NONE (fn () => finish_logging (strategy targets))
end
| xs => let
fun isPhony x = member x ["clean", "cleanDeps", "cleanAll"] orelse
x in_target ".PHONY"
in
- if List.all isPhony xs then
+ if List.all isPhony xs andalso not cline_recursive then
if finish_logging (strategy xs) then SOME visiteddirs else NONE
else
- hm_recur (fn () => finish_logging (strategy xs))
+ let
+ val ctgt =
+ List.find (fn s => member s ["clean", "cleanDeps", "cleanAll"]) xs
+ in
+ hm_recur ctgt (fn () => finish_logging (strategy xs))
+ end
end
end
@@ -1375,6 +1388,7 @@ in
" -I <file> : include directory (can be repeated)\n",
" -d <file> : ignore file (can be repeated)\n",
" -f <theory> : toggles fast build (can be repeated)\n",
+ " -r : force recursion (even for cleans)\n",
" --d : print debugging information\n",
" --fast : files default to fast build; -f toggles\n",
" --help | -h : show this message\n",
@@ -1383,7 +1397,7 @@ in
" --interactive | -i : run HOL with \"interactive\" flag set\n",
" --keep-going | -k : don't stop on failure\n",
" --logging : do per-theory time logging\n",
- " --polymllibdir directory : use specified directory for Poly/ML's libraries\n",
+ " --polymllibdir <dir> : use specified directory for Poly/ML's libraries\n",
" --poly file : use specified file as the Poly/ML executable\n",
" --poly_not_hol : Treat the Poly/ML executable as plain, not as a hol-augmented executable\n",
" --no_holmakefile : don't use any Holmakefile\n",
@@ -1394,7 +1408,7 @@ in
" --ot : log an OpenTheory article for each theory\n",
" --qof : quit on tactic failure\n",
" --quiet : be quieter in operation\n",
- " --rebuild_deps | -r : always rebuild dependency info files \n"]
+ " --rebuild_deps : always rebuild dependency info files \n"]
else let
open OS.Process
val result =
View
@@ -283,14 +283,15 @@ fun parse_command_line list = let
val (rem, dontmakes) = find_pairs "-d" rem
val (rem, debug) = find_toggle "--debug" rem
val (rem, help) = find_alternative_tags ["--help", "-h"] rem
- val (rem, rebuild_deps) = find_alternative_tags ["--rebuild_deps","-r"] rem
+ val (rem, rebuild_deps) = find_toggle "--rebuild_deps" rem
val (rem, cmdl_HOLDIRs) = find_pairs "--holdir" rem
val (rem, no_sigobj) = find_alternative_tags ["--no_sigobj", "-n"] rem
val (rem, allfast) = find_toggle "--fast" rem
val (rem, fastfiles) = find_pairs "-f" rem
val (rem, qofp) = find_toggle "--qof" rem
val (rem, no_hmakefile) = find_toggle "--no_holmakefile" rem
val (rem, no_prereqs) = find_toggle "--no_prereqs" rem
+ val (rem, recursive) = find_toggle "-r" rem
val (rem, user_hmakefile) =
find_one_pairtag "--holmakefile" NONE SOME rem
val (rem, no_overlay) = find_toggle "--no_overlay" rem
@@ -308,7 +309,9 @@ in
always_rebuild_deps=rebuild_deps,
additional_includes=includes,
dontmakes=dontmakes, no_sigobj = no_sigobj,
- quit_on_failure = qofp, no_prereqs = no_prereqs,
+ quit_on_failure = qofp,
+ no_prereqs = no_prereqs,
+ cline_recursive = recursive,
no_hmakefile = no_hmakefile,
allfast = allfast, fastfiles = fastfiles,
user_hmakefile = user_hmakefile,
@@ -347,7 +350,8 @@ val {targets, debug, dontmakes, show_usage, allfast, fastfiles,
cmdl_HOLDIR, cmdl_MOSMLDIR, nob2002, no_lastmakercheck,
no_sigobj = cline_no_sigobj, no_prereqs,
quit_on_failure, no_hmakefile, user_hmakefile, no_overlay,
- user_overlay, keep_going_flag, quiet_flag, do_logging_flag} =
+ user_overlay, keep_going_flag, quiet_flag, do_logging_flag,
+ cline_recursive} =
parse_command_line (CommandLine.arguments())
val nob2002 = nob2002 orelse Systeml.HAVE_BASIS2002
@@ -534,7 +538,12 @@ val extra_cleans = envlist "EXTRA_CLEANS"
val nob2002 = nob2002 orelse hmake_no_basis2002
val quit_on_failure = quit_on_failure orelse hmake_qof
-val no_prereqs = no_prereqs orelse hmake_noprereqs
+
+val _ = if cline_recursive andalso no_prereqs then
+ warn("-r forces recursion, taking precedence over --no_prereqs")
+ else ()
+val no_prereqs = (no_prereqs orelse hmake_noprereqs) andalso not cline_recursive
+
val _ =
if quit_on_failure andalso allfast then
warn "quit on (tactic) failure ignored for fast built theories"
@@ -1178,33 +1187,44 @@ in
if keep_going_flag then keep_going tgts else stop_on_failure tgts
end
-fun hm_recur k =
+fun hm_recur ctgt k =
maybe_recurse
{warn = warn, no_prereqs = no_prereqs, hm = Holmake,
visited = visiteddirs,
includes =
cline_additional_includes @ envlist "PRE_INCLUDES" @ hmake_includes,
dir = {abspath = dir, relpath = dirnm},
- local_build = k}
+ local_build = k, cleantgt = ctgt}
in
case targets of
[] => let
val targets = generate_all_plausible_targets ()
+ val targets = map fromFile targets
val _ =
- if debug then
- print("Generated targets are: "^print_list (map fromFile targets)^"\n")
+ if debug then let
+ val tgtstrings =
+ map (fn s => if OS.FileSys.access(s,[]) then s else s ^ "(*)")
+ targets
+ in
+ print("Generated targets are: "^print_list tgtstrings ^ "\n")
+ end
else ()
in
- hm_recur
- (fn () => finish_logging (strategy (map (fromFile) targets)))
+ hm_recur NONE (fn () => finish_logging (strategy targets))
end
| xs => let
fun isPhony x = member x ["clean", "cleanDeps", "cleanAll"] orelse
x in_target ".PHONY"
in
- if List.all isPhony xs then
+ if List.all isPhony xs andalso not cline_recursive then
if finish_logging (strategy xs) then SOME visiteddirs else NONE
- else hm_recur (fn () => finish_logging (strategy xs))
+ else
+ let
+ val ctgt =
+ List.find (fn s => member s ["clean", "cleanDeps", "cleanAll"]) xs
+ in
+ hm_recur ctgt (fn () => finish_logging (strategy xs))
+ end
end
end
@@ -1221,6 +1241,7 @@ val _ =
" -I <file> : include directory (can be repeated)\n",
" -d <file> : ignore file (can be repeated)\n",
" -f <theory> : toggles fast build (can be repeated)\n",
+ " -r : force recursion (even for cleans)\n",
" --debug : print debugging information\n",
" --fast : files default to fast build; -f toggles\n",
" --help | -h : show this message\n",
@@ -1237,7 +1258,7 @@ val _ =
" --overlay <file> : use given .ui file as overlay\n",
" --qof : quit on tactic failure\n",
" --quiet : be quieter in operation\n",
- " --rebuild_deps | -r : always rebuild dependency info files \n"]
+ " --rebuild_deps : always rebuild dependency info files \n"]
else let
open Process
val result =
@@ -44,7 +44,8 @@ sig
visited: string Binaryset.set,
includes : string list,
dir : {abspath: string, relpath: string option},
- local_build : unit -> bool} ->
+ local_build : unit -> bool,
+ cleantgt : string option} ->
string Binaryset.set option
end
@@ -224,9 +224,11 @@ end handle OS.SysErr (mesg, _) => let
| DirNotFound => true
-fun maybe_recurse {warn,no_prereqs,hm,visited,includes,dir,local_build=k} =
+fun maybe_recurse {warn,no_prereqs,hm,visited,includes,dir,local_build=k,
+ cleantgt} =
let
val {abspath=dir,relpath} = dir
+ val tgts = case cleantgt of SOME s => [s] | NONE => []
fun recurse visited (newdir,nm) =
if Binaryset.member(visited, newdir) then SOME visited
else let
@@ -239,7 +241,7 @@ let
val nm = case newrelpath of NONE => newdir | SOME d => d
val _ = warn ("Recursively calling Holmake in "^nm)
in
- hm {relpath=newrelpath,abspath=newdir} visited [] []
+ hm {relpath=newrelpath,abspath=newdir} visited [] tgts
before
(warn ("Finished recursive invocation in "^nm);
FileSys.chDir dir)

0 comments on commit e63d42f

Please sign in to comment.