--- 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.
--- 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 \
--- 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"
--- 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
--- 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>\<open>-p\<close> 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>\<open>isabelle.jedit_server\<close> provides a different server
--- 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)
}
--- 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] =
--- 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,
--- /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
+ }
+}
--- 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
- })
- }
-}
--- 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)
--- 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,
--- 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
}
--- 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
}
}
--- 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"
--- 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,
--- 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))
--- 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
--- 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