# HG changeset patch
# User wenzelm
# Date 1693142928 -7200
# Node ID 12aac1489f3bfcddfd21d3598dc2ed7512999682
# Parent  e92bbd5fd66f2b9cc40c43d10a8bec2b5034f472
minimal documentation for build cluster support;

diff -r e92bbd5fd66f -r 12aac1489f3b CONTRIBUTORS
--- 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
 -----------------------------
diff -r e92bbd5fd66f -r 12aac1489f3b NEWS
--- 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 ***
 
diff -r e92bbd5fd66f -r 12aac1489f3b src/Doc/System/Sessions.thy
--- 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>