--- a/src/Pure/System/isabelle_tool.scala Wed Dec 06 18:18:56 2023 +0100
+++ b/src/Pure/System/isabelle_tool.scala Wed Dec 06 18:28:15 2023 +0100
@@ -125,6 +125,7 @@
Build.isabelle_tool2,
Build.isabelle_tool3,
Build.isabelle_tool4,
+ Build_Schedule.isabelle_tool,
CI_Build.isabelle_tool,
Doc.isabelle_tool,
Docker_Build.isabelle_tool,
--- a/src/Pure/Tools/build_schedule.scala Wed Dec 06 18:18:56 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala Wed Dec 06 18:28:15 2023 +0100
@@ -8,6 +8,7 @@
import Host.Node_Info
import scala.annotation.tailrec
+import scala.collection.mutable
object Build_Schedule {
@@ -1202,4 +1203,86 @@
else if (File.is_pdf(name)) Graphics_File.write_pdf(output.file, paint, width, height)
else error("Bad type of file: " + quote(name) + " (.png or .pdf expected)")
}
+
+
+ /* command-line wrapper */
+
+ val isabelle_tool = Isabelle_Tool("build_schedule", "generate build schedule", Scala_Project.here,
+ { args =>
+ var afp_root: Option[Path] = None
+ val base_sessions = new mutable.ListBuffer[String]
+ val select_dirs = new mutable.ListBuffer[Path]
+ val build_hosts = new mutable.ListBuffer[Build_Cluster.Host]
+ var numa_shuffling = false
+ var output_file: Option[Path] = None
+ var requirements = false
+ val exclude_session_groups = new mutable.ListBuffer[String]
+ var all_sessions = false
+ val dirs = new mutable.ListBuffer[Path]
+ val session_groups = new mutable.ListBuffer[String]
+ var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
+ var verbose = false
+ val exclude_sessions = new mutable.ListBuffer[String]
+
+ val getopts = Getopts("""
+Usage: isabelle build_schedule [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -A ROOT include AFP with given root directory (":" for """ + AFP.BASE.implode + """)
+ -B NAME include session NAME and all descendants
+ -D DIR include session directory and select its sessions
+ -H HOSTS additional build cluster host specifications, of the form
+ "NAMES:PARAMETERS" (separated by commas)
+ -N cyclic shuffling of NUMA CPU nodes (performance tuning)
+ -O FILE output file
+ -R refer to requirements of selected sessions
+ -X NAME exclude sessions from group NAME and all descendants
+ -a select all sessions
+ -d DIR include session directory
+ -g NAME select session group NAME
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose
+ -x NAME exclude session NAME and all descendants
+
+ Generate build graph.
+""",
+ "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
+ "B:" -> (arg => base_sessions += arg),
+ "D:" -> (arg => select_dirs += Path.explode(arg)),
+ "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.global, arg)),
+ "N" -> (_ => numa_shuffling = true),
+ "O:" -> (arg => output_file = Some(Path.explode(arg))),
+ "R" -> (_ => requirements = true),
+ "X:" -> (arg => exclude_session_groups += arg),
+ "a" -> (_ => all_sessions = true),
+ "d:" -> (arg => dirs += Path.explode(arg)),
+ "g:" -> (arg => session_groups += arg),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions += arg))
+
+ val sessions = getopts(args)
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ val schedule =
+ build_schedule(options,
+ selection = Sessions.Selection(
+ requirements = requirements,
+ all_sessions = all_sessions,
+ base_sessions = base_sessions.toList,
+ exclude_session_groups = exclude_session_groups.toList,
+ exclude_sessions = exclude_sessions.toList,
+ session_groups = session_groups.toList,
+ sessions = sessions),
+ progress = progress,
+ afp_root = afp_root,
+ dirs = dirs.toList,
+ select_dirs = select_dirs.toList,
+ numa_shuffling = isabelle.Host.numa_check(progress, numa_shuffling),
+ build_hosts = build_hosts.toList)
+
+ if (!schedule.graph.is_empty && output_file.nonEmpty)
+ write_schedule_graphic(schedule, output_file.get)
+ })
}