# HG changeset patch # User wenzelm # Date 1343642628 -7200 # Node ID 231e6fa96dbb9210e2f6e7a4415dc7f4957689a3 # Parent c24907e5081e3ab280c77af531c926c013c255c5 added build option -c; tuned; diff -r c24907e5081e -r 231e6fa96dbb doc-src/System/Thy/Sessions.thy --- a/doc-src/System/Thy/Sessions.thy Mon Jul 30 11:03:44 2012 +0200 +++ b/doc-src/System/Thy/Sessions.thy Mon Jul 30 12:03:48 2012 +0200 @@ -167,6 +167,7 @@ Options are: -a select all sessions -b build heap images + -c clean build -d DIR include session directory with ROOT file -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) @@ -221,6 +222,14 @@ saved for inner nodes of the hierarchy of sessions, as required for other sessions to continue later on. + \medskip Option @{verbatim "-c"} cleans all descendants of the + selected sessions before performing the specified build operation. + + \medskip Option @{verbatim "-n"} omits the actual build process + after the preparatory stage (including optional cleanup). Note that + the return code always indicates the status of the set of selected + sessions. + \medskip Option @{verbatim "-j"} specifies the maximum number of parallel build jobs (prover processes). Note that each process is subject to a separate limit of parallel threads, cf.\ system option @@ -232,10 +241,6 @@ @{setting ISABELLE_OUTPUT} (which is normally in @{setting ISABELLE_HOME_USER}, i.e.\ the user's home directory). - \medskip Option @{verbatim "-n"} omits the actual build process - after performing all dependency checks. The return code indicates - the status of the set of selected sessions. - \medskip Option @{verbatim "-v"} enables verbose mode. *} @@ -247,30 +252,40 @@ isabelle build -b HOLCF \end{ttbox} - Build the main group of logic images (as determined by the session - ROOT specifications of the Isabelle distribution): + \smallskip Build the main group of logic images (as determined by + the session ROOT specifications of the Isabelle distribution): \begin{ttbox} isabelle build -b -g main \end{ttbox} - Provide a general overview of the status of all Isabelle sessions, - without building anything: + \smallskip Provide a general overview of the status of all Isabelle + sessions, without building anything: \begin{ttbox} isabelle build -a -n -v \end{ttbox} - Build all sessions with HTML browser info and PDF document - preparation: + \smallskip Build all sessions with HTML browser info and PDF + document preparation: \begin{ttbox} isabelle build -a -o browser_info -o document=pdf \end{ttbox} - Build all sessions with a maximum of 8 prover processes and 4 - threads each (on a machine with many cores): - + \smallskip Build all sessions with a maximum of 8 prover processes + and 4 threads each (on a machine with many cores): \begin{ttbox} isabelle build -a -j8 -o threads=4 \end{ttbox} + + \smallskip Build some session images with cleanup of their + descendants, while retaining their ancestry: +\begin{ttbox} +isabelle build -b -c HOL-Boogie HOL-SPARK +\end{ttbox} + + \smallskip Clean all sessions without building anything: +\begin{ttbox} +isabelle build -a -n -c +\end{ttbox} *} end diff -r c24907e5081e -r 231e6fa96dbb doc-src/System/Thy/document/Sessions.tex --- a/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 11:03:44 2012 +0200 +++ b/doc-src/System/Thy/document/Sessions.tex Mon Jul 30 12:03:48 2012 +0200 @@ -277,6 +277,7 @@ Options are: -a select all sessions -b build heap images + -c clean build -d DIR include session directory with ROOT file -g NAME select session group NAME -j INT maximum number of parallel jobs (default 1) @@ -327,6 +328,14 @@ saved for inner nodes of the hierarchy of sessions, as required for other sessions to continue later on. + \medskip Option \verb|-c| cleans all descendants of the + selected sessions before performing the specified build operation. + + \medskip Option \verb|-n| omits the actual build process + after the preparatory stage (including optional cleanup). Note that + the return code always indicates the status of the set of selected + sessions. + \medskip Option \verb|-j| specifies the maximum number of parallel build jobs (prover processes). Note that each process is subject to a separate limit of parallel threads, cf.\ system option @@ -337,10 +346,6 @@ \verb|$ISABELLE_HOME/heaps| instead of the default location \hyperlink{setting.ISABELLE-OUTPUT}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}OUTPUT}}}} (which is normally in \hyperlink{setting.ISABELLE-HOME-USER}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}HOME{\isaliteral{5F}{\isacharunderscore}}USER}}}}, i.e.\ the user's home directory). - \medskip Option \verb|-n| omits the actual build process - after performing all dependency checks. The return code indicates - the status of the set of selected sessions. - \medskip Option \verb|-v| enables verbose mode.% \end{isamarkuptext}% \isamarkuptrue% @@ -355,29 +360,39 @@ isabelle build -b HOLCF \end{ttbox} - Build the main group of logic images (as determined by the session - ROOT specifications of the Isabelle distribution): + \smallskip Build the main group of logic images (as determined by + the session ROOT specifications of the Isabelle distribution): \begin{ttbox} isabelle build -b -g main \end{ttbox} - Provide a general overview of the status of all Isabelle sessions, - without building anything: + \smallskip Provide a general overview of the status of all Isabelle + sessions, without building anything: \begin{ttbox} isabelle build -a -n -v \end{ttbox} - Build all sessions with HTML browser info and PDF document - preparation: + \smallskip Build all sessions with HTML browser info and PDF + document preparation: \begin{ttbox} isabelle build -a -o browser_info -o document=pdf \end{ttbox} - Build all sessions with a maximum of 8 prover processes and 4 - threads each (on a machine with many cores): - + \smallskip Build all sessions with a maximum of 8 prover processes + and 4 threads each (on a machine with many cores): \begin{ttbox} isabelle build -a -j8 -o threads=4 +\end{ttbox} + + \smallskip Build some session images with cleanup of their + descendants, while retaining their ancestry: +\begin{ttbox} +isabelle build -b -c HOL-Boogie HOL-SPARK +\end{ttbox} + + \smallskip Clean all sessions without building anything: +\begin{ttbox} +isabelle build -a -n -c \end{ttbox}% \end{isamarkuptext}% \isamarkuptrue% diff -r c24907e5081e -r 231e6fa96dbb lib/Tools/build --- a/lib/Tools/build Mon Jul 30 11:03:44 2012 +0200 +++ b/lib/Tools/build Mon Jul 30 12:03:48 2012 +0200 @@ -28,6 +28,7 @@ echo " Options are:" echo " -a select all sessions" echo " -b build heap images" + echo " -c clean build" echo " -d DIR include session directory with ROOT file" echo " -g NAME select session group NAME" echo " -j INT maximum number of parallel jobs (default 1)" @@ -58,6 +59,7 @@ ALL_SESSIONS=false BUILD_HEAP=false +CLEAN_BUILD=false declare -a MORE_DIRS=() declare -a SESSION_GROUPS=() MAX_JOBS=1 @@ -66,7 +68,7 @@ SYSTEM_MODE=false VERBOSE=false -while getopts "abd:g:j:no:sv" OPT +while getopts "abcd:g:j:no:sv" OPT do case "$OPT" in a) @@ -75,6 +77,9 @@ b) BUILD_HEAP="true" ;; + c) + CLEAN_BUILD="true" + ;; d) MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG" ;; @@ -121,7 +126,8 @@ fi "$ISABELLE_TOOL" java isabelle.Build \ - "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ + "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \ + "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \ "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@" RC="$?" diff -r c24907e5081e -r 231e6fa96dbb src/Pure/System/build.scala --- a/src/Pure/System/build.scala Mon Jul 30 11:03:44 2012 +0200 +++ b/src/Pure/System/build.scala Mon Jul 30 12:03:48 2012 +0200 @@ -64,14 +64,27 @@ def - (name: String): Queue = new Queue(graph.del_node(name)) - def required(groups: List[String], names: List[String]): Queue = + def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String]) + : (List[String], Queue) = { - val selected_group = groups.toSet - val selected_name = names.toSet + sessions.filterNot(isDefinedAt(_)) match { + case Nil => + case bad => error("Undefined session(s): " + commas_quote(bad)) + } + val selected = - graph.keys.filter(name => - selected_name(name) || apply(name).groups.exists(selected_group)).toList - new Queue(graph.restrict(graph.all_preds(selected).toSet)) + { + if (all_sessions) graph.keys.toList + else { + val sel_group = session_groups.toSet + val sel = sessions.toSet + graph.keys.toList.filter(name => + sel(name) || apply(name).groups.exists(sel_group)).toList + } + } + val descendants = graph.all_succs(selected) + val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet)) + (descendants, queue1) } def dequeue(skip: String => Boolean): Option[(String, Info)] = @@ -83,7 +96,7 @@ } def topological_order: List[(String, Info)] = - graph.topological_order.map(name => (name, graph.get_node(name))) + graph.topological_order.map(name => (name, apply(name))) } } @@ -232,8 +245,7 @@ }) } - def find_sessions(options: Options, more_dirs: List[Path], - all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue = + def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue = { var queue = Session.Queue.empty @@ -246,12 +258,7 @@ for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue) - sessions.filter(name => !queue.isDefinedAt(name)) match { - case Nil => - case bad => error("Undefined session(s): " + commas_quote(bad)) - } - - if (all_sessions) queue else queue.required(session_groups, sessions) + queue } @@ -439,6 +446,7 @@ def build( all_sessions: Boolean = false, build_heap: Boolean = false, + clean_build: Boolean = false, more_dirs: List[Path] = Nil, session_groups: List[String] = Nil, max_jobs: Int = 1, @@ -449,7 +457,8 @@ sessions: List[String] = Nil): Int = { val options = (Options.init() /: build_options)(_.define_simple(_)) - val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions) + val (descendants, queue) = + find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions) val deps = dependencies(verbose, queue) def make_stamp(name: String): String = @@ -469,6 +478,16 @@ // prepare log dir (output_dir + LOG).file.mkdirs() + // optional cleanup + if (clean_build) { + for (name <- descendants) { + val files = + List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file) + if (!files.isEmpty) echo("Cleaning " + name + " ...") + if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete") + } + } + // scheduler loop @tailrec def loop( pending: Session.Queue, @@ -571,13 +590,14 @@ case Properties.Value.Boolean(all_sessions) :: Properties.Value.Boolean(build_heap) :: + Properties.Value.Boolean(clean_build) :: Properties.Value.Int(max_jobs) :: Properties.Value.Boolean(no_build) :: Properties.Value.Boolean(system_mode) :: Properties.Value.Boolean(verbose) :: Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) => - build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups, - max_jobs, no_build, build_options, system_mode, verbose, sessions) + build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode), + session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions) case _ => error("Bad arguments:\n" + cat_lines(args)) } }