--- a/src/Pure/Tools/build_job.scala Sat Mar 04 16:15:50 2023 +0100
+++ b/src/Pure/Tools/build_job.scala Sat Mar 04 16:45:21 2023 +0100
@@ -39,10 +39,14 @@
def start_session(
build_context: Build_Process.Context,
+ progress: Progress,
+ log: Logger,
session_background: Sessions.Background,
input_shasum: SHA1.Shasum,
node_info: Host.Node_Info
- ): Session_Job = new Session_Job(build_context, session_background, input_shasum, node_info)
+ ): Session_Job = {
+ new Session_Job(build_context, progress, log, session_background, input_shasum, node_info)
+ }
object Session_Context {
def load(
@@ -103,12 +107,13 @@
class Session_Job private[Build_Job](
build_context: Build_Process.Context,
+ progress: Progress,
+ log: Logger,
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
@@ -168,7 +173,7 @@
/* session */
val resources =
- new Resources(session_background, log = build_context.log,
+ new Resources(session_background, log = log,
command_timings = build_context.old_command_timings(session_name))
val session =
--- a/src/Pure/Tools/build_process.scala Sat Mar 04 16:15:50 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Sat Mar 04 16:45:21 2023 +0100
@@ -8,6 +8,7 @@
package isabelle
+import scala.collection.immutable.SortedMap
import scala.math.Ordering
import scala.annotation.tailrec
@@ -80,7 +81,7 @@
}
val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
- new Context(store, build_deps, sessions, ordering, progress, hostname, numa_nodes,
+ new Context(store, build_deps, sessions, ordering, hostname, numa_nodes,
build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
no_build = no_build, verbose = verbose, session_setup, uuid = uuid)
}
@@ -92,7 +93,6 @@
val build_deps: Sessions.Deps,
val sessions: State.Sessions,
val ordering: Ordering[String],
- val progress: Progress,
val hostname: String,
val numa_nodes: List[Int],
val build_heap: Boolean,
@@ -105,13 +105,6 @@
) {
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 sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum
@@ -132,6 +125,8 @@
/** dynamic state **/
+ type Progress_Messages = SortedMap[Long, Progress.Message]
+
case class Entry(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) {
def is_ready: Boolean = deps.isEmpty
def resolve(dep: String): Entry =
@@ -157,12 +152,22 @@
// dynamic state of various instances, distinguished by uuid
sealed case class State(
serial: Long = 0,
+ progress_seen: Long = 0,
numa_index: Int = 0,
sessions: State.Sessions = Map.empty, // static build targets
pending: State.Pending = Nil, // dynamic build "queue"
running: State.Running = Map.empty, // presently running jobs
results: State.Results = Map.empty // finished results
) {
+ def echo(progress: Progress, message_serial: Long, message: Progress.Message): State =
+ if (message_serial > progress_seen) {
+ progress.echo(message)
+ copy(progress_seen = message_serial)
+ }
+ else {
+ error("Bad serial " + message_serial + " (already seen) for progress message:\n" + message)
+ }
+
def numa_next(numa_nodes: List[Int]): (Option[Int], State) =
if (numa_nodes.isEmpty) (None, this)
else {
@@ -246,6 +251,15 @@
val table = make_table("serial", List(serial))
}
+ object Progress {
+ val serial = SQL.Column.long("serial").make_primary_key
+ val kind = SQL.Column.int("kind")
+ val text = SQL.Column.string("text")
+ val uuid = Generic.uuid
+
+ val table = make_table("progress", List(serial, kind, text, uuid))
+ }
+
object Sessions {
val name = Generic.name.make_primary_key
val deps = SQL.Column.string("deps")
@@ -305,6 +319,38 @@
}
}
+ def read_progress(db: SQL.Database, seen: Long = 0, uuid: String = ""): Progress_Messages =
+ db.using_statement(
+ Progress.table.select(
+ sql =
+ SQL.where(
+ SQL.and(
+ if (seen <= 0) "" else Progress.serial.ident + " > " + seen,
+ Generic.sql_equal(uuid = uuid))))
+ ) { stmt =>
+ SortedMap.from(stmt.execute_query().iterator { res =>
+ val serial = res.long(Progress.serial)
+ val kind = isabelle.Progress.Kind(res.int(Progress.kind))
+ val text = res.string(Progress.text)
+ serial -> isabelle.Progress.Message(kind, text)
+ })
+ }
+
+ def write_progress(
+ db: SQL.Database,
+ message_serial: Long,
+ message: isabelle.Progress.Message,
+ uuid: String
+ ): Unit = {
+ db.using_statement(Progress.table.insert()) { stmt =>
+ stmt.long(1) = message_serial
+ stmt.int(2) = message.kind.id
+ stmt.string(3) = message.text
+ stmt.string(4) = uuid
+ stmt.execute()
+ }
+ }
+
def read_sessions_domain(db: SQL.Database): Set[String] =
db.using_statement(Sessions.table.select(List(Sessions.name)))(stmt =>
Set.from(stmt.execute_query().iterator(_.string(Sessions.name))))
@@ -475,6 +521,7 @@
List(
Base.table,
Serial.table,
+ Progress.table,
Sessions.table,
Pending.table,
Running.table,
@@ -526,14 +573,16 @@
/** main process **/
-class Build_Process(protected val build_context: Build_Process.Context)
+class Build_Process(
+ protected val build_context: Build_Process.Context,
+ protected val build_progress: Progress
+)
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.build_deps
- protected val progress: Progress = build_context.progress
protected val verbose: Boolean = build_context.verbose
@@ -579,6 +628,33 @@
}
+ /* progress backed by database */
+
+ object progress extends Progress {
+ override def echo(message: Progress.Message): Unit =
+ synchronized_database {
+ val serial1 = _state.serial + 1
+ _state = _state.echo(build_progress, serial1, message).copy(serial = serial1)
+
+ for (db <- _database) {
+ Build_Process.Data.write_progress(db, serial1, message, build_context.uuid)
+ Build_Process.Data.set_serial(db, serial1)
+ }
+ }
+
+ override def verbose: Boolean = build_progress.verbose
+ override def stop(): Unit = build_progress.stop()
+ override def stopped: Boolean = build_progress.stopped
+ }
+
+ 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)))
+ }
+
+
/* policy operations */
protected def init_state(state: Build_Process.State): Build_Process.State = {
@@ -654,8 +730,8 @@
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)
+ Build_Job.start_session(build_context, progress, log,
+ build_deps.background(session_name), input_shasum, node_info)
state1.add_running(session_name, job)
}
}