--- a/NEWS Sun Oct 01 12:28:52 2017 +0200
+++ b/NEWS Sun Oct 01 13:07:31 2017 +0200
@@ -27,6 +27,9 @@
* Windows and Cygwin is for x86_64 only. Old 32bit platform support has
been discontinued.
+* Command-line tool "isabelle build" supports option -B for base
+sessions: all descendants are included.
+
New in Isabelle2017 (October 2017)
----------------------------------
--- a/src/Doc/System/Sessions.thy Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Doc/System/Sessions.thy Sun Oct 01 13:07:31 2017 +0200
@@ -280,6 +280,7 @@
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
+ -B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
-R operate on requirements of selected sessions
@@ -329,6 +330,10 @@
completed by including all ancestors.
\<^medskip>
+ One or more options \<^verbatim>\<open>-B\<close>~\<open>NAME\<close> specify base sessions. All descendants
+ are included.
+
+ \<^medskip>
One or more options \<^verbatim>\<open>-x\<close>~\<open>NAME\<close> specify sessions to be excluded. All
descendents of excluded sessions are removed from the selection as specified
above. Option \<^verbatim>\<open>-X\<close> is analogous to this, but excluded sessions are
@@ -450,6 +455,7 @@
\<open>Usage: isabelle imports [OPTIONS] [SESSIONS ...]
Options are:
+ -B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-I operation: report potential session imports
-M operation: Mercurial repository check for theory files
@@ -469,7 +475,7 @@
\<^medskip>
The selection of sessions and session directories works as for @{tool build}
- 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
+ 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
\secref{sec:tool-build}).
\<^medskip>
--- a/src/Pure/Thy/sessions.scala Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sun Oct 01 13:07:31 2017 +0200
@@ -368,6 +368,7 @@
sealed case class Selection(
requirements: Boolean = false,
all_sessions: Boolean = false,
+ base_sessions: List[String] = Nil,
exclude_session_groups: List[String] = Nil,
exclude_sessions: List[String] = Nil,
session_groups: List[String] = Nil,
@@ -377,6 +378,7 @@
Selection(
requirements = requirements || other.requirements,
all_sessions = all_sessions || other.all_sessions,
+ base_sessions = Library.merge(base_sessions, other.base_sessions),
exclude_session_groups = Library.merge(exclude_session_groups, other.exclude_session_groups),
exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
session_groups = Library.merge(session_groups, other.session_groups),
@@ -385,8 +387,10 @@
def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
{
val bad_sessions =
- SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
- if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
+ SortedSet((base_sessions ::: exclude_sessions ::: sessions).
+ filterNot(graph.defined(_)): _*).toList
+ if (bad_sessions.nonEmpty)
+ error("Undefined session(s): " + commas_quote(bad_sessions))
val excluded =
{
@@ -404,7 +408,7 @@
if (all_sessions) graph.keys
else {
val select_group = session_groups.toSet
- val select = sessions.toSet
+ val select = sessions.toSet ++ graph.all_succs(base_sessions)
(for {
(name, (info, _)) <- graph.iterator
if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
--- a/src/Pure/Tools/build.scala Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Pure/Tools/build.scala Sun Oct 01 13:07:31 2017 +0200
@@ -357,6 +357,7 @@
pide: Boolean = false,
requirements: Boolean = false,
all_sessions: Boolean = false,
+ base_sessions: List[String] = Nil,
exclude_session_groups: List[String] = Nil,
exclude_sessions: List[String] = Nil,
session_groups: List[String] = Nil,
@@ -371,7 +372,7 @@
val (selected, selected_sessions) =
full_sessions.selection(
- Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+ Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
exclude_sessions, session_groups, sessions) ++ selection)
val deps =
@@ -627,6 +628,7 @@
{
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+ var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
var pide = false
@@ -650,6 +652,7 @@
Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
+ -B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-N cyclic shuffling of NUMA CPU nodes (performance tuning)
-P build via PIDE protocol
@@ -672,6 +675,7 @@
Build and manage Isabelle sessions, depending on implicit settings:
""" + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n",
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),
"P" -> (_ => pide = true),
@@ -722,6 +726,7 @@
pide = pide,
requirements = requirements,
all_sessions = all_sessions,
+ base_sessions = base_sessions,
exclude_session_groups = exclude_session_groups,
exclude_sessions = exclude_sessions,
session_groups = session_groups,
--- a/src/Pure/Tools/imports.scala Sun Oct 01 12:28:52 2017 +0200
+++ b/src/Pure/Tools/imports.scala Sun Oct 01 13:07:31 2017 +0200
@@ -215,6 +215,7 @@
val isabelle_tool =
Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
{
+ var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var operation_imports = false
var operation_repository_files = false
@@ -233,6 +234,7 @@
Usage: isabelle imports [OPTIONS] [SESSIONS ...]
Options are:
+ -B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
-I operation: report potential session imports
-M operation: Mercurial repository check for theory files
@@ -250,6 +252,7 @@
Maintain theory imports wrt. session structure. At least one operation
needs to be specified (see options -I -M -U).
""",
+ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"I" -> (_ => operation_imports = true),
"M" -> (_ => operation_repository_files = true),
@@ -269,7 +272,7 @@
getopts.usage()
val selection =
- Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+ Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
exclude_sessions, session_groups, sessions)
val progress = new Console_Progress(verbose = verbose)