# HG changeset patch # User wenzelm # Date 1708179638 -3600 # Node ID 389c1bfa7c3e87e96aaf2e7c23d7a742a0637556 # Parent 51e9d1a80e39387c762fd013ab6333e94e5de8fb clarified signature: more standard defaults; diff -r 51e9d1a80e39 -r 389c1bfa7c3e src/Pure/Build/build.scala --- 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) } diff -r 51e9d1a80e39 -r 389c1bfa7c3e src/Pure/Build/build_benchmark.scala --- 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) diff -r 51e9d1a80e39 -r 389c1bfa7c3e src/Pure/Build/build_schedule.scala --- 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