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