# HG changeset patch
# User wenzelm
# Date 1715517673 -7200
# Node ID 438d583ab378f9fad13bd4905b7d5fb737baba3c
# Parent  5e64a54f6790beb22ec061af7b88c3576adac542
more documentation on "isabelle build -H" and underlying system registry tables "host" and "cluster";

diff -r 5e64a54f6790 -r 438d583ab378 NEWS
--- a/NEWS	Thu May 02 15:40:05 2024 +0200
+++ b/NEWS	Sun May 12 14:41:13 2024 +0200
@@ -232,15 +232,31 @@
 default settings use "$ISABELLE_HOME/etc/registry.toml?" and
 "$ISABELLE_HOME_USER/etc/registry.toml?" (in that order).
 
-* Isabelle build cluster specifications now refer to the underlying
-registry for default parameters and system options, using the TOML table
-"host". For example, the command "isabelle build -H abc:user=test" can
-be implicitly augmented by host parameters and options in
-$ISABELLE_HOME_USER/etc/registry.toml like this:
-
-  [host.abc]
-  hostname = "abc.acme.org"
-  ssh_compression = false
+* Isabelle build cluster specifications, as seen in "isabelle build"
+option "-H", now use the underlying system registry to determine actual
+host names, parameters, and system options. A name without prefix refers
+to the registry table "host": each entry consists of an optional
+"hostname" and further options. A name with the prefix "cluster." refers
+to the table "cluster": each entry provides "hosts", an array of names
+for entries of the table "host" as above, and additional options that
+apply to all hosts simultaneously.
+
+For example, consider "isabelle build -H a -H b -H cluster.xy" in the
+context of a system registry $ISABELLE_HOME_USER/etc/registry.toml like
+this:
+
+  host.a = { hostname = "host-a.acme.org", jobs = 2 }
+  host.b = { hostname = "host-b.acme.org", jobs = 2 }
+
+  host.x = { hostname = "server1.example.com" }
+  host.y = { hostname = "server2.example.com" }
+  cluster.xy = { hosts = ["x", "y"], jobs = 4 }
+
+If "hostname" is omitted, its default is the table entry name itself. If
+that contains a dot, it needs to be quoted according to TOML syntax:
+
+  host."host-a.acme.org" = { jobs = 2 }
+  host."host-b.acme.org" = { jobs = 2 }
 
 * Isabelle/Scala and derived Scala tools now use the syntax of Scala
 3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as
diff -r 5e64a54f6790 -r 438d583ab378 src/Doc/System/Environment.thy
--- a/src/Doc/System/Environment.thy	Thu May 02 15:40:05 2024 +0200
+++ b/src/Doc/System/Environment.thy	Sun May 12 14:41:13 2024 +0200
@@ -449,7 +449,7 @@
 \<close>
 
 
-section \<open>System registry via TOML\<close>
+section \<open>System registry via TOML \label{sec:system-registry}\<close>
 
 text \<open>
   Tools implemented in Isabelle/Scala may refer to a global registry of
diff -r 5e64a54f6790 -r 438d583ab378 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Thu May 02 15:40:05 2024 +0200
+++ b/src/Doc/System/Sessions.thy	Sun May 12 14:41:13 2024 +0200
@@ -516,15 +516,24 @@
 
   \<^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>.
+  Each \<^verbatim>\<open>-H\<close> option accepts multiple host or cluster names (separated by
+  commas), which all share the same (optional) parameters or system options.
+  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 system registry (\secref{sec:system-registry}) may define host and
+  cluster names in its tables \<^verbatim>\<open>host\<close> and \<^verbatim>\<open>cluster\<close>, respectively. A name in
+  option \<^verbatim>\<open>-H\<close> without prefix refers to the registry table \<^verbatim>\<open>host\<close>: each entry
+  consists of an optional \<^verbatim>\<open>hostname\<close> and further options. A name with the
+  prefix ``\<^verbatim>\<open>cluster.\<close>'' refers to the table \<^verbatim>\<open>cluster\<close>: each entry provides
+  \<^verbatim>\<open>hosts\<close>, an array of names for entries of the table \<^verbatim>\<open>host\<close> as above, and
+  additional options that apply to all hosts simultaneously.
+
   The local host only participates in cluster build, if an explicit option
   \<^verbatim>\<open>-j\<close> > 0 is given. The default is 0, which means that \<^verbatim>\<open>isabelle build -H\<close>
   will initialize the build queue and oversee remote workers, but not run any
@@ -602,6 +611,21 @@
   @{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>}
+
+  \<^smallskip>
+  Use build hosts and cluster specifications:
+  @{verbatim [display] \<open>  isabelle build -H a -H b -H cluster.xy\<close>}
+
+  The above requires a \<^path>\<open>$ISABELLE_HOME_USER/etc/registry.toml\<close> file like
+  this:
+
+@{verbatim [display] \<open>    host.a = { hostname = "host-a.acme.org", jobs = 2 }
+    host.b = { hostname = "host-b.acme.org", jobs = 2 }
+
+    host.x = { hostname = "server1.example.com" }
+    host.y = { hostname = "server2.example.com" }
+    cluster.xy = { hosts = ["x", "y"], jobs = 4 }
+\<close>}
 \<close>