added build schedule command-line wrapper;
authorFabian Huch <huch@in.tum.de>
Wed, 06 Dec 2023 18:28:15 +0100
changeset 79182 6202d0ff36b4
parent 79181 9d6d559c9fde
child 79183 32d00ec387f4
added build schedule command-line wrapper;
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/build_schedule.scala
--- 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)
+    })
 }