--- a/src/Pure/Thy/store.scala Mon Jul 17 11:20:28 2023 +0200
+++ b/src/Pure/Thy/store.scala Mon Jul 17 11:39:32 2023 +0200
@@ -387,7 +387,7 @@
}
def check_output(
- server: SSH.Server,
+ database_server: Option[SQL.Database],
name: String,
session_options: Options,
sources_shasum: SHA1.Shasum,
@@ -395,24 +395,26 @@
fresh_build: Boolean,
store_heap: Boolean
): (Boolean, SHA1.Shasum) = {
- try_open_database(name, server = server) match {
- case Some(db) =>
- using(db) { _ =>
- read_build(db, name) match {
- case Some(build) =>
- val output_shasum = heap_shasum(if (db.is_postgresql) Some(db) else None, name)
- val current =
- !fresh_build &&
- build.ok &&
- Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
- build.input_heaps == input_shasum &&
- build.output_heap == output_shasum &&
- !(store_heap && output_shasum.is_empty)
- (current, output_shasum)
- case None => (false, SHA1.no_shasum)
- }
- }
- case None => (false, SHA1.no_shasum)
+ def no_check: (Boolean, SHA1.Shasum) = (false, SHA1.no_shasum)
+
+ def check(db: SQL.Database): (Boolean, SHA1.Shasum) =
+ read_build(db, name) match {
+ case Some(build) =>
+ val output_shasum = heap_shasum(if (db.is_postgresql) Some(db) else None, name)
+ val current =
+ !fresh_build &&
+ build.ok &&
+ Sessions.eq_sources(session_options, build.sources, sources_shasum) &&
+ build.input_heaps == input_shasum &&
+ build.output_heap == output_shasum &&
+ !(store_heap && output_shasum.is_empty)
+ (current, output_shasum)
+ case None => no_check
+ }
+
+ database_server match {
+ case Some(db) => if (session_info_exists(db)) check(db) else no_check
+ case None => using_option(try_open_database(name))(check) getOrElse no_check
}
}
--- a/src/Pure/Tools/build_job.scala Mon Jul 17 11:20:28 2023 +0200
+++ b/src/Pure/Tools/build_job.scala Mon Jul 17 11:39:32 2023 +0200
@@ -37,6 +37,7 @@
object Session_Context {
def load(
+ database_server: Option[SQL.Database],
build_uuid: String,
name: String,
deps: List[String],
@@ -45,40 +46,41 @@
sources_shasum: SHA1.Shasum,
timeout: Time,
store: Store,
- progress: Progress = new Progress,
- server: SSH.Server = SSH.no_server
+ progress: Progress = new Progress
): Session_Context = {
def default: Session_Context =
Session_Context(
name, deps, ancestors, session_prefs, sources_shasum, timeout,
Time.zero, Bytes.empty, build_uuid)
- store.try_open_database(name, server = server) match {
- case None => default
- case Some(db) =>
- def ignore_error(msg: String) = {
- progress.echo_warning(
- "Ignoring bad database " + db + " for session " + quote(name) +
- if_proper(msg, ":\n" + msg))
- default
- }
- try {
- val command_timings = store.read_command_timings(db, name)
- val elapsed =
- store.read_session_timing(db, name) match {
- case Markup.Elapsed(s) => Time.seconds(s)
- case _ => Time.zero
- }
- new Session_Context(
- name, deps, ancestors, session_prefs, sources_shasum, timeout,
- elapsed, command_timings, build_uuid)
- }
- catch {
- case ERROR(msg) => ignore_error(msg)
- case exn: java.lang.Error => ignore_error(Exn.message(exn))
- case _: XML.Error => ignore_error("XML.Error")
- }
- finally { db.close() }
+ def read(db: SQL.Database): Session_Context = {
+ def ignore_error(msg: String) = {
+ progress.echo_warning(
+ "Ignoring bad database " + db + " for session " + quote(name) +
+ if_proper(msg, ":\n" + msg))
+ default
+ }
+ try {
+ val command_timings = store.read_command_timings(db, name)
+ val elapsed =
+ store.read_session_timing(db, name) match {
+ case Markup.Elapsed(s) => Time.seconds(s)
+ case _ => Time.zero
+ }
+ new Session_Context(
+ name, deps, ancestors, session_prefs, sources_shasum, timeout,
+ elapsed, command_timings, build_uuid)
+ }
+ catch {
+ case ERROR(msg) => ignore_error(msg)
+ case exn: java.lang.Error => ignore_error(Exn.message(exn))
+ case _: XML.Error => ignore_error("XML.Error")
+ }
+ }
+
+ database_server match {
+ case Some(db) => if (store.session_info_exists(db)) read(db) else default
+ case None => using_option(store.try_open_database(name))(read) getOrElse default
}
}
}
@@ -489,7 +491,7 @@
else File.write(store.output_log(session_name), terminate_lines(log_lines))
// write database
- using(store.open_database(session_name, output = true, server = server))(db =>
+ def write_info(db: SQL.Database): Unit =
store.write_session_info(db, session_name, session_sources,
build_log =
if (process_result.timeout) build_log.error("Timeout") else build_log,
@@ -499,7 +501,11 @@
input_heaps = input_shasum,
output_heap = output_shasum,
process_result.rc,
- build_context.build_uuid)))
+ build_context.build_uuid))
+ database_server match {
+ case Some(db) => write_info(db)
+ case None => using(store.open_database(session_name, output = true))(write_info)
+ }
// messages
process_result.err_lines.foreach(progress.echo(_))
--- a/src/Pure/Tools/build_process.scala Mon Jul 17 11:20:28 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Mon Jul 17 11:39:32 2023 +0200
@@ -130,8 +130,8 @@
def init(
build_context: Context,
- progress: Progress = new Progress,
- server: SSH.Server = SSH.no_server
+ database_server: Option[SQL.Database],
+ progress: Progress = new Progress
): Sessions = {
val sessions_structure = build_context.sessions_structure
make(
@@ -169,9 +169,9 @@
}
else {
val session =
- Build_Job.Session_Context.load(
+ Build_Job.Session_Context.load(database_server,
build_context.build_uuid, name, deps, ancestors, prefs, sources_shasum,
- info.timeout, build_context.store, progress = progress, server = server)
+ info.timeout, build_context.store, progress = progress)
graph0.new_node(name, session)
}
}
@@ -933,7 +933,7 @@
/* policy operations */
protected def init_state(state: Build_Process.State): Build_Process.State = {
- val sessions1 = state.sessions.init(build_context, progress = build_progress)
+ val sessions1 = state.sessions.init(build_context, _database_server, progress = build_progress)
val old_pending = state.pending.iterator.map(_.name).toSet
val new_pending =
@@ -971,7 +971,7 @@
state.sessions.iterator.exists(_.ancestors.contains(session_name))
val (current, output_shasum) =
- store.check_output(server, session_name,
+ store.check_output(_database_server, session_name,
session_options = build_context.sessions_structure(session_name).options,
sources_shasum = sources_shasum,
input_shasum = input_shasum,