# HG changeset patch
# User wenzelm
# Date 1689756160 -7200
# Node ID 822ddccda899234d9c40032af5edb4cc76a37679
# Parent  63d55ba90a9f541444845fac2b839640ed3bcc13
proforma support for remote build hosts;

diff -r 63d55ba90a9f -r 822ddccda899 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Jul 18 23:03:39 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Jul 19 10:42:40 2023 +0200
@@ -69,8 +69,11 @@
   class Engine(val name: String) extends Isabelle_System.Service {
     override def toString: String = name
 
-    def build_options(options: Options): Options =
-      options + "completion_limit=0" + "editor_tracing_messages=0"
+    def build_options(options: Options, build_hosts: List[Build_Cluster.Host] = Nil): Options = {
+      val options1 = options + "completion_limit=0" + "editor_tracing_messages=0"
+      if (build_hosts.isEmpty) options1
+      else options1 + "build_database_server" + "build_database_test"
+    }
 
     def build_process(
       build_context: Build_Process.Context,
@@ -78,8 +81,11 @@
       server: SSH.Server
     ): Build_Process = new Build_Process(build_context, build_progress, server)
 
-    final def build_store(options: Options, cache: Term.Cache = Term.Cache.make()): Store = {
-      val store = Store(build_options(options), cache = cache)
+    final def build_store(options: Options,
+      build_hosts: List[Build_Cluster.Host] = Nil,
+      cache: Term.Cache = Term.Cache.make()
+    ): Store = {
+      val store = Store(build_options(options, build_hosts = build_hosts), cache = cache)
 
       Isabelle_System.make_directory(store.output_dir + Path.basic("log"))
 
@@ -107,6 +113,7 @@
 
   def build(
     options: Options,
+    build_hosts: List[Build_Cluster.Host] = Nil,
     selection: Sessions.Selection = Sessions.Selection.empty,
     browser_info: Browser_Info.Config = Browser_Info.Config.none,
     progress: Progress = new Progress,
@@ -192,10 +199,10 @@
         /* build process and results */
 
         val build_context =
-          Build_Process.Context(store, build_deps, hostname = hostname(build_options),
-            build_heap = build_heap, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
-            fresh_build = fresh_build, no_build = no_build, session_setup = session_setup,
-            master = true)
+          Build_Process.Context(store, build_deps, build_hosts = build_hosts,
+            hostname = hostname(build_options), build_heap = build_heap,
+            numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
+            no_build = no_build, session_setup = session_setup, master = true)
 
         if (clean_build) {
           for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
@@ -270,6 +277,7 @@
     { args =>
       var base_sessions: List[String] = Nil
       var select_dirs: List[Path] = Nil
+      val build_hosts = new mutable.ListBuffer[Build_Cluster.Host]
       var numa_shuffling = false
       var browser_info = Browser_Info.Config.none
       var requirements = false
@@ -296,6 +304,7 @@
   Options are:
     -B NAME      include session NAME and all descendants
     -D DIR       include session directory and select its sessions
+    -H HOST      add host for distrubuted build
     -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -P DIR       enable HTML/PDF presentation in directory (":" for default)
     -R           refer to requirements of selected sessions
@@ -324,6 +333,7 @@
 """ + Library.indent_lines(4,  Build_Log.Settings.show()) + "\n",
         "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
         "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+        "H:" -> (arg => build_hosts += Build_Cluster.Host.parse(arg)),
         "N" -> (_ => numa_shuffling = true),
         "P:" -> (arg => browser_info = Browser_Info.Config.make(arg)),
         "R" -> (_ => requirements = true),
@@ -381,7 +391,8 @@
             fresh_build = fresh_build,
             no_build = no_build,
             soft_build = soft_build,
-            export_files = export_files)
+            export_files = export_files,
+            build_hosts = build_hosts.toList)
         }
       val stop_date = Date.now()
       val elapsed_time = stop_date.time - start_date.time
diff -r 63d55ba90a9f -r 822ddccda899 src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Tue Jul 18 23:03:39 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Wed Jul 19 10:42:40 2023 +0200
@@ -22,6 +22,8 @@
       numa: Boolean = false,
       options: List[Options.Spec] = Nil
     ): Host = new Host(host, user, port, jobs, numa, options)
+
+    def parse(str: String): Host = Host(host = str)  // FIXME proper parse
   }
 
   final class Host private(
diff -r 63d55ba90a9f -r 822ddccda899 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Jul 18 23:03:39 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jul 19 10:42:40 2023 +0200
@@ -19,6 +19,7 @@
   sealed case class Context(
     store: Store,
     build_deps: isabelle.Sessions.Deps,
+    build_hosts: List[Build_Cluster.Host] = Nil,
     ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
     hostname: String = Isabelle_System.hostname(),
     numa_shuffling: Boolean = false,
@@ -1104,6 +1105,11 @@
       if (build_context.master) start_build()
       start_worker()
 
+      if (build_context.master && build_context.build_hosts.nonEmpty) {
+        build_progress.echo("Remote build hosts:\n" +
+          cat_lines(build_context.build_hosts.map("  " + _)))
+      }
+
       if (build_context.master && !build_context.worker_active) {
         build_progress.echo("Waiting for external workers ...")
       }