--- 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.
--- 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
--- 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