# HG changeset patch # User wenzelm # Date 1677775589 -3600 # Node ID 57ede1743caf9327ddbb3c0f2eec8e240b8afa74 # Parent df1150ec6cd770e94ae05a9e74e4bb8597631e0c# Parent 032c76e044755a9dd0012a088ad3ca82c7a7e7f5 merged diff -r df1150ec6cd7 -r 57ede1743caf NEWS --- a/NEWS Thu Mar 02 11:34:54 2023 +0000 +++ b/NEWS Thu Mar 02 17:46:29 2023 +0100 @@ -270,6 +270,10 @@ scalable, and supports most options from "isabelle build". Partial builds are supported as well, e.g. "isabelle update -n -a". +* System option "ML_process_policy" has been renamed to +"process_policy", as it may affect other processes as well (notably in +"isabelle build"). + * Isabelle/Scala provides generic support for XZ and Zstd compression, via Compress.Options and Compress.Cache. Bytes.uncompress automatically detects the compression scheme. diff -r df1150ec6cd7 -r 57ede1743caf etc/build.props --- a/etc/build.props Thu Mar 02 11:34:54 2023 +0000 +++ b/etc/build.props Thu Mar 02 17:46:29 2023 +0100 @@ -152,6 +152,7 @@ src/Pure/System/components.scala \ src/Pure/System/executable.scala \ src/Pure/System/getopts.scala \ + src/Pure/System/host.scala \ src/Pure/System/isabelle_charset.scala \ src/Pure/System/isabelle_fonts.scala \ src/Pure/System/isabelle_platform.scala \ @@ -162,7 +163,6 @@ src/Pure/System/linux.scala \ src/Pure/System/mingw.scala \ src/Pure/System/nodejs.scala \ - src/Pure/System/numa.scala \ src/Pure/System/options.scala \ src/Pure/System/platform.scala \ src/Pure/System/posix_interrupt.scala \ diff -r df1150ec6cd7 -r 57ede1743caf etc/options --- a/etc/options Thu Mar 02 11:34:54 2023 +0000 +++ b/etc/options Thu Mar 02 17:46:29 2023 +0100 @@ -132,6 +132,9 @@ option timeout_build : bool = true -- "observe timeout for session build" +option process_policy : string = "" + -- "command prefix for underlying process, notably ML with NUMA policy" + option process_output_tail : int = 40 -- "build process output tail shown to user (in lines, 0 = unlimited)" @@ -165,9 +168,6 @@ public option ML_system_apple : bool = true -- "prefer native Apple/ARM64 platform (change requires restart)" -public option ML_process_policy : string = "" - -- "ML process command prefix (process policy)" - section "Build Process" diff -r df1150ec6cd7 -r 57ede1743caf lib/scripts/polyml-version --- a/lib/scripts/polyml-version Thu Mar 02 11:34:54 2023 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,20 +0,0 @@ -#!/usr/bin/env bash -# -# polyml-version --- determine Poly/ML runtime system version - -if [ -x "$ML_HOME/polyml-version" ]; then - "$ML_HOME/polyml-version" -elif [ -x "$ML_HOME/poly" ]; then - VERSION="$(env \ - LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ - DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ - "$ML_HOME/poly" -v -H 10)" - REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' - if [[ "$VERSION" =~ $REGEXP ]]; then - echo "polyml${BASH_REMATCH[1]}" - else - echo polyml-undefined - fi -else - echo polyml-undefined -fi diff -r df1150ec6cd7 -r 57ede1743caf src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Doc/JEdit/JEdit.thy Thu Mar 02 17:46:29 2023 +0100 @@ -243,7 +243,7 @@ -l NAME logic image name -m MODE add print mode for output -n no build of session image on startup - -p CMD ML process command prefix (process policy) + -p CMD command prefix for ML process (e.g. NUMA policy) -s system build mode for session image (system_heaps=true) -u user build mode for session image (system_heaps=false) @@ -308,7 +308,7 @@ Isabelle desktop application without further options. The \<^verbatim>\-p\ option allows to override the implicit default of the system - option @{system_option_ref ML_process_policy} for ML processes started by + option @{system_option_ref process_policy} for ML processes started by the Prover IDE, e.g. to control CPU affinity on multiprocessor systems. The JVM system property \<^verbatim>\isabelle.jedit_server\ provides a different server diff -r df1150ec6cd7 -r 57ede1743caf src/HOL/Tools/Mirabelle/mirabelle.scala --- a/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Thu Mar 02 17:46:29 2023 +0100 @@ -215,7 +215,7 @@ progress = progress, dirs = dirs, select_dirs = select_dirs, - numa_shuffling = NUMA.check(progress, numa_shuffling), + numa_shuffling = Host.numa_check(progress, numa_shuffling), max_jobs = max_jobs, verbose = verbose) } diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Mar 02 17:46:29 2023 +0100 @@ -196,11 +196,9 @@ def build_history_options: String = " -h " + Bash.string(host) + " " + - (java_heap match { - case "" => "" - case h => - "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' " - }) + options + if_proper(java_heap, + "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + java_heap + "\"' ") + + options } val remote_builds_old: List[Remote_Build] = diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/ML/ml_process.scala Thu Mar 02 17:46:29 2023 +0100 @@ -117,9 +117,10 @@ bash_env.put("ISABELLE_TMP", File.standard_path(isabelle_tmp)) bash_env.put("POLYSTATSDIR", isabelle_tmp.getAbsolutePath) - val policy = options.string("ML_process_policy") match { case "" => "" case s => s + " " } + val process_policy = options.string("process_policy") + val process_prefix = if_proper(process_policy, process_policy + " ") - Bash.process(policy + """"$ML_HOME/poly" -q """ + Bash.strings(bash_args), + Bash.process(process_prefix + "\"$POLYML_EXE\" -q " + Bash.strings(bash_args), cwd = cwd, env = bash_env, redirect = redirect, diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/System/host.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/host.scala Thu Mar 02 17:46:29 2023 +0100 @@ -0,0 +1,126 @@ +/* Title: Pure/System/host.scala + Author: Makarius + +Information about compute hosts, including NUMA: Non-Uniform Memory Access of +separate CPU nodes. + +See also https://www.open-mpi.org/projects/hwloc --- notably "lstopo" or +"hwloc-ls" (e.g. via Ubuntu package "hwloc"). +*/ + +package isabelle + + +object Host { + /* allocated resources */ + + object Node_Info { def none: Node_Info = Node_Info("", None) } + + sealed case class Node_Info(hostname: String, numa_node: Option[Int]) + + + /* available NUMA nodes */ + + private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online") + + def numa_nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = { + val Single = """^(\d+)$""".r + val Multiple = """^(\d+)-(\d+)$""".r + + def parse(s: String): List[Int] = + s match { + case Single(Value.Int(i)) => List(i) + case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList + case _ => error("Cannot parse CPU NUMA node specification: " + quote(s)) + } + + val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None + for { + path <- numa_info.toList + if enabled && ssh.is_file(path) + s <- space_explode(',', ssh.read(path).trim) + n <- parse(s) + } yield n + } + + + /* process policy via numactl tool */ + + def numactl(node: Int): String = "numactl -m" + node + " -N" + node + def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok + + def process_policy(node: Int): String = if (numactl_ok(node)) numactl(node) else "" + + def process_policy_options(options: Options, numa_node: Option[Int]): Options = + numa_node match { + case None => options + case Some(n) => options.string("process_policy") = process_policy(n) + } + + def perhaps_process_policy_options(options: Options): Options = { + val numa_node = + try { + numa_nodes() match { + case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head) + case _ => None + } + } + catch { case ERROR(_) => None } + process_policy_options(options, numa_node) + } + + + /* shuffling of NUMA nodes */ + + def numa_check(progress: Progress, enabled: Boolean): Boolean = { + def warning = + numa_nodes() match { + case ns if ns.length < 2 => Some("no NUMA nodes available") + case ns if !numactl_ok(ns.head) => Some("bad numactl tool") + case _ => None + } + + enabled && + (warning match { + case Some(s) => + progress.echo_warning("Shuffling of NUMA CPU nodes is disabled: " + s) + false + case _ => true + }) + } + + + /* SQL data model */ + + object Data { + def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table = + SQL.Table("isabelle_host" + if_proper(name, "_" + name), columns, body = body) + + object Node_Info { + val hostname = SQL.Column.string("hostname").make_primary_key + val numa_index = SQL.Column.int("numa_index") + + val table = make_table("node_info", List(hostname, numa_index)) + } + + def read_numa_index(db: SQL.Database, hostname: String): Int = + db.using_statement( + Node_Info.table.select(List(Node_Info.numa_index), + sql = Node_Info.hostname.where_equal(hostname)) + )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_index)).nextOption.getOrElse(0)) + + def update_numa_index(db: SQL.Database, hostname: String, numa_index: Int): Boolean = + if (read_numa_index(db, hostname) != numa_index) { + db.using_statement( + Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)) + )(_.execute()) + db.using_statement(Node_Info.table.insert()) { stmt => + stmt.string(1) = hostname + stmt.int(2) = numa_index + stmt.execute() + } + true + } + else false + } +} diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/System/numa.scala --- a/src/Pure/System/numa.scala Thu Mar 02 11:34:54 2023 +0000 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,78 +0,0 @@ -/* Title: Pure/System/numa.scala - Author: Makarius - -Support for Non-Uniform Memory Access of separate CPU nodes. -*/ - -package isabelle - - -object NUMA { - /* information about nodes */ - - private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online") - - private val Info_Single = """^(\d+)$""".r - private val Info_Multiple = """^(\d+)-(\d+)$""".r - - private def parse_nodes(s: String): List[Int] = - s match { - case Info_Single(Value.Int(i)) => List(i) - case Info_Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList - case _ => error("Cannot parse CPU node specification: " + quote(s)) - } - - def nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = { - val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None - for { - path <- numa_info.toList - if enabled && ssh.is_file(path) - s <- space_explode(',', ssh.read(path).trim) - n <- parse_nodes(s) - } yield n - } - - - /* CPU policy via numactl tool */ - - def numactl(node: Int): String = "numactl -m" + node + " -N" + node - def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok - - def policy(node: Int): String = if (numactl_ok(node)) numactl(node) else "" - - def policy_options(options: Options, numa_node: Option[Int]): Options = - numa_node match { - case None => options - case Some(n) => options.string("ML_process_policy") = policy(n) - } - - def perhaps_policy_options(options: Options): Options = { - val numa_node = - try { - nodes() match { - case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head) - case _ => None - } - } - catch { case ERROR(_) => None } - policy_options(options, numa_node) - } - - - /* shuffling of CPU nodes */ - - def check(progress: Progress, enabled: Boolean): Boolean = { - def warning = - nodes() match { - case ns if ns.length < 2 => Some("no NUMA nodes available") - case ns if !numactl_ok(ns.head) => Some("bad numactl tool") - case _ => None - } - - enabled && - (warning match { - case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false - case _ => true - }) - } -} diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/Thy/sessions.scala Thu Mar 02 17:46:29 2023 +0100 @@ -1484,13 +1484,13 @@ database_server && { try_open_database(name) match { case Some(db) => - try { + using(db) { db => db.transaction { val relevant_db = session_info_defined(db, name) init_session_info(db, name) relevant_db } - } finally { db.close() } + } case None => false } } @@ -1508,6 +1508,37 @@ (relevant, ok) } + def init_output(name: String): Unit = { + clean_output(name) + using(open_database(name, output = true))(init_session_info(_, name)) + } + + def check_output( + name: String, + sources_shasum: SHA1.Shasum, + input_shasum: SHA1.Shasum, + fresh_build: Boolean, + store_heap: Boolean + ): (Boolean, SHA1.Shasum) = { + try_open_database(name) match { + case Some(db) => + using(db)(read_build(_, name)) match { + case Some(build) => + val output_shasum = find_heap_shasum(name) + val current = + !fresh_build && + build.ok && + build.sources == sources_shasum && + build.input_heaps == input_shasum && + build.output_heap == output_shasum && + !(store_heap && output_shasum.is_empty) + (current, output_shasum) + case None => (false, SHA1.no_shasum) + } + case None => (false, SHA1.no_shasum) + } + } + /* SQL database content */ @@ -1591,8 +1622,8 @@ def read_session_timing(db: SQL.Database, name: String): Properties.T = Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache) - def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = - read_properties(db, name, Session_Info.command_timings) + def read_command_timings(db: SQL.Database, name: String): Bytes = + read_bytes(db, name, Session_Info.command_timings) def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.theory_timings) diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/Tools/build.scala Thu Mar 02 17:46:29 2023 +0100 @@ -13,7 +13,7 @@ object Results { def apply(context: Build_Process.Context, results: Map[String, Process_Result]): Results = - new Results(context.store, context.deps, results) + new Results(context.store, context.build_deps, results) } class Results private( @@ -317,7 +317,7 @@ clean_build = clean_build, dirs = dirs, select_dirs = select_dirs, - numa_shuffling = NUMA.check(progress, numa_shuffling), + numa_shuffling = Host.numa_check(progress, numa_shuffling), max_jobs = max_jobs, list_files = list_files, check_keywords = check_keywords, diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/Tools/build_job.scala Thu Mar 02 17:46:29 2023 +0100 @@ -13,25 +13,21 @@ trait Build_Job { def job_name: String - def node_info: Build_Job.Node_Info - def start(): Unit = () - def terminate(): Unit = () + def node_info: Host.Node_Info + def cancel(): Unit = () def is_finished: Boolean = false - def finish: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) + def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum) def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, node_info) } object Build_Job { - object Node_Info { def none: Node_Info = Node_Info("", None) } - sealed case class Node_Info(hostname: String, numa_node: Option[Int]) - - sealed case class Result(node_info: Node_Info, process_result: Process_Result) { + sealed case class Result(node_info: Host.Node_Info, process_result: Process_Result) { def ok: Boolean = process_result.ok } sealed case class Abstract( override val job_name: String, - override val node_info: Node_Info + override val node_info: Host.Node_Info ) extends Build_Job { override def make_abstract: Abstract = this } @@ -39,38 +35,106 @@ /* build session */ - class Build_Session( - progress: Progress, - verbose: Boolean, + def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name) + + def start_session( + build_context: Build_Process.Context, session_background: Sessions.Background, - session_heaps: List[Path], - store: Sessions.Store, - do_store: Boolean, - resources: Resources, - session_setup: (String, Session) => Unit, - sources_shasum: SHA1.Shasum, - input_heaps: SHA1.Shasum, - override val node_info: Node_Info + input_shasum: SHA1.Shasum, + node_info: Host.Node_Info + ): Session_Job = new Session_Job(build_context, session_background, input_shasum, node_info) + + object Session_Context { + def load( + name: String, + deps: List[String], + ancestors: List[String], + sources_shasum: SHA1.Shasum, + timeout: Time, + store: Sessions.Store, + progress: Progress = new Progress + ): Session_Context = { + def default: Session_Context = + new Session_Context(name, deps, ancestors, sources_shasum, timeout, Time.zero, Bytes.empty) + + store.try_open_database(name) match { + case None => default + case Some(db) => + def ignore_error(msg: String) = { + progress.echo_warning( + "Ignoring bad database " + db + " for session " + quote(name) + + if_proper(msg, ":\n" + msg)) + default + } + try { + val command_timings = store.read_command_timings(db, name) + val elapsed = + store.read_session_timing(db, name) match { + case Markup.Elapsed(s) => Time.seconds(s) + case _ => Time.zero + } + new Session_Context( + name, deps, ancestors, sources_shasum, timeout, elapsed, command_timings) + } + catch { + case ERROR(msg) => ignore_error(msg) + case exn: java.lang.Error => ignore_error(Exn.message(exn)) + case _: XML.Error => ignore_error("XML.Error") + } + finally { db.close() } + } + } + } + + final class Session_Context( + val name: String, + val deps: List[String], + val ancestors: List[String], + val sources_shasum: SHA1.Shasum, + val timeout: Time, + val old_time: Time, + val old_command_timings_blob: Bytes + ) { + override def toString: String = name + } + + class Session_Job private[Build_Job]( + build_context: Build_Process.Context, + session_background: Sessions.Background, + input_shasum: SHA1.Shasum, + override val node_info: Host.Node_Info ) extends Build_Job { + private val store = build_context.store + private val progress = build_context.progress + private val verbose = build_context.verbose + def session_name: String = session_background.session_name def job_name: String = session_name val info: Sessions.Info = session_background.sessions_structure(session_name) - val options: Options = NUMA.policy_options(info.options, node_info.numa_node) + val options: Options = Host.process_policy_options(info.options, node_info.numa_node) val session_sources: Sessions.Sources = Sessions.Sources.load(session_background.base, cache = store.cache.compress) - private lazy val future_result: Future[Process_Result] = + val store_heap = build_context.store_heap(session_name) + + private val future_result: Future[(Process_Result, SHA1.Shasum)] = Future.thread("build", uninterruptible = true) { val env = Isabelle_System.settings( List("ISABELLE_ML_DEBUGGER" -> options.bool("ML_debugger").toString)) + val session_heaps = + session_background.info.parent match { + case None => Nil + case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic) + } + val use_prelude = if (session_heaps.isEmpty) Thy_Header.ml_roots.map(_._1) else Nil val eval_store = - if (do_store) { + if (store_heap) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(session_name)))) @@ -97,6 +161,13 @@ } } + + /* session */ + + val resources = + new Resources(session_background, log = build_context.log, + command_timings = build_context.old_command_timings(session_name)) + val session = new Session(options, resources) { override val cache: Term.Cache = store.cache @@ -261,14 +332,20 @@ case _ => } - session_setup(session_name, session) + build_context.session_setup(session_name, session) val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) - val process = { + + /* process */ + + val process = Isabelle_Process.start(options, session, session_background, session_heaps, use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env) - } + + val timeout_request: Option[Event_Timer.Request] = + if (info.timeout_ignored) None + else Some(Event_Timer.request(Time.now() + info.timeout) { process.terminate() }) val build_errors = Isabelle_Thread.interrupt_handler(_ => process.terminate()) { @@ -290,9 +367,15 @@ } } - val process_result = + val result0 = Isabelle_Thread.interrupt_handler(_ => process.terminate()) { process.await_shutdown() } + val was_timeout = + timeout_request match { + case None => false + case Some(request) => !request.cancel() + } + session.stop() val export_errors = @@ -300,7 +383,7 @@ val (document_output, document_errors) = try { - if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { + if (build_errors.isInstanceOf[Exn.Res[_]] && result0.ok && info.documents.nonEmpty) { using(Export.open_database_context(store)) { database_context => val documents = using(database_context.open_session(session_background)) { @@ -322,7 +405,10 @@ case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } - val result = { + + /* process result */ + + val result1 = { val theory_timing = theory_timings.iterator.flatMap( { @@ -342,111 +428,102 @@ task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) ::: document_output - process_result.output(more_output) + result0.output(more_output) .error(Library.trim_line(stderr.toString)) .errors_rc(export_errors ::: document_errors) } - build_errors match { - case Exn.Res(build_errs) => - val errs = build_errs ::: document_errors - if (errs.nonEmpty) { - result.error_rc.output( - errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: - errs.map(Protocol.Error_Message_Marker.apply)) - } - else if (progress.stopped && result.ok) result.copy(rc = Process_Result.RC.interrupt) - else result - case Exn.Exn(Exn.Interrupt()) => - if (result.ok) result.copy(rc = Process_Result.RC.interrupt) - else result - case Exn.Exn(exn) => throw exn - } - } - - override def start(): Unit = future_result - override def terminate(): Unit = future_result.cancel() - override def is_finished: Boolean = future_result.is_finished - - private val timeout_request: Option[Event_Timer.Request] = { - if (info.timeout_ignored) None - else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) - } - - override lazy val finish: (Process_Result, SHA1.Shasum) = { - val process_result = { - val result = future_result.join - - val was_timeout = - timeout_request match { - case None => false - case Some(request) => !request.cancel() + val result2 = + build_errors match { + case Exn.Res(build_errs) => + val errs = build_errs ::: document_errors + if (errs.nonEmpty) { + result1.error_rc.output( + errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: + errs.map(Protocol.Error_Message_Marker.apply)) + } + else if (progress.stopped && result1.ok) result1.copy(rc = Process_Result.RC.interrupt) + else result1 + case Exn.Exn(Exn.Interrupt()) => + if (result1.ok) result1.copy(rc = Process_Result.RC.interrupt) + else result1 + case Exn.Exn(exn) => throw exn } - if (result.ok) result - else if (was_timeout) result.error(Output.error_message_text("Timeout")).timeout_rc - else if (result.interrupted) result.error(Output.error_message_text("Interrupt")) - else result + val process_result = + if (result2.ok) result2 + else if (was_timeout) result2.error(Output.error_message_text("Timeout")).timeout_rc + else if (result2.interrupted) result2.error(Output.error_message_text("Interrupt")) + else result2 + + + /* output heap */ + + val output_shasum = + if (process_result.ok && store_heap && store.output_heap(session_name).is_file) { + SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) + } + else SHA1.no_shasum + + val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) + + val build_log = + Build_Log.Log_File(session_name, process_result.out_lines). + parse_session_info( + command_timings = true, + theory_timings = true, + ml_statistics = true, + task_statistics = true) + + // write log file + if (process_result.ok) { + File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) + } + else File.write(store.output_log(session_name), terminate_lines(log_lines)) + + // write database + using(store.open_database(session_name, output = true))(db => + store.write_session_info(db, session_name, session_sources, + build_log = + if (process_result.timeout) build_log.error("Timeout") else build_log, + build = + Sessions.Build_Info( + sources = build_context.sources_shasum(session_name), + input_heaps = input_shasum, + output_heap = output_shasum, + process_result.rc, build_context.uuid))) + + // messages + process_result.err_lines.foreach(progress.echo) + + if (process_result.ok) { + if (verbose) { + val props = build_log.session_timing + val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 + val timing = Markup.Timing_Properties.get(props) + progress.echo( + "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")") + } + progress.echo( + "Finished " + session_name + " (" + process_result.timing.message_resources + ")") + } + else { + progress.echo( + session_name + " FAILED (see also \"isabelle log -H Error " + session_name + "\")") + if (!process_result.interrupted) { + val tail = info.options.int("process_output_tail") + val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0) + val prefix = if (log_lines.length == suffix.length) Nil else List("...") + progress.echo(Library.trim_line(cat_lines(prefix ::: suffix))) + } + } + + (process_result.copy(out_lines = log_lines), output_shasum) } - val output_heap = - if (process_result.ok && do_store && store.output_heap(session_name).is_file) { - SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) - } - else SHA1.no_shasum - - val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) - - val build_log = - Build_Log.Log_File(session_name, process_result.out_lines). - parse_session_info( - command_timings = true, - theory_timings = true, - ml_statistics = true, - task_statistics = true) - - // write log file - if (process_result.ok) { - File.write_gzip(store.output_log_gz(session_name), terminate_lines(log_lines)) - } - else File.write(store.output_log(session_name), terminate_lines(log_lines)) - - // write database - using(store.open_database(session_name, output = true))(db => - store.write_session_info(db, session_name, session_sources, - build_log = - if (process_result.timeout) build_log.error("Timeout") else build_log, - build = - Sessions.Build_Info(sources_shasum, input_heaps, output_heap, - process_result.rc, UUID.random().toString))) - - // messages - process_result.err_lines.foreach(progress.echo) - - if (process_result.ok) { - if (verbose) { - val props = build_log.session_timing - val threads = Markup.Session_Timing.Threads.unapply(props) getOrElse 1 - val timing = Markup.Timing_Properties.get(props) - progress.echo( - "Timing " + session_name + " (" + threads + " threads, " + timing.message_factor + ")") - } - progress.echo( - "Finished " + session_name + " (" + process_result.timing.message_resources + ")") - } - else { - progress.echo( - session_name + " FAILED (see also \"isabelle log -H Error " + session_name + "\")") - if (!process_result.interrupted) { - val tail = info.options.int("process_output_tail") - val suffix = if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0) - val prefix = if (log_lines.length == suffix.length) Nil else List("...") - progress.echo(Library.trim_line(cat_lines(prefix ::: suffix))) - } - } - - (process_result.copy(out_lines = log_lines), output_heap) - } + override def cancel(): Unit = future_result.cancel() + override def is_finished: Boolean = future_result.is_finished + override def join: (Process_Result, SHA1.Shasum) = future_result.join } diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/Tools/build_process.scala --- a/src/Pure/Tools/build_process.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/Tools/build_process.scala Thu Mar 02 17:46:29 2023 +0100 @@ -13,60 +13,12 @@ object Build_Process { - /* static context */ - - object Session_Context { - def empty(session: String, timeout: Time): Session_Context = - new Session_Context(session, timeout, Time.zero, Nil) - - def apply( - session: String, - timeout: Time, - store: Sessions.Store, - progress: Progress = new Progress - ): Session_Context = { - store.try_open_database(session) match { - case None => empty(session, timeout) - case Some(db) => - def ignore_error(msg: String) = { - progress.echo_warning("Ignoring bad database " + db + - " for session " + quote(session) + (if (msg == "") "" else ":\n" + msg)) - empty(session, timeout) - } - try { - val command_timings = store.read_command_timings(db, session) - val elapsed = - store.read_session_timing(db, session) match { - case Markup.Elapsed(s) => Time.seconds(s) - case _ => Time.zero - } - new Session_Context(session, timeout, elapsed, command_timings) - } - catch { - case ERROR(msg) => ignore_error(msg) - case exn: java.lang.Error => ignore_error(Exn.message(exn)) - case _: XML.Error => ignore_error("XML.Error") - } - finally { db.close() } - } - } - } - - final class Session_Context( - val session: String, - val timeout: Time, - val old_time: Time, - val old_command_timings: List[Properties.T] - ) { - def is_empty: Boolean = old_time.is_zero && old_command_timings.isEmpty - - override def toString: String = session - } + /** static context **/ object Context { def apply( store: Sessions.Store, - deps: Sessions.Deps, + build_deps: Sessions.Deps, progress: Progress = new Progress, hostname: String = Isabelle_System.hostname(), numa_shuffling: Boolean = false, @@ -76,17 +28,22 @@ no_build: Boolean = false, verbose: Boolean = false, session_setup: (String, Session) => Unit = (_, _) => (), - instance: String = UUID.random().toString + uuid: String = UUID.random().toString ): Context = { - val sessions_structure = deps.sessions_structure + val sessions_structure = build_deps.sessions_structure val build_graph = sessions_structure.build_graph val sessions = Map.from( - for (name <- build_graph.keys_iterator) + for ((name, (info, _)) <- build_graph.iterator) yield { - val timeout = sessions_structure(name).timeout - name -> Build_Process.Session_Context(name, timeout, store, progress = progress) + val deps = info.parent.toList + val ancestors = sessions_structure.build_requirements(deps) + val sources_shasum = build_deps.sources_shasum(name) + val session_context = + Build_Job.Session_Context.load( + name, deps, ancestors, sources_shasum, info.timeout, store, progress = progress) + name -> session_context }) val sessions_time = { @@ -121,18 +78,17 @@ } } - val numa_nodes = NUMA.nodes(enabled = numa_shuffling) - new Context(instance, store, deps, sessions, ordering, progress, hostname, numa_nodes, + val numa_nodes = Host.numa_nodes(enabled = numa_shuffling) + new Context(store, build_deps, sessions, ordering, progress, hostname, numa_nodes, build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build, - no_build = no_build, verbose = verbose, session_setup) + no_build = no_build, verbose = verbose, session_setup, uuid = uuid) } } final class Context private( - val instance: String, val store: Sessions.Store, - val deps: Sessions.Deps, - sessions: Map[String, Session_Context], + val build_deps: Sessions.Deps, + val sessions: Map[String, Build_Job.Session_Context], val ordering: Ordering[String], val progress: Progress, val hostname: String, @@ -143,18 +99,36 @@ val no_build: Boolean, val verbose: Boolean, val session_setup: (String, Session) => Unit, + val uuid: String ) { - def sessions_structure: Sessions.Structure = deps.sessions_structure + def build_options: Options = store.options + + val log: Logger = + build_options.string("system_log") match { + case "" => No_Logger + case "-" => Logger.make(progress) + case log_file => Logger.make(Some(Path.explode(log_file))) + } + + def sessions_structure: Sessions.Structure = build_deps.sessions_structure - def apply(session: String): Session_Context = - sessions.getOrElse(session, Session_Context.empty(session, Time.zero)) + def sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum - def do_store(session: String): Boolean = - build_heap || Sessions.is_pure(session) || !sessions_structure.build_graph.is_maximal(session) + def old_command_timings(name: String): List[Properties.T] = + sessions.get(name) match { + case Some(session_context) => + Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache) + case None => Nil + } + + def store_heap(name: String): Boolean = + build_heap || Sessions.is_pure(name) || + sessions.valuesIterator.exists(_.ancestors.contains(name)) } - /* dynamic state */ + + /** dynamic state **/ case class Entry(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) { def is_ready: Boolean = deps.isEmpty @@ -163,10 +137,10 @@ } case class Result( - current: Boolean, - output_heap: SHA1.Shasum, - node_info: Build_Job.Node_Info, - process_result: Process_Result + process_result: Process_Result, + output_shasum: SHA1.Shasum, + node_info: Host.Node_Info, + current: Boolean ) { def ok: Boolean = process_result.ok } @@ -199,7 +173,7 @@ def is_running(name: String): Boolean = running.isDefinedAt(name) - def stop_running(): Unit = running.valuesIterator.foreach(_.terminate()) + def stop_running(): Unit = running.valuesIterator.foreach(_.cancel()) def finished_running(): List[Build_Job] = List.from(running.valuesIterator.filter(_.is_finished)) @@ -212,21 +186,19 @@ def make_result( name: String, - current: Boolean, - output_heap: SHA1.Shasum, process_result: Process_Result, - node_info: Build_Job.Node_Info = Build_Job.Node_Info.none + output_shasum: SHA1.Shasum, + node_info: Host.Node_Info = Host.Node_Info.none, + current: Boolean = false ): State = { - val result = Build_Process.Result(current, output_heap, node_info, process_result) - copy(results = results + (name -> result)) + val entry = name -> Build_Process.Result(process_result, output_shasum, node_info, current) + copy(results = results + entry) } - - def get_results(names: List[String]): List[Build_Process.Result] = - names.map(results.apply) } - /* SQL data model */ + + /** SQL data model **/ object Data { val database = Path.explode("$ISABELLE_HOME_USER/build.db") @@ -235,26 +207,26 @@ SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body) object Generic { - val instance = SQL.Column.string("instance") + val uuid = SQL.Column.string("uuid") val name = SQL.Column.string("name") - def sql_equal(instance: String = "", name: String = ""): SQL.Source = + def sql_equal(uuid: String = "", name: String = ""): SQL.Source = SQL.and( - if_proper(instance, Generic.instance.equal(instance)), + if_proper(uuid, Generic.uuid.equal(uuid)), if_proper(name, Generic.name.equal(name))) - def sql_member(instance: String = "", names: Iterable[String] = Nil): SQL.Source = + def sql_member(uuid: String = "", names: Iterable[String] = Nil): SQL.Source = SQL.and( - if_proper(instance, Generic.instance.equal(instance)), + if_proper(uuid, Generic.uuid.equal(uuid)), if_proper(names, Generic.name.member(names))) } object Base { - val instance = Generic.instance.make_primary_key + val uuid = Generic.uuid.make_primary_key val ml_platform = SQL.Column.string("ml_platform") val options = SQL.Column.string("options") - val table = make_table("", List(instance, ml_platform, options)) + val table = make_table("", List(uuid, ml_platform, options)) } object Serial { @@ -263,13 +235,6 @@ val table = make_table("serial", List(serial)) } - object Node_Info { - val hostname = SQL.Column.string("hostname").make_primary_key - val numa_index = SQL.Column.int("numa_index") - - val table = make_table("node_info", List(hostname, numa_index)) - } - object Pending { val name = Generic.name.make_primary_key val deps = SQL.Column.string("deps") @@ -315,26 +280,6 @@ } } - def read_numa_index(db: SQL.Database, hostname: String): Int = - db.using_statement( - Node_Info.table.select(List(Node_Info.numa_index), - sql = Node_Info.hostname.where_equal(hostname)) - )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_index)).nextOption.getOrElse(0)) - - def update_numa_index(db: SQL.Database, hostname: String, numa_index: Int): Boolean = - if (read_numa_index(db, hostname) != numa_index) { - db.using_statement( - Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname)) - )(_.execute()) - db.using_statement(Node_Info.table.insert()) { stmt => - stmt.string(1) = hostname - stmt.int(2) = numa_index - stmt.execute() - } - true - } - else false - def read_pending(db: SQL.Database): List[Entry] = db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt => List.from( @@ -375,7 +320,7 @@ val name = res.string(Running.name) val hostname = res.string(Running.hostname) val numa_node = res.get_int(Running.numa_node) - Build_Job.Abstract(name, Build_Job.Node_Info(hostname, numa_node)) + Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node)) }) } @@ -417,7 +362,7 @@ val timing_elapsed = res.long(Results.timing_elapsed) val timing_cpu = res.long(Results.timing_cpu) val timing_gc = res.long(Results.timing_gc) - val node_info = Build_Job.Node_Info(hostname, numa_node) + val node_info = Host.Node_Info(hostname, numa_node) val process_result = Process_Result(rc, out_lines = split_lines(out), @@ -460,10 +405,10 @@ List( Base.table, Serial.table, - Node_Info.table, Pending.table, Running.table, - Results.table) + Results.table, + Host.Data.Node_Info.table) for (table <- tables) db.create_table(table) @@ -476,7 +421,7 @@ for (table <- tables) db.using_statement(table.delete())(_.execute()) db.using_statement(Base.table.insert()) { stmt => - stmt.string(1) = build_context.instance + stmt.string(1) = build_context.uuid stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM") stmt.string(3) = build_context.store.options.make_prefs(Options.init(prefs = "")) stmt.execute() @@ -485,16 +430,16 @@ def update_database( db: SQL.Database, - instance: String, + uuid: String, hostname: String, state: State ): State = { val changed = List( - update_numa_index(db, hostname, state.numa_index), update_pending(db, state.pending), update_running(db, state.running), - update_results(db, state.results)) + update_results(db, state.results), + Host.Data.update_numa_index(db, hostname, state.numa_index)) val serial0 = get_serial(db) val serial = if (changed.exists(identity)) serial0 + 1 else serial0 @@ -506,23 +451,25 @@ } -/* main process */ + +/** main process **/ -class Build_Process(protected val build_context: Build_Process.Context) extends AutoCloseable { +class Build_Process(protected val build_context: Build_Process.Context) +extends AutoCloseable { + /* context */ + protected val store: Sessions.Store = build_context.store protected val build_options: Options = store.options - protected val build_deps: Sessions.Deps = build_context.deps + protected val build_deps: Sessions.Deps = build_context.build_deps protected val progress: Progress = build_context.progress protected val verbose: Boolean = build_context.verbose - protected val log: Logger = - build_options.string("system_log") match { - case "" => No_Logger - case "-" => Logger.make(progress) - case log_file => Logger.make(Some(Path.explode(log_file))) - } + + /* global state: internal var vs. external database */ - protected val database: Option[SQL.Database] = + private var _state: Build_Process.State = init_state(Build_Process.State()) + + private val _database: Option[SQL.Database] = if (!build_options.bool("build_database_test")) None else if (store.database_server) Some(store.open_database_server()) else { @@ -532,149 +479,130 @@ Some(db) } - def close(): Unit = database.foreach(_.close()) + def close(): Unit = synchronized { _database.foreach(_.close()) } + + private def setup_database(): Unit = + synchronized { + for (db <- _database) { + db.transaction { Build_Process.Data.init_database(db, build_context) } + db.rebuild() + } + } - // global state - protected var _state: Build_Process.State = init_state(Build_Process.State()) + protected def synchronized_database[A](body: => A): A = + synchronized { + _database match { + case None => body + case Some(db) => db.transaction { body } + } + } + + private def sync_database(): Unit = + synchronized_database { + for (db <- _database) { + _state = + Build_Process.Data.update_database( + db, build_context.uuid, build_context.hostname, _state) + } + } + + + /* policy operations */ protected def init_state(state: Build_Process.State): Build_Process.State = { val old_pending = state.pending.iterator.map(_.name).toSet val new_pending = List.from( for { - (name, (_, (preds, _))) <- build_context.sessions_structure.build_graph.iterator + (name, session_context) <- build_context.sessions.iterator if !old_pending(name) - } yield Build_Process.Entry(name, preds.toList)) + } yield Build_Process.Entry(name, session_context.deps)) state.copy(pending = new_pending ::: state.pending) } - protected def next_pending(): Option[String] = synchronized { - if (_state.running.size < (build_context.max_jobs max 1)) { - _state.pending.filter(entry => entry.is_ready && !_state.is_running(entry.name)) + protected def next_job(state: Build_Process.State): Option[String] = + if (state.running.size < (build_context.max_jobs max 1)) { + state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name)) .sortBy(_.name)(build_context.ordering) .headOption.map(_.name) } else None - } - protected def start_job(session_name: String): Unit = { - val ancestor_results = synchronized { - _state.get_results( - build_deps.sessions_structure.build_requirements(List(session_name)). - filterNot(_ == session_name)) - } - val input_heaps = + protected def start_session(state: Build_Process.State, session_name: String): Build_Process.State = { + val ancestor_results = + for (a <- build_context.sessions(session_name).ancestors) yield state.results(a) + + val input_shasum = if (ancestor_results.isEmpty) { SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) } - else SHA1.flat_shasum(ancestor_results.map(_.output_heap)) + else SHA1.flat_shasum(ancestor_results.map(_.output_shasum)) + + val store_heap = build_context.store_heap(session_name) - val do_store = build_context.do_store(session_name) - val (current, output_heap) = { - store.try_open_database(session_name) match { - case Some(db) => - using(db)(store.read_build(_, session_name)) match { - case Some(build) => - val output_heap = store.find_heap_shasum(session_name) - val current = - !build_context.fresh_build && - build.ok && - build.sources == build_deps.sources_shasum(session_name) && - build.input_heaps == input_heaps && - build.output_heap == output_heap && - !(do_store && output_heap.is_empty) - (current, output_heap) - case None => (false, SHA1.no_shasum) - } - case None => (false, SHA1.no_shasum) - } - } + val (current, output_shasum) = + store.check_output(session_name, + sources_shasum = build_context.sources_shasum(session_name), + input_shasum = input_shasum, + fresh_build = build_context.fresh_build, + store_heap = store_heap) + val all_current = current && ancestor_results.forall(_.current) if (all_current) { - synchronized { - _state = _state. - remove_pending(session_name). - make_result(session_name, true, output_heap, Process_Result.ok) - } + state + .remove_pending(session_name) + .make_result(session_name, Process_Result.ok, output_shasum, current = true) } else if (build_context.no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") - synchronized { - _state = _state. - remove_pending(session_name). - make_result(session_name, false, output_heap, Process_Result.error) - } + state. + remove_pending(session_name). + make_result(session_name, Process_Result.error, output_shasum) } - else if (ancestor_results.forall(_.ok) && !progress.stopped) { - progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") - - store.clean_output(session_name) - using(store.open_database(session_name, output = true))( - store.init_session_info(_, session_name)) - - val session_background = build_deps.background(session_name) - val session_heaps = - session_background.info.parent match { - case None => Nil - case Some(logic) => ML_Process.session_heaps(store, session_background, logic = logic) - } - - val resources = - new Resources(session_background, log = log, - command_timings = build_context(session_name).old_command_timings) - - val job = - synchronized { - val (numa_node, state1) = _state.numa_next(build_context.numa_nodes) - val node_info = Build_Job.Node_Info(build_context.hostname, numa_node) - val job = - new Build_Job.Build_Session(progress, verbose, session_background, session_heaps, - store, do_store, resources, build_context.session_setup, - build_deps.sources_shasum(session_name), input_heaps, node_info) - _state = state1.add_running(session_name, job) - job - } - job.start() + else if (!ancestor_results.forall(_.ok) || progress.stopped) { + progress.echo(session_name + " CANCELLED") + state + .remove_pending(session_name) + .make_result(session_name, Process_Result.undefined, output_shasum) } else { - progress.echo(session_name + " CANCELLED") - synchronized { - _state = _state. - remove_pending(session_name). - make_result(session_name, false, output_heap, Process_Result.undefined) - } + progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...") + + store.init_output(session_name) + + val (numa_node, state1) = state.numa_next(build_context.numa_nodes) + val node_info = Host.Node_Info(build_context.hostname, numa_node) + val job = + Build_Job.start_session( + build_context, build_deps.background(session_name), input_shasum, node_info) + state1.add_running(session_name, job) } } - protected def setup_database(): Unit = - for (db <- database) { - synchronized { - db.transaction { - Build_Process.Data.init_database(db, build_context) - } + + /* run */ + + def run(): Map[String, Process_Result] = { + def finished(): Boolean = synchronized_database { _state.finished } + + def sleep(): Unit = + Isabelle_Thread.interrupt_handler(_ => progress.stop()) { + build_options.seconds("editor_input_delay").sleep() } - db.rebuild() - } - protected def sync_database(): Unit = - for (db <- database) { - synchronized { - db.transaction { - _state = - Build_Process.Data.update_database( - db, build_context.instance, build_context.hostname, _state) - } + + def start(): Boolean = synchronized_database { + next_job(_state) match { + case Some(name) => + if (Build_Job.is_session_name(name)) { + _state = start_session(_state, name) + true + } + else error("Unsupported build job name " + quote(name)) + case None => false } } - protected def sleep(): Unit = - Isabelle_Thread.interrupt_handler(_ => progress.stop()) { - build_options.seconds("editor_input_delay").sleep() - } - - def run(): Map[String, Process_Result] = { - def finished(): Boolean = synchronized { _state.finished } - if (finished()) { progress.echo_warning("Nothing to build") Map.empty[String, Process_Result] @@ -682,28 +610,26 @@ else { setup_database() while (!finished()) { - if (progress.stopped) synchronized { _state.stop_running() } + if (progress.stopped) synchronized_database { _state.stop_running() } - for (job <- synchronized { _state.finished_running() }) { + for (job <- synchronized_database { _state.finished_running() }) { val job_name = job.job_name - val (process_result, output_heap) = job.finish - synchronized { + val (process_result, output_shasum) = job.join + synchronized_database { _state = _state. remove_pending(job_name). remove_running(job_name). - make_result(job_name, false, output_heap, process_result, node_info = job.node_info) + make_result(job_name, process_result, output_shasum, node_info = job.node_info) } } - next_pending() match { - case Some(name) => - start_job(name) - case None => - sync_database() - sleep() + if (!start()) { + sync_database() + sleep() } } - synchronized { + + synchronized_database { for ((name, result) <- _state.results) yield name -> result.process_result } } diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/Tools/dump.scala Thu Mar 02 17:46:29 2023 +0100 @@ -98,7 +98,7 @@ ): Context = { val session_options: Options = { val options1 = - NUMA.perhaps_policy_options(options) + + Host.perhaps_process_policy_options(options) + "parallel_proofs=0" + "completion_limit=0" + "editor_tracing_messages=0" diff -r df1150ec6cd7 -r 57ede1743caf src/Pure/Tools/update.scala --- a/src/Pure/Tools/update.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Pure/Tools/update.scala Thu Mar 02 17:46:29 2023 +0100 @@ -220,7 +220,7 @@ clean_build, dirs = dirs, select_dirs = select_dirs, - numa_shuffling = NUMA.check(progress, numa_shuffling), + numa_shuffling = Host.numa_check(progress, numa_shuffling), max_jobs = max_jobs, fresh_build, no_build = no_build, diff -r df1150ec6cd7 -r 57ede1743caf src/Tools/VSCode/src/vscode_main.scala --- a/src/Tools/VSCode/src/vscode_main.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Tools/VSCode/src/vscode_main.scala Thu Mar 02 17:46:29 2023 +0100 @@ -203,7 +203,7 @@ -m MODE add print mode for output -n no build of session image on startup -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -p CMD ML process command prefix (process policy) + -p CMD command prefix for ML process (e.g. NUMA policy) -s system build mode for session image (system_heaps=true) -u user build mode for session image (system_heaps=false) -v verbose logging of language server @@ -226,7 +226,7 @@ "m:" -> (arg => modes = modes ::: List(arg)), "n" -> (_ => no_build = true), "o:" -> add_option, - "p:" -> (arg => add_option("ML_process_policy=" + arg)), + "p:" -> (arg => add_option("process_policy=" + arg)), "s" -> (_ => add_option("system_heaps=true")), "u" -> (_ => add_option("system_heaps=false")), "v" -> (_ => verbose = true)) diff -r df1150ec6cd7 -r 57ede1743caf src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Tools/jEdit/lib/Tools/jedit Thu Mar 02 17:46:29 2023 +0100 @@ -28,7 +28,7 @@ echo " -l NAME logic session name" echo " -m MODE add print mode for output" echo " -n no build of session image on startup" - echo " -p CMD ML process command prefix (process policy)" + echo " -p CMD command prefix for ML process (e.g. NUMA policy)" echo " -s system build mode for session image (system_heaps=true)" echo " -u user build mode for session image (system_heaps=false)" echo @@ -56,7 +56,7 @@ BUILD_ONLY=false BUILD_OPTIONS="" -ML_PROCESS_POLICY="" +PROCESS_POLICY="" JEDIT_LOGIC_ANCESTOR="" JEDIT_LOGIC_REQUIREMENTS="" JEDIT_INCLUDE_SESSIONS="" @@ -119,7 +119,7 @@ JEDIT_NO_BUILD="true" ;; p) - ML_PROCESS_POLICY="$OPTARG" + PROCESS_POLICY="$OPTARG" ;; s) JEDIT_BUILD_MODE="system" @@ -163,7 +163,7 @@ export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE - export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" + export JEDIT_PROCESS_POLICY="$PROCESS_POLICY" exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \ "${JAVA_ARGS[@]}" isabelle.jedit.JEdit_Main "${ARGS[@]}" fi diff -r df1150ec6cd7 -r 57ede1743caf src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Mar 02 11:34:54 2023 +0000 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Thu Mar 02 17:46:29 2023 +0100 @@ -28,9 +28,9 @@ } val options2 = - Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match { + Isabelle_System.getenv("JEDIT_PROCESS_POLICY") match { case "" => options1 - case s => options1.string.update("ML_process_policy", s) + case s => options1.string.update("process_policy", s) } options2