merged
authorFabian Huch <huch@in.tum.de>
Sun, 02 Feb 2025 00:14:26 +0100
changeset 82047 9457e0133a85
parent 82046 5a2b9e25cc85 (diff)
parent 82037 cb121d499f11 (current diff)
child 82048 2ea9f9ed19c6
merged
--- a/etc/options	Sat Feb 01 22:49:33 2025 +0100
+++ b/etc/options	Sun Feb 02 00:14:26 2025 +0100
@@ -240,11 +240,14 @@
 
 section "Build Manager"
 
+option build_manager_group : string = "isabelle"
+  -- "common group for users on build manager system"
+
 option build_manager_dir : string = "/srv/build"
   -- "directory for submissions on build server"
 
-option build_manager_address : string = "https://build.proof.cit.tum.de"
-  -- "web address for build server"
+option build_manager_address : string = ""
+  -- "explicit web address for build server"
 
 option build_manager_identifier : string = "build_manager"
   -- "isabelle identifier for build manager processes"
@@ -485,15 +488,13 @@
 section "Build Manager SSH"
 
 option build_manager_ssh_host : string = "build.proof.cit.tum.de" for connection
-  -- "ssh server on which build manager runs"
-
+option build_manager_ssh_port : int = 0 for connection
 option build_manager_ssh_user : string = "" for connection
   -- "ssh user to access build manager system"
 
-option build_manager_ssh_group : string = "isabelle"
-  -- "common group for users on build manager system"
-
-option build_manager_ssh_port : int = 0 for connection
+option build_manager_cluster_ssh_host : string = "localhost" for connection
+option build_manager_cluster_ssh_user : string = "" for connection
+option build_manager_cluster_ssh_port : int = 0 for connection
 
 
 section "Build Manager Database"
--- a/src/Doc/System/Sessions.thy	Sat Feb 01 22:49:33 2025 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Feb 02 00:14:26 2025 +0100
@@ -1065,4 +1065,132 @@
   @{verbatim [display] \<open>  isabelle sync -A: -T -H -s testmachine test/isabelle_afp\<close>}
 \<close>
 
