# HG changeset patch # User wenzelm # Date 1708602787 -3600 # Node ID d298c5b65d8efd239bb68971406b1181b003c746 # Parent ecc851dd274f549c7200b0d7b6974e78122ff841 clarified store_session: heap requires process_result.ok, but log_db is always stored; clarified ML_Heap.clean_entry vs. ML_Heap.init_entry; diff -r ecc851dd274f -r d298c5b65d8e src/Pure/Build/build_job.scala --- a/src/Pure/Build/build_job.scala Thu Feb 22 12:22:13 2024 +0100 +++ b/src/Pure/Build/build_job.scala Thu Feb 22 12:53:07 2024 +0100 @@ -120,7 +120,6 @@ val options = Host.node_options(info.options, node_info) val store = build_context.store - val store_session = store.output_session(session_name, store_heap = store_heap) using_optional(store.maybe_open_database_server(server = server)) { database_server => @@ -465,14 +464,16 @@ else if (result2.interrupted) result2.error(Output.error_message_text("Interrupt")) else result2 + val store_session = + store.output_session(session_name, store_heap = process_result.ok && store_heap) + /* output heap */ val output_shasum = store_session.heap match { - case Some(path) if process_result.ok => - SHA1.shasum(ML_Heap.write_file_digest(path), session_name) - case _ => SHA1.no_shasum + case Some(path) => SHA1.shasum(ML_Heap.write_file_digest(path), session_name) + case None => SHA1.no_shasum } val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) @@ -517,11 +518,8 @@ using_optional(store.maybe_open_heaps_database(database_server, server = server)) { heaps_database => for (db <- database_server orElse heaps_database) { - ML_Heap.clean_entry(db, session_name) - if (process_result.ok) { - val slice = Space.MiB(options.real("build_database_slice")) - ML_Heap.store(db, store_session, slice, progress = progress) - } + val slice = Space.MiB(options.real("build_database_slice")) + ML_Heap.store(db, store_session, slice, progress = progress) } } diff -r ecc851dd274f -r d298c5b65d8e src/Pure/ML/ml_heap.scala --- a/src/Pure/ML/ml_heap.scala Thu Feb 22 12:22:13 2024 +0100 +++ b/src/Pure/ML/ml_heap.scala Thu Feb 22 12:53:07 2024 +0100 @@ -131,12 +131,13 @@ for (table <- List(Base.table, Slices.table)) { db.execute_statement(table.delete(sql = Base.name.where_equal(name))) } + } + + def init_entry(db: SQL.Database, name: String): Unit = { + clean_entry(db, name) for (table <- List(Size.table, Slices_Size.table)) { db.create_view(table) } - } - - def init_entry(db: SQL.Database, name: String): Unit = db.execute_statement(Base.table.insert(), body = { stmt => stmt.string(1) = name @@ -145,6 +146,7 @@ stmt.string(4) = None stmt.bytes(5) = None }) + } def finish_entry( db: SQL.Database,