# HG changeset patch # User wenzelm # Date 1710090074 -3600 # Node ID 15948836fa908bfc011e2f16e99ddfe51b7780c9 # Parent 61c3e1c5fce550fb6516c7660415308394158ce5 more robust init_built: get_build_id and start_build within the same transaction; diff -r 61c3e1c5fce5 -r 15948836fa90 src/Pure/Build/build_process.scala --- a/src/Pure/Build/build_process.scala Sun Mar 10 17:33:44 2024 +0100 +++ b/src/Pure/Build/build_process.scala Sun Mar 10 18:01:14 2024 +0100 @@ -945,9 +945,19 @@ private_data.read_builds(db) } - def get_build_id(db: SQL.Database, build_uuid: String): Long = - private_data.transaction_lock(db, create = true, label = "Build_Process.build_id") { - private_data.get_build_id(db, build_uuid) + def init_build( + db: SQL.Database, + build_context: isabelle.Build.Context, + build_start: Date + ): Long = + private_data.transaction_lock(db, create = true, label = "Build_Process.init_build") { + val build_uuid = build_context.build_uuid + val build_id = private_data.get_build_id(db, build_uuid) + if (build_context.master) { + private_data.start_build(db, build_id, build_uuid, build_context.ml_platform, + build_context.sessions_structure.session_prefs, build_start) + } + build_id } } @@ -1043,16 +1053,16 @@ } } + protected val log: Logger = Logger.make_system_log(progress, build_options) + + protected val build_start: Date = build_context.build_start getOrElse progress.now() + protected val build_id: Long = _build_database match { case None => 0L - case Some(db) => Build_Process.get_build_id(db, build_uuid) + case Some(db) => Build_Process.init_build(db, build_context, build_start) } - protected val build_start: Date = build_context.build_start getOrElse progress.now() - - protected val log: Logger = Logger.make_system_log(progress, build_options) - protected def open_build_cluster(): Build_Cluster = Build_Cluster.make(build_context, progress = build_progress).open() @@ -1211,13 +1221,6 @@ final def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name) - protected final def start_build(): Unit = synchronized_database("Build_Process.start_build") { - for (db <- _build_database) { - Build_Process.private_data.start_build(db, build_id, build_uuid, - build_context.ml_platform, build_context.sessions_structure.session_prefs, build_start) - } - } - protected final def stop_build(): Unit = synchronized_database("Build_Process.stop_build") { for (db <- _build_database) { Build_Process.private_data.stop_build(db, build_uuid) @@ -1311,10 +1314,10 @@ } if (vacuous) { progress.echo_warning("Nothing to build") + if (build_context.master) stop_build() Build.Results(build_context) } else { - if (build_context.master) start_build() start_worker() _build_cluster.start()