--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Mar 14 10:35:10 2023 +0100
@@ -105,9 +105,7 @@
val isabelle_tool = Isabelle_Tool("mirabelle", "testing tool for automated proof tools",
Scala_Project.here,
{ args =>
- val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
-
- var options = Options.init(opts = build_options)
+ var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
val mirabelle_dry_run = options.check_name("mirabelle_dry_run")
val mirabelle_max_calls = options.check_name("mirabelle_max_calls")
val mirabelle_randomize = options.check_name("mirabelle_randomize")
--- a/src/Pure/ROOT.ML Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/ROOT.ML Tue Mar 14 10:35:10 2023 +0100
@@ -366,3 +366,4 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
+
--- a/src/Pure/System/options.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/System/options.scala Tue Mar 14 10:35:10 2023 +0100
@@ -8,9 +8,30 @@
object Options {
- type Spec = (String, Option[String])
+ val empty: Options = new Options()
+
+ object Spec {
+ def make(s: String): Spec =
+ s match {
+ case Properties.Eq(a, b) => Spec(a, Some(b))
+ case _ => Spec(s)
+ }
- val empty: Options = new Options()
+ def ISABELLE_BUILD_OPTIONS: List[Spec] =
+ Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).map(make)
+ }
+
+ sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) {
+ override def toString: String = name + if_proper(value, "=" + value.get)
+ }
+
+ sealed case class Change(name: String, value: String, unknown: Boolean) {
+ def spec: Spec = Spec(name, Some(value))
+
+ def print_prefs: String =
+ name + " = " + Outer_Syntax.quote_string(value) +
+ if_proper(unknown, " (* unknown *)") + "\n"
+ }
/* typed access */
@@ -150,7 +171,8 @@
val prefs_entry: Parser[Options => Options] = {
option_name ~ ($$$("=") ~! option_value) ^^
- { case a ~ (_ ~ b) => (options: Options) => options.add_permissive(a, b) }
+ { case a ~ (_ ~ b) => (options: Options) =>
+ options + Options.Spec(a, Some(b), permissive = true) }
}
def parse_file(
@@ -177,13 +199,13 @@
def read_prefs(file: Path = PREFS): String =
if (file.is_file) File.read(file) else ""
- def init(prefs: String = read_prefs(PREFS), opts: List[String] = Nil): Options = {
+ def init(prefs: String = read_prefs(file = PREFS), specs: List[Spec] = Nil): Options = {
var options = empty
for {
dir <- Components.directories()
file = dir + OPTIONS if file.is_file
} { options = Parsers.parse_file(options, file.implode, File.read(file)) }
- opts.foldLeft(Parsers.parse_prefs(options, prefs))(_ + _)
+ Parsers.parse_prefs(options, prefs) ++ specs
}
def init0(): Options = init(prefs = "")
@@ -225,10 +247,7 @@
val options = {
val options0 = Options.init()
val options1 =
- if (build_options) {
- Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _)
- }
- else options0
+ if (build_options) options0 ++ Options.Spec.ISABELLE_BUILD_OPTIONS else options0
more_options.foldLeft(options1)(_ + _)
}
@@ -328,9 +347,6 @@
def update(name: String, x: String): Options = put(name, Options.String, x)
}
- def proper_string(name: String): Option[String] =
- Library.proper_string(string(name))
-
def seconds(name: String): Time = Time.seconds(real(name))
@@ -387,37 +403,29 @@
}
}
- def add_permissive(name: String, value: String): Options = {
- if (options.isDefinedAt(name)) this + (name, value)
- else {
+ def + (spec: Options.Spec): Options = {
+ val name = spec.name
+ if (spec.permissive && !options.isDefinedAt(name)) {
+ val value = spec.value.getOrElse("")
val opt =
Options.Entry(false, Position.none, name, Options.Unknown, value, value, None, Nil, "", "")
new Options(options + (name -> opt), section)
}
- }
-
- def + (name: String, value: String): Options = {
- val opt = check_name(name)
- (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name)
- }
-
- def + (name: String, opt_value: Option[String]): Options = {
- val opt = check_name(name)
- opt_value orElse opt.standard_value match {
- case Some(value) => this + (name, value)
- case None if opt.typ == Options.Bool => this + (name, "true")
- case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
+ else {
+ val opt = check_name(name)
+ def put(value: String): Options =
+ (new Options(options + (name -> opt.copy(value = value)), section)).check_value(name)
+ spec.value orElse opt.standard_value match {
+ case Some(value) => put(value)
+ case None if opt.typ == Options.Bool => put("true")
+ case None => error("Missing value for option " + quote(name) + " : " + opt.typ.print)
+ }
}
}
- def + (str: String): Options =
- str match {
- case Properties.Eq(a, b) => this + (a, b)
- case _ => this + (str, None)
- }
+ def + (s: String): Options = this + Options.Spec.make(s)
- def ++ (specs: List[Options.Spec]): Options =
- specs.foldLeft(this) { case (x, (y, z)) => x + (y, z) }
+ def ++ (specs: List[Options.Spec]): Options = specs.foldLeft(this)(_ + _)
/* sections */
@@ -441,20 +449,27 @@
}
+ /* changed options */
+
+ def changed(
+ defaults: Options = Options.init0(),
+ filter: Options.Entry => Boolean = _ => true
+ ): List[Options.Change] = {
+ List.from(
+ for {
+ (name, opt2) <- options.iterator
+ opt1 = defaults.get(name)
+ if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2)
+ } yield Options.Change(name, opt2.value, opt1.isEmpty))
+ }
+
+
/* preferences */
def make_prefs(
defaults: Options = Options.init0(),
filter: Options.Entry => Boolean = _ => true
- ): String = {
- (for {
- (name, opt2) <- options.iterator
- opt1 = defaults.get(name)
- if (opt1.isEmpty || opt1.get.value != opt2.value) && filter(opt2)
- } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else ""))
- .toList.sortBy(_._1)
- .map({ case (x, y, z) => x + " = " + Outer_Syntax.quote_string(y) + z + "\n" }).mkString
- }
+ ): String = changed(defaults = defaults, filter = filter).map(_.print_prefs).mkString
def save_prefs(file: Path = Options.PREFS, defaults: Options = Options.init0()): Unit = {
val prefs = make_prefs(defaults = defaults)
@@ -469,7 +484,7 @@
def value: Options = synchronized { _options }
def change(f: Options => Options): Unit = synchronized { _options = f(_options) }
- def += (name: String, x: String): Unit = change(options => options + (name, x))
+ def += (name: String, x: String): Unit = change(options => options + Options.Spec(name, Some(x)))
val bool: Options.Access_Variable[Boolean] =
new Options.Access_Variable[Boolean](this, _.bool)
@@ -483,8 +498,5 @@
val string: Options.Access_Variable[String] =
new Options.Access_Variable[String](this, _.string)
- def proper_string(name: String): Option[String] =
- Library.proper_string(string(name))
-
def seconds(name: String): Time = value.seconds(name)
}
--- a/src/Pure/Thy/sessions.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Mar 14 10:35:10 2023 +0100
@@ -258,7 +258,6 @@
List(
Info.make(
Chapter_Defs.empty,
- Options.init0(),
info.options,
augment_options = _ => Nil,
dir_selected = false,
@@ -609,7 +608,6 @@
object Info {
def make(
chapter_defs: Chapter_Defs,
- options0: Options,
options: Options,
augment_options: String => List[Options.Spec],
dir_selected: Boolean,
@@ -627,9 +625,10 @@
val session_path = dir + Path.explode(entry.path)
val directories = entry.directories.map(dir => session_path + Path.explode(dir))
- val entry_options = entry.options ::: augment_options(name)
- val session_options = options ++ entry_options
- val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content)
+ val session_options0 = options ++ entry.options
+ val session_options = session_options0 ++ augment_options(name)
+ val session_prefs =
+ session_options.make_prefs(defaults = session_options0, filter = _.session_content)
val theories =
entry.theories.map({ case (opts, thys) =>
@@ -664,7 +663,7 @@
val meta_digest =
SHA1.digest(
- (name, chapter, entry.parent, entry.directories, entry_options, entry.imports,
+ (name, chapter, entry.parent, entry.directories, entry.options, entry.imports,
entry.theories_no_position, conditions, entry.document_theories_no_position,
entry.document_files, session_prefs)
.toString)
@@ -824,8 +823,8 @@
}
}
- val options0 = Options.init0()
- val session_prefs = options.make_prefs(defaults = options0, filter = _.session_content)
+ val session_prefs =
+ options.make_prefs(defaults = Options.init0(), filter = _.session_content)
val root_infos = {
var chapter = UNSORTED
@@ -835,7 +834,7 @@
case entry: Chapter_Entry => chapter = entry.name
case entry: Session_Entry =>
root_infos +=
- Info.make(chapter_defs, options0, options, augment_options,
+ Info.make(chapter_defs, options, augment_options,
root.select, root.dir, chapter, entry)
case _ =>
}
@@ -1168,7 +1167,7 @@
private val session_entry: Parser[Session_Entry] = {
val option =
option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
- { case x ~ y => (x, y) }
+ { case x ~ y => Options.Spec(x, y) }
val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
val theory_entry =
@@ -1471,7 +1470,7 @@
cat_lines(input_dirs.map(dir => " " + File.standard_path(dir))))
- /* database */
+ /* databases for build process and session content */
def find_database(name: String): Option[Path] =
input_dirs.map(_ + database(name)).find(_.is_file)
@@ -1486,13 +1485,25 @@
host = options.string("build_database_host"),
port = options.int("build_database_port"),
ssh =
- options.proper_string("build_database_ssh_host").map(ssh_host =>
+ proper_string(options.string("build_database_ssh_host")).map(ssh_host =>
SSH.open_session(options,
host = ssh_host,
user = options.string("build_database_ssh_user"),
port = options.int("build_database_ssh_port"))),
ssh_close = true)
+ val build_database: Path = Path.explode("$ISABELLE_HOME_USER/build.db")
+
+ def open_build_database(): Option[SQL.Database] =
+ if (!options.bool("build_database_test")) None
+ else if (database_server) Some(open_database_server())
+ else {
+ val db = SQLite.open_database(build_database)
+ try { Isabelle_System.chmod("600", build_database) }
+ catch { case exn: Throwable => db.close(); throw exn }
+ Some(db)
+ }
+
def try_open_database(
name: String,
output: Boolean = false,
--- a/src/Pure/Tools/build.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/Tools/build.scala Tue Mar 14 10:35:10 2023 +0100
@@ -248,8 +248,6 @@
val isabelle_tool1 = Isabelle_Tool("build", "build and manage Isabelle sessions",
Scala_Project.here,
{ args =>
- val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
-
var base_sessions: List[String] = Nil
var select_dirs: List[Path] = Nil
var numa_shuffling = false
@@ -268,7 +266,7 @@
var check_keywords: Set[String] = Set.empty
var list_files = false
var no_build = false
- var options = Options.init(opts = build_options)
+ var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
var verbose = false
var exclude_sessions: List[String] = Nil
@@ -406,12 +404,10 @@
val isabelle_tool2 = Isabelle_Tool("build_worker", "external worker for session build process",
Scala_Project.here,
{ args =>
- val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
-
var numa_shuffling = false
var dirs: List[Path] = Nil
var max_jobs = 1
- var options = Options.init(opts = build_options)
+ var options = Options.init(specs = Options.Spec.ISABELLE_BUILD_OPTIONS)
var verbose = false
var build_uuid = ""
--- a/src/Pure/Tools/build_job.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Tue Mar 14 10:35:10 2023 +0100
@@ -12,12 +12,10 @@
trait Build_Job {
def job_name: String
- def worker_uuid: String
def node_info: Host.Node_Info
def cancel(): Unit = ()
def is_finished: Boolean = false
def join: (Process_Result, SHA1.Shasum) = (Process_Result.undefined, SHA1.no_shasum)
- def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, worker_uuid, node_info)
}
object Build_Job {
@@ -25,14 +23,6 @@
def ok: Boolean = process_result.ok
}
- sealed case class Abstract(
- override val job_name: String,
- override val worker_uuid: String,
- override val node_info: Host.Node_Info
- ) extends Build_Job {
- override def make_abstract: Abstract = this
- }
-
/* build session */
@@ -40,15 +30,13 @@
def start_session(
build_context: Build_Process.Context,
- worker_uuid: String,
progress: Progress,
log: Logger,
session_background: Sessions.Background,
input_shasum: SHA1.Shasum,
node_info: Host.Node_Info
): Session_Job = {
- new Session_Job(
- build_context, worker_uuid, progress, log, session_background, input_shasum, node_info)
+ new Session_Job(build_context, progress, log, session_background, input_shasum, node_info)
}
object Session_Context {
@@ -114,7 +102,6 @@
class Session_Job private[Build_Job](
build_context: Build_Process.Context,
- override val worker_uuid: String,
progress: Progress,
log: Logger,
session_background: Sessions.Background,
--- a/src/Pure/Tools/build_process.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Tue Mar 14 10:35:10 2023 +0100
@@ -120,18 +120,8 @@
case None => Nil
}
- def open_database(): Option[SQL.Database] =
- if (!build_options.bool("build_database_test")) None
- else if (store.database_server) Some(store.open_database_server())
- else {
- val db = SQLite.open_database(Build_Process.Data.database)
- try { Isabelle_System.chmod("600", Build_Process.Data.database) }
- catch { case exn: Throwable => db.close(); throw exn }
- Some(db)
- }
-
def prepare_database(): Unit = {
- using_option(open_database()) { db =>
+ using_option(store.open_build_database()) { db =>
db.transaction {
Data.all_tables.create_lock(db)
Data.clean_build(db)
@@ -153,12 +143,6 @@
type Progress_Messages = SortedMap[Long, Progress.Message]
- case class Task(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) {
- def is_ready: Boolean = deps.isEmpty
- def resolve(dep: String): Task =
- if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this
- }
-
case class Worker(
worker_uuid: String,
build_uuid: String,
@@ -168,7 +152,28 @@
start: Date,
stamp: Date,
stop: Option[Date],
- serial: Long)
+ serial: Long
+ )
+
+ case class Task(
+ name: String,
+ deps: List[String],
+ info: JSON.Object.T = JSON.Object.empty
+ ) {
+ def is_ready: Boolean = deps.isEmpty
+ def resolve(dep: String): Task =
+ if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this
+ }
+
+ case class Job(
+ name: String,
+ worker_uuid: String,
+ build_uuid: String,
+ node_info: Host.Node_Info,
+ build: Option[Build_Job]
+ ) {
+ def no_build: Job = copy(build = None)
+ }
case class Result(
process_result: Process_Result,
@@ -183,7 +188,7 @@
type Sessions = Map[String, Build_Job.Session_Context]
type Workers = List[Worker]
type Pending = List[Task]
- type Running = Map[String, Build_Job]
+ type Running = Map[String, Job]
type Results = Map[String, Result]
def inc_serial(serial: Long): Long = {
@@ -215,7 +220,7 @@
def set_workers(new_workers: State.Workers): State = copy(workers = new_workers)
- def numa_next_node(numa_nodes: List[Int]): (Option[Int], State) =
+ def next_numa_node(numa_nodes: List[Int]): (Option[Int], State) =
if (numa_nodes.isEmpty) (None, this)
else {
val available = numa_nodes.zipWithIndex
@@ -239,13 +244,16 @@
def is_running(name: String): Boolean = running.isDefinedAt(name)
- def stop_running(): Unit = running.valuesIterator.foreach(_.cancel())
+ def stop_running(): Unit =
+ for (job <- running.valuesIterator; build <- job.build) build.cancel()
def finished_running(): List[Build_Job] =
- List.from(running.valuesIterator.filter(_.is_finished))
+ List.from(
+ for (job <- running.valuesIterator; build <- job.build if build.is_finished)
+ yield build)
- def add_running(name: String, job: Build_Job): State =
- copy(running = running + (name -> job))
+ def add_running(job: Job): State =
+ copy(running = running + (job.name -> job))
def remove_running(name: String): State =
copy(running = running - name)
@@ -267,8 +275,6 @@
/** SQL data model **/
object Data {
- val database = Path.explode("$ISABELLE_HOME_USER/build.db")
-
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body)
@@ -299,15 +305,18 @@
val options = SQL.Column.string("options")
val start = SQL.Column.date("start")
val stop = SQL.Column.date("stop")
+ val progress_stopped = SQL.Column.bool("progress_stopped")
- val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
+ val table =
+ make_table("", List(build_uuid, ml_platform, options, start, stop, progress_stopped))
}
def start_build(
db: SQL.Database,
build_uuid: String,
ml_platform: String,
- options: String
+ options: String,
+ progress_stopped: Boolean
): Unit = {
db.execute_statement(Base.table.insert(), body =
{ stmt =>
@@ -316,12 +325,13 @@
stmt.string(3) = options
stmt.date(4) = db.now()
stmt.date(5) = None
+ stmt.bool(6) = progress_stopped
})
}
def stop_build(db: SQL.Database, build_uuid: String): Unit =
db.execute_statement(
- Base.table.update(List(Base.stop), sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+ Base.table.update(List(Base.stop), sql = Base.build_uuid.where_equal(build_uuid)),
body = { stmt => stmt.date(1) = db.now() })
def clean_build(db: SQL.Database): Unit = {
@@ -449,6 +459,37 @@
})
}
+ def sync_progress(
+ db: SQL.Database,
+ seen: Long,
+ build_uuid: String,
+ build_progress: Progress
+ ): (Progress_Messages, Boolean) = {
+ require(build_uuid.nonEmpty)
+
+ val messages = read_progress(db, seen = seen, build_uuid = build_uuid)
+
+ val stopped_db =
+ db.execute_query_statementO[Boolean](
+ Base.table.select(List(Base.progress_stopped),
+ sql = SQL.where(Base.build_uuid.equal(build_uuid))),
+ res => res.bool(Base.progress_stopped)
+ ).getOrElse(false)
+
+ def stop_db(): Unit =
+ db.execute_statement(
+ Base.table.update(
+ List(Base.progress_stopped), sql = Base.build_uuid.where_equal(build_uuid)),
+ body = { stmt => stmt.bool(1) = true })
+
+ val stopped = build_progress.stopped
+
+ if (stopped_db && !stopped) build_progress.stop()
+ if (stopped && !stopped_db) stop_db()
+
+ (messages, messages.isEmpty && stopped_db == stopped)
+ }
+
/* workers */
@@ -511,8 +552,7 @@
val build_stop =
db.execute_query_statementO(
- Base.table.select(List(Base.stop),
- sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+ Base.table.select(List(Base.stop), sql = Base.build_uuid.where_equal(build_uuid)),
res => res.get_date(Base.stop))
build_stop match {
@@ -546,7 +586,7 @@
): Unit = {
val sql =
Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial),
- sql = SQL.where(Generic.sql(worker_uuid = worker_uuid)))
+ sql = Workers.worker_uuid.where_equal(worker_uuid))
db.execute_statement(sql, body =
{ stmt =>
val now = db.now()
@@ -605,43 +645,46 @@
object Running {
val name = Generic.name.make_primary_key
val worker_uuid = Generic.worker_uuid
+ val build_uuid = Generic.build_uuid
val hostname = SQL.Column.string("hostname")
val numa_node = SQL.Column.int("numa_node")
- val table = make_table("running", List(name, worker_uuid, hostname, numa_node))
+ val table = make_table("running", List(name, worker_uuid, build_uuid, hostname, numa_node))
}
- def read_running(db: SQL.Database): List[Build_Job.Abstract] =
+ def read_running(db: SQL.Database): List[Job] =
db.execute_query_statement(
Running.table.select(sql = SQL.order_by(List(Running.name))),
- List.from[Build_Job.Abstract],
+ List.from[Job],
{ res =>
val name = res.string(Running.name)
val worker_uuid = res.string(Running.worker_uuid)
+ val build_uuid = res.string(Running.build_uuid)
val hostname = res.string(Running.hostname)
val numa_node = res.get_int(Running.numa_node)
- Build_Job.Abstract(name, worker_uuid, Host.Node_Info(hostname, numa_node))
+ Job(name, worker_uuid, build_uuid, Host.Node_Info(hostname, numa_node), None)
}
)
def update_running(db: SQL.Database, running: State.Running): Boolean = {
- val old_running = read_running(db)
- val abs_running = running.valuesIterator.map(_.make_abstract).toList
+ val running0 = read_running(db)
+ val running1 = running.valuesIterator.map(_.no_build).toList
- val (delete, insert) = Library.symmetric_difference(old_running, abs_running)
+ val (delete, insert) = Library.symmetric_difference(running0, running1)
if (delete.nonEmpty) {
db.execute_statement(
- Running.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.job_name)))))
+ Running.table.delete(sql = SQL.where(Generic.sql(names = delete.map(_.name)))))
}
for (job <- insert) {
db.execute_statement(Running.table.insert(), body =
{ stmt =>
- stmt.string(1) = job.job_name
+ stmt.string(1) = job.name
stmt.string(2) = job.worker_uuid
- stmt.string(3) = job.node_info.hostname
- stmt.int(4) = job.node_info.numa_node
+ stmt.string(3) = job.build_uuid
+ stmt.string(4) = job.node_info.hostname
+ stmt.int(5) = job.node_info.numa_node
})
}
@@ -777,12 +820,16 @@
protected final val build_uuid: String = build_context.build_uuid
protected final val worker_uuid: String = UUID.random().toString
+ override def toString: String =
+ "Build_Process(worker_uuid = " + quote(worker_uuid) + ", build_uuid = " + quote(build_uuid) +
+ if_proper(build_context.master, ", master = true") + ")"
+
/* global state: internal var vs. external database */
private var _state: Build_Process.State = init_state(Build_Process.State())
- private val _database: Option[SQL.Database] = build_context.open_database()
+ private val _database: Option[SQL.Database] = store.open_build_database()
def close(): Unit = synchronized { _database.foreach(_.close()) }
@@ -790,7 +837,26 @@
synchronized {
_database match {
case None => body
- case Some(db) => db.transaction_lock(Build_Process.Data.all_tables)(body)
+ case Some(db) =>
+ @tailrec def loop(): A = {
+ val sync_progress =
+ db.transaction_lock(Build_Process.Data.all_tables) {
+ val (messages, sync) =
+ Build_Process.Data.sync_progress(
+ db, _state.progress_seen, build_uuid, build_progress)
+ if (sync) Left(body) else Right(messages)
+ }
+ sync_progress match {
+ case Left(res) => res
+ case Right(messages) =>
+ for ((message_serial, message) <- messages) {
+ _state = _state.progress_serial(message_serial = message_serial)
+ if (build_progress.do_output(message)) build_progress.output(message)
+ }
+ loop()
+ }
+ }
+ loop()
}
}
@@ -808,13 +874,12 @@
private def progress_output(message: Progress.Message, build_progress_output: => Unit): Unit = {
synchronized_database {
- val state1 = _state.inc_serial.progress_serial()
+ _state = _state.inc_serial.progress_serial()
for (db <- _database) {
- Build_Process.Data.write_progress(db, state1.serial, message, build_uuid)
- Build_Process.Data.stamp_worker(db, worker_uuid, state1.serial)
+ Build_Process.Data.write_progress(db, _state.serial, message, build_uuid)
+ Build_Process.Data.stamp_worker(db, worker_uuid, _state.serial)
}
build_progress_output
- _state = state1
}
}
@@ -905,7 +970,7 @@
.make_result(session_name, Process_Result.undefined, output_shasum)
}
else {
- val (numa_node, state1) = state.numa_next_node(build_context.numa_nodes)
+ val (numa_node, state1) = state.next_numa_node(build_context.numa_nodes)
val node_info = Host.Node_Info(build_context.hostname, numa_node)
progress.echo(
@@ -914,10 +979,13 @@
store.init_output(session_name)
- val job =
- Build_Job.start_session(build_context, worker_uuid, progress, log,
+ val build =
+ Build_Job.start_session(build_context, progress, log,
build_deps.background(session_name), input_shasum, node_info)
- state1.add_running(session_name, job)
+
+ val job = Build_Process.Job(session_name, worker_uuid, build_uuid, node_info, Some(build))
+
+ state1.add_running(job)
}
}
@@ -927,7 +995,7 @@
final def start_build(): Unit = synchronized_database {
for (db <- _database) {
Build_Process.Data.start_build(db, build_uuid, build_context.ml_platform,
- build_context.sessions_structure.session_prefs)
+ build_context.sessions_structure.session_prefs, progress.stopped)
}
}
@@ -992,16 +1060,16 @@
try {
while (!finished()) {
- if (progress.stopped) synchronized_database { _state.stop_running() }
+ synchronized_database {
+ if (progress.stopped) _state.stop_running()
- for (job <- synchronized_database { _state.finished_running() }) {
- val job_name = job.job_name
- val (process_result, output_shasum) = job.join
- synchronized_database {
+ for (build <- _state.finished_running()) {
+ val job_name = build.job_name
+ val (process_result, output_shasum) = build.join
_state = _state.
remove_pending(job_name).
remove_running(job_name).
- make_result(job_name, process_result, output_shasum, node_info = job.node_info)
+ make_result(job_name, process_result, output_shasum, node_info = build.node_info)
}
}
--- a/src/Pure/Tools/server_commands.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/Tools/server_commands.scala Tue Mar 14 10:35:10 2023 +0100
@@ -61,7 +61,8 @@
args: Args,
progress: Progress = new Progress
) : (JSON.Object.T, Build.Results, Options, Sessions.Background) = {
- val options = Options.init(prefs = args.preferences, opts = args.options)
+ val options =
+ Options.init(prefs = args.preferences, specs = args.options.map(Options.Spec.make))
val dirs = args.dirs.map(Path.explode)
val session_background =
--- a/src/Pure/Tools/update.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Pure/Tools/update.scala Tue Mar 14 10:35:10 2023 +0100
@@ -194,7 +194,7 @@
"l:" -> (arg => base_logics = space_explode(',', arg)),
"n" -> (_ => no_build = true),
"o:" -> (arg => options = options + arg),
- "u:" -> (arg => update_options = update_options ::: List(("update_" + arg, None))),
+ "u:" -> (arg => update_options = update_options ::: List(Options.Spec("update_" + arg))),
"v" -> (_ => verbose = true),
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
--- a/src/Tools/jEdit/src/jedit_options.scala Tue Mar 14 10:34:48 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala Tue Mar 14 10:35:10 2023 +0100
@@ -186,7 +186,7 @@
}
text_area.peer.setInputVerifier({
case text: JTextComponent =>
- try { value + (opt_name, text.getText); true }
+ try { value + Options.Spec(opt_name, Some(text.getText)); true }
catch { case ERROR(_) => false }
case _ => true
})