added isabelle build option -x, to exclude sessions;
authorwenzelm
Wed Apr 01 16:24:38 2015 +0200 (2015-04-01)
changeset 598922a616319c171
parent 59891 9ce697050455
child 59893 89f3bd11fa8b
added isabelle build option -x, to exclude sessions;
NEWS
lib/Tools/build
src/Doc/System/Sessions.thy
src/Pure/PIDE/batch_session.scala
src/Pure/Tools/build.scala
     1.1 --- a/NEWS	Wed Apr 01 15:41:08 2015 +0200
     1.2 +++ b/NEWS	Wed Apr 01 16:24:38 2015 +0200
     1.3 @@ -396,7 +396,7 @@
     1.4  * The Isabelle tool "update_cartouches" changes theory files to use
     1.5  cartouches instead of old-style {* verbatim *} or `alt_string` tokens.
     1.6  
     1.7 -* The Isabelle tool "build" provides new option -k.
     1.8 +* The Isabelle tool "build" provides new options -k and -x.
     1.9  
    1.10  
    1.11  
     2.1 --- a/lib/Tools/build	Wed Apr 01 15:41:08 2015 +0200
     2.2 +++ b/lib/Tools/build	Wed Apr 01 16:24:38 2015 +0200
     2.3 @@ -40,6 +40,7 @@
     2.4    echo "    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)"
     2.5    echo "    -s           system build mode: produce output in ISABELLE_HOME"
     2.6    echo "    -v           verbose"
     2.7 +  echo "    -x SESSION   exclude SESSION and all its descendants"
     2.8    echo
     2.9    echo "  Build and manage Isabelle sessions, depending on implicit"
    2.10    show_settings "  "
    2.11 @@ -75,8 +76,9 @@
    2.12  eval "declare -a BUILD_OPTIONS=($ISABELLE_BUILD_OPTIONS)"
    2.13  SYSTEM_MODE=false
    2.14  VERBOSE=false
    2.15 +declare -a EXCLUDE_SESSIONS=()
    2.16  
    2.17 -while getopts "D:Rabcd:g:j:k:lno:sv" OPT
    2.18 +while getopts "D:Rabcd:g:j:k:lno:svx:" OPT
    2.19  do
    2.20    case "$OPT" in
    2.21      D)
    2.22 @@ -122,6 +124,9 @@
    2.23      v)
    2.24        VERBOSE="true"
    2.25        ;;
    2.26 +    x)
    2.27 +      EXCLUDE_SESSIONS["${#EXCLUDE_SESSIONS[@]}"]="$OPTARG"
    2.28 +      ;;
    2.29      \?)
    2.30        usage
    2.31        ;;
    2.32 @@ -151,7 +156,7 @@
    2.33    "$LIST_FILES" "$NO_BUILD" "$SYSTEM_MODE" "$VERBOSE" \
    2.34    "${INCLUDE_DIRS[@]}" $'\n' "${SELECT_DIRS[@]}" $'\n' \
    2.35    "${SESSION_GROUPS[@]}" $'\n' "${CHECK_KEYWORDS[@]}" $'\n' \
    2.36 -  "${BUILD_OPTIONS[@]}" $'\n' "$@"
    2.37 +  "${BUILD_OPTIONS[@]}" $'\n' "${EXCLUDE_SESSIONS[@]}" $'\n' "$@"
    2.38  RC="$?"
    2.39  
    2.40  if [ "$NO_BUILD" = false -a "$VERBOSE" = true ]; then
     3.1 --- a/src/Doc/System/Sessions.thy	Wed Apr 01 15:41:08 2015 +0200
     3.2 +++ b/src/Doc/System/Sessions.thy	Wed Apr 01 16:24:38 2015 +0200
     3.3 @@ -290,6 +290,7 @@
     3.4      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     3.5      -s           system build mode: produce output in ISABELLE_HOME
     3.6      -v           verbose
     3.7 +    -x SESSION   exclude SESSION and all its descendants
     3.8  
     3.9    Build and manage Isabelle sessions, depending on implicit
    3.10    ISABELLE_BUILD_OPTIONS="..."
    3.11 @@ -322,6 +323,10 @@
    3.12    The build tool takes session dependencies into account: the set of
    3.13    selected sessions is completed by including all ancestors.
    3.14  
    3.15 +  \medskip One or more options @{verbatim "-x"}~@{text SESSION} specify
    3.16 +  sessions to be excluded. All descendents of excluded sessions are removed
    3.17 +  from the selection as specified above.
    3.18 +
    3.19    \medskip Option @{verbatim "-R"} reverses the selection in the sense
    3.20    that it refers to its requirements: all ancestor sessions excluding
    3.21    the original selection.  This allows to prepare the stage for some
     4.1 --- a/src/Pure/PIDE/batch_session.scala	Wed Apr 01 15:41:08 2015 +0200
     4.2 +++ b/src/Pure/PIDE/batch_session.scala	Wed Apr 01 16:24:38 2015 +0200
     4.3 @@ -19,7 +19,7 @@
     4.4      session: String): Batch_Session =
     4.5    {
     4.6      val (_, session_tree) =
     4.7 -      Build.find_sessions(options, dirs).selection(false, false, Nil, List(session))
     4.8 +      Build.find_sessions(options, dirs).selection(sessions = List(session))
     4.9      val session_info = session_tree(session)
    4.10      val parent_session =
    4.11        session_info.parent getOrElse error("No parent session for " + quote(session))
     5.1 --- a/src/Pure/Tools/build.scala	Wed Apr 01 15:41:08 2015 +0200
     5.2 +++ b/src/Pure/Tools/build.scala	Wed Apr 01 16:24:38 2015 +0200
     5.3 @@ -162,12 +162,18 @@
     5.4      def apply(name: String): Session_Info = graph.get_node(name)
     5.5      def isDefinedAt(name: String): Boolean = graph.defined(name)
     5.6  
     5.7 -    def selection(requirements: Boolean, all_sessions: Boolean,
     5.8 -      session_groups: List[String], sessions: List[String]): (List[String], Session_Tree) =
     5.9 +    def selection(
    5.10 +      requirements: Boolean = false,
    5.11 +      all_sessions: Boolean = false,
    5.12 +      session_groups: List[String] = Nil,
    5.13 +      exclude_sessions: List[String] = Nil,
    5.14 +      sessions: List[String] = Nil): (List[String], Session_Tree) =
    5.15      {
    5.16 -      val bad_sessions = sessions.filterNot(isDefinedAt(_))
    5.17 +      val bad_sessions =
    5.18 +        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
    5.19        if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    5.20  
    5.21 +      val excluded = graph.all_succs(exclude_sessions).toSet
    5.22        val pre_selected =
    5.23        {
    5.24          if (all_sessions) graph.keys
    5.25 @@ -179,7 +185,8 @@
    5.26              if info.select || select(name) || apply(name).groups.exists(select_group)
    5.27            } yield name).toList
    5.28          }
    5.29 -      }
    5.30 +      }.filterNot(excluded)
    5.31 +
    5.32        val selected =
    5.33          if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
    5.34          else pre_selected
    5.35 @@ -533,7 +540,7 @@
    5.36      dirs: List[Path],
    5.37      sessions: List[String]): Deps =
    5.38    {
    5.39 -    val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
    5.40 +    val (_, tree) = find_sessions(options, dirs = dirs).selection(sessions = sessions)
    5.41      dependencies(inlined_files = inlined_files, tree = tree)
    5.42    }
    5.43  
    5.44 @@ -758,13 +765,14 @@
    5.45      no_build: Boolean = false,
    5.46      system_mode: Boolean = false,
    5.47      verbose: Boolean = false,
    5.48 +    exclude_sessions: List[String] = Nil,
    5.49      sessions: List[String] = Nil): Map[String, Int] =
    5.50    {
    5.51      /* session tree and dependencies */
    5.52  
    5.53      val full_tree = find_sessions(options.int("completion_limit") = 0, dirs, select_dirs)
    5.54      val (selected, selected_tree) =
    5.55 -      full_tree.selection(requirements, all_sessions, session_groups, sessions)
    5.56 +      full_tree.selection(requirements, all_sessions, session_groups, exclude_sessions, sessions)
    5.57  
    5.58      val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
    5.59  
    5.60 @@ -1010,12 +1018,13 @@
    5.61      no_build: Boolean = false,
    5.62      system_mode: Boolean = false,
    5.63      verbose: Boolean = false,
    5.64 +    exclude_sessions: List[String] = Nil,
    5.65      sessions: List[String] = Nil): Int =
    5.66    {
    5.67      val results =
    5.68 -      build_results(options, progress, requirements, all_sessions,
    5.69 -        build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
    5.70 -        list_files, check_keywords, no_build, system_mode, verbose, sessions)
    5.71 +      build_results(options, progress, requirements, all_sessions, build_heap, clean_build,
    5.72 +        dirs, select_dirs, session_groups, max_jobs, list_files, check_keywords,
    5.73 +        no_build, system_mode, verbose, exclude_sessions, sessions)
    5.74  
    5.75      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
    5.76      if (rc != 0 && (verbose || !no_build)) {
    5.77 @@ -1043,15 +1052,15 @@
    5.78            Properties.Value.Boolean(no_build) ::
    5.79            Properties.Value.Boolean(system_mode) ::
    5.80            Properties.Value.Boolean(verbose) ::
    5.81 -          Command_Line.Chunks(
    5.82 -              dirs, select_dirs, session_groups, check_keywords, build_options, sessions) =>
    5.83 +          Command_Line.Chunks(dirs, select_dirs, session_groups, check_keywords,
    5.84 +              build_options, exclude_sessions, sessions) =>
    5.85              val options = (Options.init() /: build_options)(_ + _)
    5.86              val progress = new Console_Progress(verbose)
    5.87              progress.interrupt_handler {
    5.88                build(options, progress, requirements, all_sessions, build_heap, clean_build,
    5.89                  dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
    5.90                  max_jobs, list_files, check_keywords.toSet, no_build, system_mode,
    5.91 -                verbose, sessions)
    5.92 +                verbose, exclude_sessions, sessions)
    5.93              }
    5.94          case _ => error("Bad arguments:\n" + cat_lines(args))
    5.95        }