# HG changeset patch
# User wenzelm
# Date 1708185415 -3600
# Node ID b7187d4cdf68212dfdb7af9a60160deecece57d0
# Parent  7b22356fd55ca25d59e1c978bb14005f4c9a275b
clarified default "isabelle build -j0 -H";

diff -r 7b22356fd55c -r b7187d4cdf68 NEWS
--- a/NEWS	Sat Feb 17 15:33:01 2024 +0100
+++ b/NEWS	Sat Feb 17 16:56:55 2024 +0100
@@ -100,6 +100,12 @@
 
 *** System ***
 
+* The command-line tool "isabelle build" now uses default 0 (instead of
+1) for option -j. This means that "isabelle build -H" will initialize
+the build queue and oversee remote workers, but not run any Isabelle
+sessions on its own account. INCOMPATIBILITY, use "isabelle build -j1
+-H" for the old behaviour, to have the local host participate as worker.
+
 * Directory src/Tools/Demo provides an Isabelle system component with
 command-line tool that is implemented in Isabelle/Scala. It serves as
 demonstration for user-defined tools.
diff -r 7b22356fd55c -r b7187d4cdf68 src/Doc/System/Sessions.thy
--- a/src/Doc/System/Sessions.thy	Sat Feb 17 15:33:01 2024 +0100
+++ b/src/Doc/System/Sessions.thy	Sat Feb 17 16:56:55 2024 +0100
@@ -377,7 +377,8 @@
     -e           export files from session specification into file-system
     -f           fresh build
     -g NAME      select session group NAME
-    -j INT       maximum number of parallel jobs (default 1)
+    -j INT       maximum number of parallel jobs
+                 (default: 1 for local build, 0 for build cluster)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- take existing session build databases
@@ -495,7 +496,8 @@
   \<^medskip>
   Option \<^verbatim>\<open>-j\<close> specifies the maximum number of parallel build jobs (prover
   processes). Each prover process is subject to a separate limit of parallel
-  worker threads, cf.\ system option @{system_option_ref threads}.
+  worker threads, cf.\ system option @{system_option_ref threads}. The default
+  is 1 for a local build, and 0 for a cluster build (see option \<^verbatim>\<open>-H\<close> below).
 
   \<^medskip>
   Option \<^verbatim>\<open>-N\<close> enables cyclic shuffling of NUMA CPU nodes. This may help
@@ -524,6 +526,11 @@
   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 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
+  Isabelle sessions on its own account.
+
   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
diff -r 7b22356fd55c -r b7187d4cdf68 src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Sat Feb 17 15:33:01 2024 +0100
+++ b/src/Pure/Build/build.scala	Sat Feb 17 16:56:55 2024 +0100
@@ -247,7 +247,7 @@
             build_hosts = build_hosts, hostname = hostname(build_options), build_heap = build_heap,
             numa_shuffling = numa_shuffling, fresh_build = fresh_build,
             no_build = no_build, session_setup = session_setup,
-            jobs = max_jobs.getOrElse(1), master = true)
+            jobs = max_jobs.getOrElse(if (build_hosts.nonEmpty) 0 else 1), master = true)
 
         if (clean_build) {
           for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
@@ -365,7 +365,8 @@
     -e           export files from session specification into file-system
     -f           fresh build
     -g NAME      select session group NAME
-    -j INT       maximum number of parallel jobs (default 1)
+    -j INT       maximum number of parallel jobs
+                 (default: 1 for local build, 0 for build cluster)
     -k KEYWORD   check theory sources for conflicts with proposed keywords
     -l           list session source files
     -n           no build -- take existing session build databases