# HG changeset patch # User nipkow # Date 1678786510 -3600 # Node ID 4b688b8f1de33076a6c652cf5bb53881594ff66d # Parent 4563db765eb273b2a1b6c548731d053ccf75f50e# Parent a28ee8058ea35f5ce15f9c1d898fb6abff2555ea merged diff -r a28ee8058ea3 -r 4b688b8f1de3 src/HOL/Tools/Mirabelle/mirabelle.scala --- 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") diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/ROOT.ML --- 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"; + diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/System/options.scala --- 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) } diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/Thy/sessions.scala --- 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, diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/Tools/build.scala --- 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 = "" diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/Tools/build_job.scala --- 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, diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/Tools/build_process.scala --- 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) } } diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/Tools/server_commands.scala --- 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 = diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Pure/Tools/update.scala --- 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))) diff -r a28ee8058ea3 -r 4b688b8f1de3 src/Tools/jEdit/src/jedit_options.scala --- 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 })