option -B for "isabelle build" and "isabelle imports";
authorwenzelm
Sun Oct 01 13:07:31 2017 +0200 (18 months ago)
changeset 667372edc0c42c883
parent 66736 148891036469
child 66738 793e7a9c30c5
option -B for "isabelle build" and "isabelle imports";
NEWS
src/Doc/System/Sessions.thy
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/imports.scala
     1.1 --- a/NEWS	Sun Oct 01 12:28:52 2017 +0200
     1.2 +++ b/NEWS	Sun Oct 01 13:07:31 2017 +0200
     1.3 @@ -27,6 +27,9 @@
     1.4  * Windows and Cygwin is for x86_64 only. Old 32bit platform support has
     1.5  been discontinued.
     1.6  
     1.7 +* Command-line tool "isabelle build" supports option -B for base
     1.8 +sessions: all descendants are included.
     1.9 +
    1.10  
    1.11  New in Isabelle2017 (October 2017)
    1.12  ----------------------------------
     2.1 --- a/src/Doc/System/Sessions.thy	Sun Oct 01 12:28:52 2017 +0200
     2.2 +++ b/src/Doc/System/Sessions.thy	Sun Oct 01 13:07:31 2017 +0200
     2.3 @@ -280,6 +280,7 @@
     2.4  \<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
     2.5  
     2.6    Options are:
     2.7 +    -B NAME      include session NAME and all descendants
     2.8      -D DIR       include session directory and select its sessions
     2.9      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
    2.10      -R           operate on requirements of selected sessions
    2.11 @@ -329,6 +330,10 @@
    2.12    completed by including all ancestors.
    2.13  
    2.14    \<^medskip>
    2.15 +  One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
    2.16 +  are included.
    2.17 +
    2.18 +  \<^medskip>
    2.19    One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
    2.20    descendents of excluded sessions are removed from the selection as specified
    2.21    above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
    2.22 @@ -450,6 +455,7 @@
    2.23  \<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
    2.24  
    2.25    Options are:
    2.26 +    -B NAME      include session NAME and all descendants
    2.27      -D DIR       include session directory and select its sessions
    2.28      -I           operation: report potential session imports
    2.29      -M           operation: Mercurial repository check for theory files
    2.30 @@ -469,7 +475,7 @@
    2.31  
    2.32    \<^medskip>
    2.33    The selection of sessions and session directories works as for @{tool build}
    2.34 -  via options \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
    2.35 +  via options \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-D\<close>, \<^verbatim>\<open>-R\<close>, \<^verbatim>\<open>-X\<close>, \<^verbatim>\<open>-a\<close>, \<^verbatim>\<open>-d\<close>, \<^verbatim>\<open>-g\<close>, \<^verbatim>\<open>-x\<close> (see
    2.36    \secref{sec:tool-build}).
    2.37  
    2.38    \<^medskip>
     3.1 --- a/src/Pure/Thy/sessions.scala	Sun Oct 01 12:28:52 2017 +0200
     3.2 +++ b/src/Pure/Thy/sessions.scala	Sun Oct 01 13:07:31 2017 +0200
     3.3 @@ -368,6 +368,7 @@
     3.4    sealed case class Selection(
     3.5      requirements: Boolean = false,
     3.6      all_sessions: Boolean = false,
     3.7 +    base_sessions: List[String] = Nil,
     3.8      exclude_session_groups: List[String] = Nil,
     3.9      exclude_sessions: List[String] = Nil,
    3.10      session_groups: List[String] = Nil,
    3.11 @@ -377,6 +378,7 @@
    3.12        Selection(
    3.13          requirements = requirements || other.requirements,
    3.14          all_sessions = all_sessions || other.all_sessions,
    3.15 +        base_sessions = Library.merge(base_sessions, other.base_sessions),
    3.16          exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
    3.17          exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
    3.18          session_groups = Library.merge(session_groups, other.session_groups),
    3.19 @@ -385,8 +387,10 @@
    3.20      def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
    3.21      {
    3.22        val bad_sessions =
    3.23 -        SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
    3.24 -      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    3.25 +        SortedSet((base_sessions ::: exclude_sessions ::: sessions).
    3.26 +          filterNot(graph.defined(_)): _*).toList
    3.27 +      if (bad_sessions.nonEmpty)
    3.28 +        error("Undefined session(s): " + commas_quote(bad_sessions))
    3.29  
    3.30        val excluded =
    3.31        {
    3.32 @@ -404,7 +408,7 @@
    3.33          if (all_sessions) graph.keys
    3.34          else {
    3.35            val select_group = session_groups.toSet
    3.36 -          val select = sessions.toSet
    3.37 +          val select = sessions.toSet ++ graph.all_succs(base_sessions)
    3.38            (for {
    3.39              (name, (info, _)) <- graph.iterator
    3.40              if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
     4.1 --- a/src/Pure/Tools/build.scala	Sun Oct 01 12:28:52 2017 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Sun Oct 01 13:07:31 2017 +0200
     4.3 @@ -357,6 +357,7 @@
     4.4      pide: Boolean = false,
     4.5      requirements: Boolean = false,
     4.6      all_sessions: Boolean = false,
     4.7 +    base_sessions: List[String] = Nil,
     4.8      exclude_session_groups: List[String] = Nil,
     4.9      exclude_sessions: List[String] = Nil,
    4.10      session_groups: List[String] = Nil,
    4.11 @@ -371,7 +372,7 @@
    4.12  
    4.13      val (selected, selected_sessions) =
    4.14        full_sessions.selection(
    4.15 -          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
    4.16 +          Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    4.17              exclude_sessions, session_groups, sessions) ++ selection)
    4.18  
    4.19      val deps =
    4.20 @@ -627,6 +628,7 @@
    4.21    {
    4.22      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
    4.23  
    4.24 +    var base_sessions: List[String] = Nil
    4.25      var select_dirs: List[Path] = Nil
    4.26      var numa_shuffling = false
    4.27      var pide = false
    4.28 @@ -650,6 +652,7 @@
    4.29  Usage: isabelle build [OPTIONS] [SESSIONS ...]
    4.30  
    4.31    Options are:
    4.32 +    -B NAME      include session NAME and all descendants
    4.33      -D DIR       include session directory and select its sessions
    4.34      -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
    4.35      -P           build via PIDE protocol
    4.36 @@ -672,6 +675,7 @@
    4.37    Build and manage Isabelle sessions, depending on implicit settings:
    4.38  
    4.39  """ + Library.prefix_lines("  ", Build_Log.Settings.show()) + "\n",
    4.40 +      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
    4.41        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    4.42        "N" -> (_ => numa_shuffling = true),
    4.43        "P" -> (_ => pide = true),
    4.44 @@ -722,6 +726,7 @@
    4.45            pide = pide,
    4.46            requirements = requirements,
    4.47            all_sessions = all_sessions,
    4.48 +          base_sessions = base_sessions,
    4.49            exclude_session_groups = exclude_session_groups,
    4.50            exclude_sessions = exclude_sessions,
    4.51            session_groups = session_groups,
     5.1 --- a/src/Pure/Tools/imports.scala	Sun Oct 01 12:28:52 2017 +0200
     5.2 +++ b/src/Pure/Tools/imports.scala	Sun Oct 01 13:07:31 2017 +0200
     5.3 @@ -215,6 +215,7 @@
     5.4    val isabelle_tool =
     5.5      Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
     5.6      {
     5.7 +      var base_sessions: List[String] = Nil
     5.8        var select_dirs: List[Path] = Nil
     5.9        var operation_imports = false
    5.10        var operation_repository_files = false
    5.11 @@ -233,6 +234,7 @@
    5.12  Usage: isabelle imports [OPTIONS] [SESSIONS ...]
    5.13  
    5.14    Options are:
    5.15 +    -B NAME      include session NAME and all descendants
    5.16      -D DIR       include session directory and select its sessions
    5.17      -I           operation: report potential session imports
    5.18      -M           operation: Mercurial repository check for theory files
    5.19 @@ -250,6 +252,7 @@
    5.20    Maintain theory imports wrt. session structure. At least one operation
    5.21    needs to be specified (see options -I -M -U).
    5.22  """,
    5.23 +      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
    5.24        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    5.25        "I" -> (_ => operation_imports = true),
    5.26        "M" -> (_ => operation_repository_files = true),
    5.27 @@ -269,7 +272,7 @@
    5.28          getopts.usage()
    5.29  
    5.30        val selection =
    5.31 -        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
    5.32 +        Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    5.33            exclude_sessions, session_groups, sessions)
    5.34  
    5.35        val progress = new Console_Progress(verbose = verbose)