added build option -c;
authorwenzelm
Mon Jul 30 12:03:48 2012 +0200 (2012-07-30)
changeset 48595231e6fa96dbb
parent 48594 c24907e5081e
child 48597 4b8559b227ed
added build option -c;
tuned;
doc-src/System/Thy/Sessions.thy
doc-src/System/Thy/document/Sessions.tex
lib/Tools/build
src/Pure/System/build.scala
     1.1 --- a/doc-src/System/Thy/Sessions.thy	Mon Jul 30 11:03:44 2012 +0200
     1.2 +++ b/doc-src/System/Thy/Sessions.thy	Mon Jul 30 12:03:48 2012 +0200
     1.3 @@ -167,6 +167,7 @@
     1.4    Options are:
     1.5      -a           select all sessions
     1.6      -b           build heap images
     1.7 +    -c           clean build
     1.8      -d DIR       include session directory with ROOT file
     1.9      -g NAME      select session group NAME
    1.10      -j INT       maximum number of parallel jobs (default 1)
    1.11 @@ -221,6 +222,14 @@
    1.12    saved for inner nodes of the hierarchy of sessions, as required for
    1.13    other sessions to continue later on.
    1.14  
    1.15 +  \medskip Option @{verbatim "-c"} cleans all descendants of the
    1.16 +  selected sessions before performing the specified build operation.
    1.17 +
    1.18 +  \medskip Option @{verbatim "-n"} omits the actual build process
    1.19 +  after the preparatory stage (including optional cleanup).  Note that
    1.20 +  the return code always indicates the status of the set of selected
    1.21 +  sessions.
    1.22 +
    1.23    \medskip Option @{verbatim "-j"} specifies the maximum number of
    1.24    parallel build jobs (prover processes).  Note that each process is
    1.25    subject to a separate limit of parallel threads, cf.\ system option
    1.26 @@ -232,10 +241,6 @@
    1.27    @{setting ISABELLE_OUTPUT} (which is normally in @{setting
    1.28    ISABELLE_HOME_USER}, i.e.\ the user's home directory).
    1.29  
    1.30 -  \medskip Option @{verbatim "-n"} omits the actual build process
    1.31 -  after performing all dependency checks.  The return code indicates
    1.32 -  the status of the set of selected sessions.
    1.33 -
    1.34    \medskip Option @{verbatim "-v"} enables verbose mode.
    1.35  *}
    1.36  
    1.37 @@ -247,30 +252,40 @@
    1.38  isabelle build -b HOLCF
    1.39  \end{ttbox}
    1.40  
    1.41 -  Build the main group of logic images (as determined by the session
    1.42 -  ROOT specifications of the Isabelle distribution):
    1.43 +  \smallskip Build the main group of logic images (as determined by
    1.44 +  the session ROOT specifications of the Isabelle distribution):
    1.45  \begin{ttbox}
    1.46  isabelle build -b -g main
    1.47  \end{ttbox}
    1.48  
    1.49 -  Provide a general overview of the status of all Isabelle sessions,
    1.50 -  without building anything:
    1.51 +  \smallskip Provide a general overview of the status of all Isabelle
    1.52 +  sessions, without building anything:
    1.53  \begin{ttbox}
    1.54  isabelle build -a -n -v
    1.55  \end{ttbox}
    1.56  
    1.57 -  Build all sessions with HTML browser info and PDF document
    1.58 -  preparation:
    1.59 +  \smallskip Build all sessions with HTML browser info and PDF
    1.60 +  document preparation:
    1.61  \begin{ttbox}
    1.62  isabelle build -a -o browser_info -o document=pdf
    1.63  \end{ttbox}
    1.64  
    1.65 -  Build all sessions with a maximum of 8 prover processes and 4
    1.66 -  threads each (on a machine with many cores):
    1.67 -
    1.68 +  \smallskip Build all sessions with a maximum of 8 prover processes
    1.69 +  and 4 threads each (on a machine with many cores):
    1.70  \begin{ttbox}
    1.71  isabelle build -a -j8 -o threads=4
    1.72  \end{ttbox}
    1.73 +
    1.74 +  \smallskip Build some session images with cleanup of their
    1.75 +  descendants, while retaining their ancestry:
    1.76 +\begin{ttbox}
    1.77 +isabelle build -b -c HOL-Boogie HOL-SPARK
    1.78 +\end{ttbox}
    1.79 +
    1.80 +  \smallskip Clean all sessions without building anything:
    1.81 +\begin{ttbox}
    1.82 +isabelle build -a -n -c
    1.83 +\end{ttbox}
    1.84  *}
    1.85  
    1.86  end
     2.1 --- a/doc-src/System/Thy/document/Sessions.tex	Mon Jul 30 11:03:44 2012 +0200
     2.2 +++ b/doc-src/System/Thy/document/Sessions.tex	Mon Jul 30 12:03:48 2012 +0200
     2.3 @@ -277,6 +277,7 @@
     2.4    Options are:
     2.5      -a           select all sessions
     2.6      -b           build heap images
     2.7 +    -c           clean build
     2.8      -d DIR       include session directory with ROOT file
     2.9      -g NAME      select session group NAME
    2.10      -j INT       maximum number of parallel jobs (default 1)
    2.11 @@ -327,6 +328,14 @@
    2.12    saved for inner nodes of the hierarchy of sessions, as required for
    2.13    other sessions to continue later on.
    2.14  
    2.15 +  \medskip Option \verb|-c| cleans all descendants of the
    2.16 +  selected sessions before performing the specified build operation.
    2.17 +
    2.18 +  \medskip Option \verb|-n| omits the actual build process
    2.19 +  after the preparatory stage (including optional cleanup).  Note that
    2.20 +  the return code always indicates the status of the set of selected
    2.21 +  sessions.
    2.22 +
    2.23    \medskip Option \verb|-j| specifies the maximum number of
    2.24    parallel build jobs (prover processes).  Note that each process is
    2.25    subject to a separate limit of parallel threads, cf.\ system option
    2.26 @@ -337,10 +346,6 @@
    2.27    \verb|$ISABELLE_HOME/heaps| instead of the default location
    2.28    \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).
    2.29  
    2.30 -  \medskip Option \verb|-n| omits the actual build process
    2.31 -  after performing all dependency checks.  The return code indicates
    2.32 -  the status of the set of selected sessions.
    2.33 -
    2.34    \medskip Option \verb|-v| enables verbose mode.%
    2.35  \end{isamarkuptext}%
    2.36  \isamarkuptrue%
    2.37 @@ -355,29 +360,39 @@
    2.38  isabelle build -b HOLCF
    2.39  \end{ttbox}
    2.40  
    2.41 -  Build the main group of logic images (as determined by the session
    2.42 -  ROOT specifications of the Isabelle distribution):
    2.43 +  \smallskip Build the main group of logic images (as determined by
    2.44 +  the session ROOT specifications of the Isabelle distribution):
    2.45  \begin{ttbox}
    2.46  isabelle build -b -g main
    2.47  \end{ttbox}
    2.48  
    2.49 -  Provide a general overview of the status of all Isabelle sessions,
    2.50 -  without building anything:
    2.51 +  \smallskip Provide a general overview of the status of all Isabelle
    2.52 +  sessions, without building anything:
    2.53  \begin{ttbox}
    2.54  isabelle build -a -n -v
    2.55  \end{ttbox}
    2.56  
    2.57 -  Build all sessions with HTML browser info and PDF document
    2.58 -  preparation:
    2.59 +  \smallskip Build all sessions with HTML browser info and PDF
    2.60 +  document preparation:
    2.61  \begin{ttbox}
    2.62  isabelle build -a -o browser_info -o document=pdf
    2.63  \end{ttbox}
    2.64  
    2.65 -  Build all sessions with a maximum of 8 prover processes and 4
    2.66 -  threads each (on a machine with many cores):
    2.67 -
    2.68 +  \smallskip Build all sessions with a maximum of 8 prover processes
    2.69 +  and 4 threads each (on a machine with many cores):
    2.70  \begin{ttbox}
    2.71  isabelle build -a -j8 -o threads=4
    2.72 +\end{ttbox}
    2.73 +
    2.74 +  \smallskip Build some session images with cleanup of their
    2.75 +  descendants, while retaining their ancestry:
    2.76 +\begin{ttbox}
    2.77 +isabelle build -b -c HOL-Boogie HOL-SPARK
    2.78 +\end{ttbox}
    2.79 +
    2.80 +  \smallskip Clean all sessions without building anything:
    2.81 +\begin{ttbox}
    2.82 +isabelle build -a -n -c
    2.83  \end{ttbox}%
    2.84  \end{isamarkuptext}%
    2.85  \isamarkuptrue%
     3.1 --- a/lib/Tools/build	Mon Jul 30 11:03:44 2012 +0200
     3.2 +++ b/lib/Tools/build	Mon Jul 30 12:03:48 2012 +0200
     3.3 @@ -28,6 +28,7 @@
     3.4    echo "  Options are:"
     3.5    echo "    -a           select all sessions"
     3.6    echo "    -b           build heap images"
     3.7 +  echo "    -c           clean build"
     3.8    echo "    -d DIR       include session directory with ROOT file"
     3.9    echo "    -g NAME      select session group NAME"
    3.10    echo "    -j INT       maximum number of parallel jobs (default 1)"
    3.11 @@ -58,6 +59,7 @@
    3.12  
    3.13  ALL_SESSIONS=false
    3.14  BUILD_HEAP=false
    3.15 +CLEAN_BUILD=false
    3.16  declare -a MORE_DIRS=()
    3.17  declare -a SESSION_GROUPS=()
    3.18  MAX_JOBS=1
    3.19 @@ -66,7 +68,7 @@
    3.20  SYSTEM_MODE=false
    3.21  VERBOSE=false
    3.22  
    3.23 -while getopts "abd:g:j:no:sv" OPT
    3.24 +while getopts "abcd:g:j:no:sv" OPT
    3.25  do
    3.26    case "$OPT" in
    3.27      a)
    3.28 @@ -75,6 +77,9 @@
    3.29      b)
    3.30        BUILD_HEAP="true"
    3.31        ;;
    3.32 +    c)
    3.33 +      CLEAN_BUILD="true"
    3.34 +      ;;
    3.35      d)
    3.36        MORE_DIRS["${#MORE_DIRS[@]}"]="$OPTARG"
    3.37        ;;
    3.38 @@ -121,7 +126,8 @@
    3.39  fi
    3.40  
    3.41  "$ISABELLE_TOOL" java isabelle.Build \
    3.42 -  "$ALL_SESSIONS" "$BUILD_HEAP" "$MAX_JOBS" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    3.43 +  "$ALL_SESSIONS" "$BUILD_HEAP" "$CLEAN_BUILD" "$MAX_JOBS" \
    3.44 +  "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    3.45    "${MORE_DIRS[@]}" $'\n' "${SESSION_GROUPS[@]}" $'\n' "${BUILD_OPTIONS[@]}" $'\n' "$@"
    3.46  RC="$?"
    3.47  
     4.1 --- a/src/Pure/System/build.scala	Mon Jul 30 11:03:44 2012 +0200
     4.2 +++ b/src/Pure/System/build.scala	Mon Jul 30 12:03:48 2012 +0200
     4.3 @@ -64,14 +64,27 @@
     4.4  
     4.5        def - (name: String): Queue = new Queue(graph.del_node(name))
     4.6  
     4.7 -      def required(groups: List[String], names: List[String]): Queue =
     4.8 +      def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
     4.9 +        : (List[String], Queue) =
    4.10        {
    4.11 -        val selected_group = groups.toSet
    4.12 -        val selected_name = names.toSet
    4.13 +        sessions.filterNot(isDefinedAt(_)) match {
    4.14 +          case Nil =>
    4.15 +          case bad => error("Undefined session(s): " + commas_quote(bad))
    4.16 +        }
    4.17 +
    4.18          val selected =
    4.19 -          graph.keys.filter(name =>
    4.20 -            selected_name(name) || apply(name).groups.exists(selected_group)).toList
    4.21 -        new Queue(graph.restrict(graph.all_preds(selected).toSet))
    4.22 +        {
    4.23 +          if (all_sessions) graph.keys.toList
    4.24 +          else {
    4.25 +            val sel_group = session_groups.toSet
    4.26 +            val sel = sessions.toSet
    4.27 +              graph.keys.toList.filter(name =>
    4.28 +                sel(name) || apply(name).groups.exists(sel_group)).toList
    4.29 +          }
    4.30 +        }
    4.31 +        val descendants = graph.all_succs(selected)
    4.32 +        val queue1 = new Queue(graph.restrict(graph.all_preds(selected).toSet))
    4.33 +        (descendants, queue1)
    4.34        }
    4.35  
    4.36        def dequeue(skip: String => Boolean): Option[(String, Info)] =
    4.37 @@ -83,7 +96,7 @@
    4.38        }
    4.39  
    4.40        def topological_order: List[(String, Info)] =
    4.41 -        graph.topological_order.map(name => (name, graph.get_node(name)))
    4.42 +        graph.topological_order.map(name => (name, apply(name)))
    4.43      }
    4.44    }
    4.45  
    4.46 @@ -232,8 +245,7 @@
    4.47        })
    4.48    }
    4.49  
    4.50 -  def find_sessions(options: Options, more_dirs: List[Path],
    4.51 -    all_sessions: Boolean, session_groups: List[String], sessions: List[String]): Session.Queue =
    4.52 +  def find_sessions(options: Options, more_dirs: List[Path]): Session.Queue =
    4.53    {
    4.54      var queue = Session.Queue.empty
    4.55  
    4.56 @@ -246,12 +258,7 @@
    4.57  
    4.58      for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
    4.59  
    4.60 -    sessions.filter(name => !queue.isDefinedAt(name)) match {
    4.61 -      case Nil =>
    4.62 -      case bad => error("Undefined session(s): " + commas_quote(bad))
    4.63 -    }
    4.64 -
    4.65 -    if (all_sessions) queue else queue.required(session_groups, sessions)
    4.66 +    queue
    4.67    }
    4.68  
    4.69  
    4.70 @@ -439,6 +446,7 @@
    4.71    def build(
    4.72      all_sessions: Boolean = false,
    4.73      build_heap: Boolean = false,
    4.74 +    clean_build: Boolean = false,
    4.75      more_dirs: List[Path] = Nil,
    4.76      session_groups: List[String] = Nil,
    4.77      max_jobs: Int = 1,
    4.78 @@ -449,7 +457,8 @@
    4.79      sessions: List[String] = Nil): Int =
    4.80    {
    4.81      val options = (Options.init() /: build_options)(_.define_simple(_))
    4.82 -    val queue = find_sessions(options, more_dirs, all_sessions, session_groups, sessions)
    4.83 +    val (descendants, queue) =
    4.84 +      find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
    4.85      val deps = dependencies(verbose, queue)
    4.86  
    4.87      def make_stamp(name: String): String =
    4.88 @@ -469,6 +478,16 @@
    4.89      // prepare log dir
    4.90      (output_dir + LOG).file.mkdirs()
    4.91  
    4.92 +    // optional cleanup
    4.93 +    if (clean_build) {
    4.94 +      for (name <- descendants) {
    4.95 +        val files =
    4.96 +          List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
    4.97 +        if (!files.isEmpty) echo("Cleaning " + name + " ...")
    4.98 +        if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
    4.99 +      }
   4.100 +    }
   4.101 +
   4.102      // scheduler loop
   4.103      @tailrec def loop(
   4.104        pending: Session.Queue,
   4.105 @@ -571,13 +590,14 @@
   4.106          case
   4.107            Properties.Value.Boolean(all_sessions) ::
   4.108            Properties.Value.Boolean(build_heap) ::
   4.109 +          Properties.Value.Boolean(clean_build) ::
   4.110            Properties.Value.Int(max_jobs) ::
   4.111            Properties.Value.Boolean(no_build) ::
   4.112            Properties.Value.Boolean(system_mode) ::
   4.113            Properties.Value.Boolean(verbose) ::
   4.114            Command_Line.Chunks(more_dirs, session_groups, build_options, sessions) =>
   4.115 -            build(all_sessions, build_heap, more_dirs.map(Path.explode), session_groups,
   4.116 -              max_jobs, no_build, build_options, system_mode, verbose, sessions)
   4.117 +            build(all_sessions, build_heap, clean_build, more_dirs.map(Path.explode),
   4.118 +              session_groups, max_jobs, no_build, build_options, system_mode, verbose, sessions)
   4.119          case _ => error("Bad arguments:\n" + cat_lines(args))
   4.120        }
   4.121      }