--- a/src/Pure/Build/build.scala Sat Feb 17 15:08:48 2024 +0100
+++ b/src/Pure/Build/build.scala Sat Feb 17 15:20:38 2024 +0100
@@ -35,11 +35,11 @@
hostname: String = Isabelle_System.hostname(),
numa_shuffling: Boolean = false,
build_heap: Boolean = false,
- max_jobs: Option[Int] = None,
fresh_build: Boolean = false,
no_build: Boolean = false,
session_setup: (String, Session) => Unit = (_, _) => (),
build_uuid: String = UUID.random().toString,
+ jobs: Int = 0,
master: Boolean = false
) {
override def toString: String =
@@ -49,7 +49,6 @@
def sessions_structure: isabelle.Sessions.Structure = deps.sessions_structure
- def jobs: Int = max_jobs.getOrElse(1)
def worker_active: Boolean = jobs > 0
}
@@ -240,8 +239,9 @@
val build_context =
Context(store, build_deps, engine = build_engine, afp_root = afp_root,
build_hosts = build_hosts, hostname = hostname(build_options), build_heap = build_heap,
- numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
- no_build = no_build, session_setup = session_setup, master = true)
+ numa_shuffling = numa_shuffling, fresh_build = fresh_build,
+ no_build = no_build, session_setup = session_setup,
+ jobs = max_jobs.getOrElse(1), master = true)
if (clean_build) {
for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
@@ -625,7 +625,7 @@
val build_context =
Context(store, build_deps, engine = build_engine, afp_root = afp_root,
hostname = hostname(build_options), numa_shuffling = numa_shuffling,
- max_jobs = max_jobs, build_uuid = build_master.build_uuid)
+ build_uuid = build_master.build_uuid, jobs = max_jobs.getOrElse(1))
build_engine.run_build_process(build_context, progress, server)
}
--- a/src/Pure/Build/build_benchmark.scala Sat Feb 17 15:08:48 2024 +0100
+++ b/src/Pure/Build/build_benchmark.scala Sat Feb 17 15:20:38 2024 +0100
@@ -45,8 +45,8 @@
val selection = Sessions.Selection(sessions = List(benchmark_session))
val full_sessions = Sessions.load_structure(options.int.update("threads", 1))
- val build_context =
- Build.Context(store, Sessions.deps(full_sessions.selection(selection)).check_errors)
+ val build_deps = Sessions.deps(full_sessions.selection(selection)).check_errors
+ val build_context = Build.Context(store, build_deps, jobs = 1)
val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
val session = sessions(benchmark_session)
--- a/src/Pure/Build/build_schedule.scala Sat Feb 17 15:08:48 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Sat Feb 17 15:20:38 2024 +0100
@@ -1304,8 +1304,7 @@
val build_context =
Build.Context(store, build_deps, engine = Build_Engine, afp_root = afp_root,
build_hosts = build_hosts, hostname = Build.hostname(build_options),
- numa_shuffling = numa_shuffling, max_jobs = Some(0), session_setup = session_setup,
- master = true)
+ numa_shuffling = numa_shuffling, session_setup = session_setup, master = true)
val cluster_hosts = build_context.build_hosts