# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1738451321 -3600
# Node ID b8ba54ab790bd51087761a1826e396ee3214e16f
# Parent  c1685983428828e09fe8196bb47ff18b0acb87c4
documentation about Build_Manager;

diff -r c16859834288 -r b8ba54ab790b src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Feb 01 22:41:43 2025 +0100
+++ b/src/Doc/System/Sessions.thy	Sun Feb 02 00:08:41 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