+
+section \<open>Remote build management\<close>
+
+text \<open>
+  Building large collections of Isabelle session (e.g., the AFP) is an
+  expensive operation that might not be feasible on a local device, so
+  powerful remote hardware is necessary to be able to test changes quickly.
+  In a multi-user environment, these hardware resources must be managed such
+  that important tasks can be completed as soon as possible, and automated
+  tasks run in the background when necessary.
+\<close>
+
+subsection \<open>Build manager server\<close>
+
+text \<open>
+  The @{tool_def build_manager} tool starts a server process that manages
+  a queue of tasks, runs build jobs, and serves a web view that displays the
+  results. It consists of several threads:
+  
+    \<^item> \<^emph>\<open>poller\<close>: listens to repository updates and queues automatic tasks.
+  
+    \<^item> \<^emph>\<open>timer\<close>: queues periodic tasks at specific points in time.
+  
+    \<^item> \<^emph>\<open>runner\<close>: starts jobs for feasible tasks with the highest priority
+    whenever possible. Jobs run exclusively on their resources, either on the
+    cluster specified via @{system_option build_manager_cluster} (the 
+    connection to the \<^verbatim>\<open>build_master\<close> host must be specified via
+    \<^verbatim>\<open>build_manager_cluster_ssh\<close> connection options), or on a single remote
+    host (under the identifier given by
+    @{system_option build_manager_identifier}).
+  
+    \<^item> \<^emph>\<open>web_server\<close>: serves the web page. If the web address is not reachable
+    under the SSH hostname of the server, it must be set via 
+    @{system_option build_manager_address}.
+
+  Automated tasks must be registered in a \<^scala_type>\<open>isabelle.Isabelle_CI_Jobs\<close>
+  service. The system option @{system_option build_manager_ci_jobs} controls
+  which jobs are executed by the \<^verbatim>\<open>Build_Manager\<close>.
+
+  The command-line usage to start the server is:
+  @{verbatim [display]
+\<open>Usage: isabelle build_manager [OPTIONS]
+
+  Options are:
+    -A ROOT      include AFP with given root directory (":" for $AFP_BASE)
+    -D DIR       include extra component in given directory
+    -H HOSTS     host specifications for all available hosts of the form
+                 NAMES:PARAMETERS (separated by commas)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -p PORT      explicit web server port
+
+  Run Isabelle build manager.
+\<close>}
+
+  \<^medskip> Options \<^verbatim>\<open>-o\<close> and \<^verbatim>\<open>-p\<close> are the same as in other server applications.
+
+  \<^medskip> Option \<^verbatim>\<open>-A\<close> refers to the AFP (must be a Mercurial clone)
+
+  \<^medskip> Option \<^verbatim>\<open>-D\<close> extra Isabelle components in a Mercurial repository clone to
+  be considered by the poller and CI jobs.
+
+  \<^medskip> Option \<^verbatim>\<open>-H\<close> must list all host specifications to be used in the build
+  cluster or as remote host.
+
+  \<^medskip>
+  In case a job does not complete on its own, it is terminated after a timeout
+  defined by the CI job, or @{system_option build_manager_timeout} for
+  user-submitted tasks.
+
+  \<^medskip>
+  To gracefully stop the build manager, it should be sent an interrupt signal
+  (\<^verbatim>\<open>kill -INT\<close>). This will stop all threads gracefully: Any running build is
+  allowed to complete before the Isabelle process terminates.
+
+  \<^medskip>
+  The build manager stores its persistent data (including user-submitted tasks
+  and build logs) in the directory given by @{system_option build_manager_dir}.
+  It must be writable by the common Unix group specified in
+  @{system_option build_manager_group}. It also needs a PostgreSQL database 
+  (via \<^verbatim>\<open>build_manager_database\<close> connection options) for shared state.
+  A clean database state (e.g., after a schema update) can be restored from
+  build logs via the @{tool_def build_manager_database} tool:
+  @{verbatim [display]
+\<open>Usage: isabelle build_manager_database [OPTIONS]
+
+  Options are:
+    -A ROOT      include AFP with given root directory (":" for $AFP_BASE)
+    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
+    -u           update reports
+
+  Restore build_manager database from log files.
+\<close>}
+
+  Options \<^verbatim>\<open>-A\<close> and \<^verbatim>\<open>-o\<close> are the same as in @{tool_ref build_manager}.
+
+  Option \<^verbatim>\<open>-u\<close> updates Mercurial reports in the persistent storage based on
+  the version history (e.g., to change the diff display in the web server).
+\<close>
+
+subsection \<open>Submitting build tasks\<close>
+
+text \<open>
+  The @{tool_def build_task} tool submits user-defined build tasks by syncing
+  the local Isabelle repository to the server and queuing a task in the shared
+  state. Command-line options are almost identical to the regular @{tool_ref 
+  build}, with the exception of preferences in the remote build.
+
+  For the SSH connection, the server needs to be accessible with the system
+  options @{system_option build_manager_ssh_user}, @{system_option 
+  build_manager_ssh_host}, etc.
+
+  The database needs to be configured similarly (via \<^verbatim>\<open>build_manager_database\<close>
+  connection options) though the PostgreSQL server can also be configured
+  to trust connections of logged in users via ``peer authentication''.
+\<close>
+
+subsubsection \<open>Examples\<close>
+
+text \<open>
+Clean build of the distribution:
+
+  @{verbatim [display] \<open>  isabelle build_task -c -a\<close>}
+
+Build all sessions in the AFP excluding the \<^verbatim>\<open>very_slow\<close> group:
+
+  @{verbatim [display] \<open>  isabelle build_task -A: -X slow -g AFP\<close>}
+\<close>
+
 end
--- a/src/Pure/Build/build_manager.scala	Sat Feb 01 22:49:33 2025 +0100
+++ b/src/Pure/Build/build_manager.scala	Sun Feb 02 00:14:26 2025 +0100
@@ -1537,7 +1537,7 @@
       if (task.build_cluster) store.options.string("build_cluster_identifier") else store.identifier
 
     def open_ssh(): SSH.System = {
-      if (task.build_cluster) store.open_ssh()
+      if (task.build_cluster) store.open_cluster_ssh()
       else Library.the_single(task.build_hosts).open_ssh(store.options)
     }
   }
