# HG changeset patch
# User wenzelm
# Date 1678187161 -3600
# Node ID eff08c3f89fe143c45eaba9548fadd4bb28b4300
# Parent  911548e4f228abe62af09308b9f9b98f449459d9
basic setup for "isabelle build_worker";

diff -r 911548e4f228 -r eff08c3f89fe src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Mar 07 12:03:42 2023 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Tue Mar 07 12:06:01 2023 +0100
@@ -122,6 +122,7 @@
 class Tools extends Isabelle_Scala_Tools(
   Build.isabelle_tool1,
   Build.isabelle_tool2,
+  Build.isabelle_tool3,
   Build_Docker.isabelle_tool,
   CI_Build.isabelle_tool,
   Doc.isabelle_tool,
diff -r 911548e4f228 -r eff08c3f89fe src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 07 12:03:42 2023 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 07 12:06:01 2023 +0100
@@ -66,6 +66,19 @@
 
   /* build */
 
+  def build_init(options: Options): Sessions.Store = {
+    val build_options =
+      options +
+        "completion_limit=0" +
+        "editor_tracing_messages=0" +
+        ("pide_reports=" + options.bool("build_pide_reports"))
+    val store = Sessions.store(build_options)
+
+    Isabelle_Fonts.init()
+
+    store
+  }
+
   def build(
     options: Options,
     selection: Sessions.Selection = Sessions.Selection.empty,
@@ -88,15 +101,8 @@
     augment_options: String => List[Options.Spec] = _ => Nil,
     session_setup: (String, Session) => Unit = (_, _) => ()
   ): Results = {
-    val build_options =
-      options +
-        "completion_limit=0" +
-        "editor_tracing_messages=0" +
-        ("pide_reports=" + options.bool("build_pide_reports"))
-
-    val store = Sessions.store(build_options)
-
-    Isabelle_Fonts.init()
+    val store = build_init(options)
+    val build_options = store.options
 
 
     /* session selection and dependencies */
@@ -365,6 +371,85 @@
 
 
 
+  /** "isabelle build_worker" **/
+
+  /* build_worker */
+
+  def build_worker(
+    options: Options,
+    build_uuid: String,
+    progress: Progress = new Progress,
+    dirs: List[Path] = Nil,
+    infos: List[Sessions.Info] = Nil,
+    numa_shuffling: Boolean = false,
+    max_jobs: Int = 1,
+    session_setup: (String, Session) => Unit = (_, _) => ()
+  ): Results = {
+    val store = build_init(options)
+    val build_options = store.options
+
+    progress.echo("build worker for " + build_uuid)
+    progress.echo_warning("FIXME")
+    ???
+  }
+
+
+  /* command-line wrapper */
+
+  val isabelle_tool2 = Isabelle_Tool("build_worker", "external worker for session build process",
+    Scala_Project.here,
+    { args =>
+      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
+
+      var numa_shuffling = false
+      var dirs: List[Path] = Nil
+      var max_jobs = 1
+      var options = Options.init(opts = build_options)
+      var verbose = false
+      var build_uuid = ""
+
+      val getopts = Getopts("""
+Usage: isabelle build_worker [OPTIONS] ...]
+
+  Options are:
+    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
+    -U UUID      Universally Unique Identifier of the build process
+    -d DIR       include session directory
+    -j INT       maximum number of parallel jobs (default 1)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -v           verbose
+
+  Run as external worker for session build process, as identified via
+  option -U UUID.
+""" + Library.indent_lines(2,  Build_Log.Settings.show()) + "\n",
+        "N" -> (_ => numa_shuffling = true),
+        "U:" -> (arg => build_uuid = arg),
+        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+        "j:" -> (arg => max_jobs = Value.Int.parse(arg)),
+        "o:" -> (arg => options = options + arg),
+        "v" -> (_ => verbose = true))
+
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      if (build_uuid.isEmpty) error("Missing UUID for build process (option -U)")
+
+      val progress = new Console_Progress(verbose = verbose)
+
+      val results =
+        progress.interrupt_handler {
+          build_worker(options, build_uuid,
+            progress = progress,
+            dirs = dirs,
+            numa_shuffling = Host.numa_check(progress, numa_shuffling),
+            max_jobs = max_jobs)
+        }
+
+      sys.exit(results.rc)
+    })
+
+
+
   /** "isabelle log" **/
 
   /* theory markup/messages from session database */
@@ -535,7 +620,7 @@
 
   /* command-line wrapper */
 
-  val isabelle_tool2 = Isabelle_Tool("log", "print messages from session build database",
+  val isabelle_tool3 = Isabelle_Tool("log", "print messages from session build database",
     Scala_Project.here,
     { args =>
       /* arguments */