--- 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