@@ -1617,31 +1617,24 @@
 
   case class Store(options: Options) {
     val base_dir = Path.explode(options.string("build_manager_dir"))
-    val identifier = options.string("build_manager_identifier")
-    val address = Url(options.string("build_manager_address"))
+    val address = {
+      Url(proper_string(options.string("build_manager_address")) getOrElse
+        "https://" + options.string("build_manager_ssh_host"))
+    }
 
     val pending = base_dir + Path.basic("pending")
-    val finished = base_dir + Path.basic("finished")
 
     def task_dir(task: Task) = pending + Path.basic(task.uuid.toString)
-    def report(kind: String, id: Long): Report =
-      Report(kind, id, finished + Path.make(List(kind, id.toString)))
 
     def sync_permissions(dir: Path, ssh: SSH.System = SSH.Local): Unit = {
       ssh.execute("chmod -R g+rwx " + File.bash_path(dir))
-      ssh.execute("chown -R :" + ssh_group + " " + File.bash_path(dir))
+      ssh.execute("chown -R :" + unix_group + " " + File.bash_path(dir))
     }
 
     def init_dirs(): Unit =
       List(pending, finished).foreach(dir => sync_permissions(Isabelle_System.make_directory(dir)))
 
-    val ssh_group: String = options.string("build_manager_ssh_group")
-
-    def open_ssh(): SSH.Session =
-      SSH.open_session(options,
-        host = options.string("build_manager_ssh_host"),
-        port = options.int("build_manager_ssh_port"),
-        user = options.string("build_manager_ssh_user"))
+    val unix_group: String = options.string("build_manager_group")
 
     def open_database(server: SSH.Server = SSH.no_server): PostgreSQL.Database =
       PostgreSQL.open_database_server(options, server = server,
@@ -1654,6 +1647,30 @@
         ssh_port = options.int("build_manager_database_ssh_port"),
         ssh_user = options.string("build_manager_database_ssh_user"))
 
+
+    /* server */
+
+    val identifier = options.string("build_manager_identifier")
+
+    val finished = base_dir + Path.basic("finished")
+    def report(kind: String, id: Long): Report =
+      Report(kind, id, finished + Path.make(List(kind, id.toString)))
+
+    def open_cluster_ssh(): SSH.Session =
+      SSH.open_session(options,
+        host = options.string("build_manager_cluster_ssh_host"),
+        port = options.int("build_manager_cluster_ssh_port"),
+        user = options.string("build_manager_cluster_ssh_user"))
+
+
+    /* client */
+
+    def open_ssh(): SSH.Session =
+      SSH.open_session(options,
+        host = options.string("build_manager_ssh_host"),
+        port = options.int("build_manager_ssh_port"),
+        user = options.string("build_manager_ssh_user"))
+
     def open_postgresql_server(): SSH.Server =
       PostgreSQL.open_server(options,
         host = options.string("build_manager_database_host"),
@@ -1704,24 +1721,13 @@
 
   /* Isabelle tool wrapper */
 
-  private def show_options(relevant_options: List[String], options: Options): String =
-    cat_lines(relevant_options.flatMap(options.get).map(_.print))
-
-  private val notable_server_options =
-    List(
-      "build_manager_dir",
-      "build_manager_address",
-      "build_manager_ssh_host",
-      "build_manager_ssh_group",
-      "build_manager_ci_jobs")
-
   val isabelle_tool = Isabelle_Tool("build_manager", "run build manager", Scala_Project.here,
     { args =>
       var afp_root: Option[Path] = None
       val dirs = new mutable.ListBuffer[Path]
       val build_hosts = new mutable.ListBuffer[Build_Cluster.Host]
       var options = Options.init()
-      var port = 8080
+      var port = 0
 
       val getopts = Getopts("""
 Usage: isabelle build_manager [OPTIONS]
@@ -1734,9 +1740,8 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p PORT      explicit web server port
 
-  Run Isabelle build manager. Notable system options:
-
-""" + Library.indent_lines(2, show_options(notable_server_options, options)) + "\n",
+  Run Isabelle build manager.
+""",
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "D:" -> (arg => dirs += Path.explode(arg)),
         "H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.global, arg)),
@@ -1934,8 +1939,6 @@
 
   /* Isabelle tool wrapper */
 
-  val notable_client_options = List("build_manager_ssh_user", "build_manager_ssh_group")
-
   val isabelle_tool2 = Isabelle_Tool("build_task", "submit build task for build manager",
     Scala_Project.here,
     { args =>
@@ -1979,7 +1982,7 @@
 
   Submit build task on SSH server. Notable system options:
 
-""" + Library.indent_lines(2, show_options(notable_client_options, options)) + "\n",
+""" + Library.indent_lines(2, options.get("build_manager_ssh_user").get.print) + "\n",
         "A:" -> (arg => afp_root = Some(if (arg == ":") AFP.BASE else Path.explode(arg))),
         "B:" -> (arg => base_sessions += arg),
         "P" -> (_ => presentation = true),