--- a/CONTRIBUTORS Sun Aug 27 14:22:28 2023 +0200
+++ b/CONTRIBUTORS Sun Aug 27 15:28:48 2023 +0200
@@ -21,6 +21,9 @@
ML heap usage and stored heap size has been significantly reduced;
based on new command-line tool "isabelle profiling".
+* 2023: Makarius Wenzel and Fabian Huch
+ Support for distributed build clusters, based on SSH and PostgreSQL.
+
Contributions to Isabelle2022
-----------------------------
--- a/NEWS Sun Aug 27 14:22:28 2023 +0200
+++ b/NEWS Sun Aug 27 15:28:48 2023 +0200
@@ -43,6 +43,22 @@
* The Eisbach 'method' command now takes an optional description for
display with 'print_methods', similar to the 'method_setup' command.
+* Experimental support for distributed build clusters, based on SSH and
+PostgreSQL. Example for 3 nodes (local, host1, host2):
+
+ isabelle build -a -j2 -o threads=8 \
+ -H host1:jobs=2,threads=8
+ -H host2:jobs=4:threads=4,numa,shared
+
+Like the "isabelle sync" tool, this requires a proper Isabelle
+repository clone (e.g. via "isabelle/Admin/init -r Isabelle2023").
+
+The build database server needs to be specified for each remote node in
+$USER_HOME/.isabelle/build_cluster (according to option
+"build_cluster_identifier").
+
+See also "isabelle build_process -?" and "isabelle build_worker -?".
+
*** Document preparation ***
--- a/src/Doc/System/Sessions.thy Sun Aug 27 14:22:28 2023 +0200
+++ b/src/Doc/System/Sessions.thy Sun Aug 27 15:28:48 2023 +0200
@@ -360,8 +360,11 @@
\<open>Usage: isabelle build [OPTIONS] [SESSIONS ...]
Options are:
+ -A ROOT include AFP with given root directory (":" for $AFP_BASE)
-B NAME include session NAME and all descendants
-D DIR include session directory and select its sessions
+ -H HOSTS additional build cluster host specifications, of the form
+ "NAMES:PARAMETERS" (separated by commas)
-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
@@ -384,6 +387,9 @@
Build and manage Isabelle sessions: ML heaps, session databases, documents.
+ Parameters for host specifications (option -H), apart from system options:
+ ...
+
Notable system options: see "isabelle options -l -t build"
Notable system settings:
@@ -506,6 +512,25 @@
possible to use option \<^verbatim>\<open>-k\<close> repeatedly to check multiple keywords. The
theory sources are checked for conflicts wrt.\ this hypothetical change of
syntax, e.g.\ to reveal occurrences of identifiers that need to be quoted.
+
+ \<^medskip>
+ Option \<^verbatim>\<open>-H\<close> augments the cluster hosts to be used in this build process.
+ Each \<^verbatim>\<open>-H\<close> option accepts multiple host names (separated by commas), which
+ all share the same (optional) parameters. Multiple \<^verbatim>\<open>-H\<close> options may be
+ given to specify further hosts (with different parameters). For example:
+ \<^verbatim>\<open>-H host1,host2:jobs=2,threads=4 -H host3:jobs=4,threads=6\<close>.
+
+ The syntax for host parameters follows Isabelle outer syntax, notably with
+ double-quoted string literals. On the command-line, this may require extra
+ single quotes or escapes. For example: \<^verbatim>\<open>-H 'host4:dirs="..."'\<close>.
+
+ The presence of at least one \<^verbatim>\<open>-H\<close> option changes the mode of operation of
+ \<^verbatim>\<open>isabelle build\<close> substantially. It uses a shared PostgreSQL database
+ server, which needs to be accessible from each node via local system options
+ such as @{system_option "build_database_server"}, @{system_option
+ "build_database_host"}, or @{system_option "build_database_ssh_host"}.
+ Remote host connections are managed via regular SSH configuration, see also
+ \<^path>\<open>$HOME/.ssh/config\<close> on each node.
\<close>
@@ -565,6 +590,12 @@
Inform about the status of all sessions required for AFP, without building
anything yet:
@{verbatim [display] \<open> isabelle build -D '$AFP' -R -v -n\<close>}
+
+ \<^smallskip>
+ Run a distributed build on 3 cluster hosts (local, \<^verbatim>\<open>host1\<close>, \<^verbatim>\<open>host2\<close>):
+ @{verbatim [display] \<open> isabelle build -a -j2 -o threads=8 \
+ -H host1:jobs=2,threads=8
+ -H host2:jobs=4:threads=4,numa,shared\<close>}
\<close>