--- a/src/Pure/Tools/build.scala Tue Jun 27 11:39:02 2023 +0200
+++ b/src/Pure/Tools/build.scala Tue Jun 27 14:50:48 2023 +0200
@@ -163,13 +163,11 @@
/* build process and results */
val build_context =
- Build_Process.Context(store, build_deps, progress = progress,
+ Build_Process.init_context(store, build_deps, progress = progress,
hostname = hostname(build_options), build_heap = build_heap,
numa_shuffling = numa_shuffling, max_jobs = max_jobs, fresh_build = fresh_build,
no_build = no_build, session_setup = session_setup, master = true)
- build_context.store_init()
-
if (clean_build) {
using_optional(store.maybe_open_database_server()) { database_server =>
for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
--- a/src/Pure/Tools/build_process.scala Tue Jun 27 11:39:02 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Tue Jun 27 14:50:48 2023 +0200
@@ -16,79 +16,89 @@
object Build_Process {
/** static context **/
- object Context {
- def apply(
- store: Store,
- build_deps: Sessions.Deps,
- progress: Progress = new Progress,
- ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
- hostname: String = Isabelle_System.hostname(),
- numa_shuffling: Boolean = false,
- build_heap: Boolean = false,
- max_jobs: Int = 1,
- fresh_build: Boolean = false,
- no_build: Boolean = false,
- session_setup: (String, Session) => Unit = (_, _) => (),
- build_uuid: String = UUID.random().toString,
- master: Boolean = false,
- ): Context = {
- val sessions_structure = build_deps.sessions_structure
- val build_graph = sessions_structure.build_graph
+ def init_context(
+ store: Store,
+ build_deps: Sessions.Deps,
+ progress: Progress = new Progress,
+ ml_platform: String = Isabelle_System.getenv("ML_PLATFORM"),
+ hostname: String = Isabelle_System.hostname(),
+ numa_shuffling: Boolean = false,
+ build_heap: Boolean = false,
+ max_jobs: Int = 1,
+ fresh_build: Boolean = false,
+ no_build: Boolean = false,
+ session_setup: (String, Session) => Unit = (_, _) => (),
+ build_uuid: String = UUID.random().toString,
+ master: Boolean = false,
+ ): Context = {
+ val sessions_structure = build_deps.sessions_structure
+ val build_graph = sessions_structure.build_graph
- val sessions =
- Map.from(
- for ((name, (info, _)) <- build_graph.iterator)
- yield {
- 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(
- build_uuid, name, deps, ancestors, info.session_prefs, sources_shasum,
- info.timeout, store, progress = progress)
- name -> session_context
- })
+ val sessions =
+ Map.from(
+ for ((name, (info, _)) <- build_graph.iterator)
+ yield {
+ 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(
+ build_uuid, name, deps, ancestors, info.session_prefs, sources_shasum,
+ info.timeout, store, progress = progress)
+ name -> session_context
+ })
- val sessions_time = {
- val maximals = build_graph.maximals.toSet
- def descendants_time(name: String): Double = {
- if (maximals.contains(name)) sessions(name).old_time.seconds
- else {
- val descendants = build_graph.all_succs(List(name)).toSet
- val g = build_graph.restrict(descendants)
- (0.0 :: g.maximals.flatMap { desc =>
- val ps = g.all_preds(List(desc))
- if (ps.exists(p => !sessions.isDefinedAt(p))) None
- else Some(ps.map(p => sessions(p).old_time.seconds).sum)
- }).max
+ val sessions_time = {
+ val maximals = build_graph.maximals.toSet
+ def descendants_time(name: String): Double = {
+ if (maximals.contains(name)) sessions(name).old_time.seconds
+ else {
+ val descendants = build_graph.all_succs(List(name)).toSet
+ val g = build_graph.restrict(descendants)
+ (0.0 :: g.maximals.flatMap { desc =>
+ val ps = g.all_preds(List(desc))
+ if (ps.exists(p => !sessions.isDefinedAt(p))) None
+ else Some(ps.map(p => sessions(p).old_time.seconds).sum)
+ }).max
+ }
+ }
+ Map.from(
+ for (name <- sessions.keysIterator)
+ yield name -> descendants_time(name)).withDefaultValue(0.0)
+ }
+
+ val ordering =
+ new Ordering[String] {
+ def compare(name1: String, name2: String): Int =
+ sessions_time(name2) compare sessions_time(name1) match {
+ case 0 =>
+ sessions(name2).timeout compare sessions(name1).timeout match {
+ case 0 => name1 compare name2
+ case ord => ord
+ }
+ case ord => ord
}
- }
- Map.from(
- for (name <- sessions.keysIterator)
- yield name -> descendants_time(name)).withDefaultValue(0.0)
}
- val ordering =
- new Ordering[String] {
- def compare(name1: String, name2: String): Int =
- sessions_time(name2) compare sessions_time(name1) match {
- case 0 =>
- sessions(name2).timeout compare sessions(name1).timeout match {
- case 0 => name1 compare name2
- case ord => ord
- }
- case ord => ord
- }
- }
+ Isabelle_System.make_directory(store.output_dir + Path.basic("log"))
- val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
- new Context(store, build_deps, sessions, ordering, ml_platform, hostname, numa_nodes,
- build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
- no_build = no_build, session_setup, build_uuid = build_uuid, master = master)
+ using_option(store.maybe_open_build_database(Data.database)) { db =>
+ val shared_db = db.is_postgresql
+ Data.transaction_lock(db, create = true) {
+ Data.clean_build(db)
+ if (shared_db) Store.Data.tables.lock(db, create = true)
+ }
+ Data.vacuum(db, more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty)
}
+
+ val numa_nodes = Host.numa_nodes(enabled = numa_shuffling)
+
+ new Context(store, build_deps, sessions, ordering, ml_platform, hostname, numa_nodes,
+ build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build,
+ no_build = no_build, session_setup, build_uuid = build_uuid, master = master)
}
- final class Context private(
+ final class Context private[Build_Process](
val store: Store,
val build_deps: Sessions.Deps,
val sessions: State.Sessions,
@@ -121,19 +131,6 @@
case None => Nil
}
- def store_init(): Unit = {
- Isabelle_System.make_directory(store.output_dir + Path.basic("log"))
-
- using_option(store.maybe_open_build_database(Data.database)) { db =>
- val shared_db = db.is_postgresql
- Data.transaction_lock(db, create = true) {
- Data.clean_build(db)
- if (shared_db) Store.Data.tables.lock(db, create = true)
- }
- Data.vacuum(db, more_tables = if (shared_db) Store.Data.tables else SQL.Tables.empty)
- }
- }
-
def store_heap(name: String): Boolean =
build_heap || Sessions.is_pure(name) ||
sessions.valuesIterator.exists(_.ancestors.contains(name))