# HG changeset patch # User Fabian Huch # Date 1701883695 -3600 # Node ID 6202d0ff36b4e94f8d680e1be626e2e57b9914fd # Parent 9d6d559c9fde4df9c300bd8e2b0e180ce8a99424 added build schedule command-line wrapper; diff -r 9d6d559c9fde -r 6202d0ff36b4 src/Pure/System/isabelle_tool.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, diff -r 9d6d559c9fde -r 6202d0ff36b4 src/Pure/Tools/build_schedule.scala --- 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) + }) }