# HG changeset patch # User wenzelm # Date 1675684725 -3600 # Node ID 6784eaef7d0c1fd297989bc7dcd743b3cbdd9ef4 # Parent a197d583bf9fbad229c8f4b7a17f324ac3ef2b5c prefer explicit shasum; clarified signature; diff -r a197d583bf9f -r 6784eaef7d0c src/Pure/ML/ml_heap.scala --- a/src/Pure/ML/ml_heap.scala Mon Feb 06 11:05:35 2023 +0100 +++ b/src/Pure/ML/ml_heap.scala Mon Feb 06 12:58:45 2023 +0100 @@ -17,7 +17,7 @@ private val sha1_prefix = "SHA1:" - def read_digest(heap: Path): Option[String] = { + def read_digest(heap: Path): Option[SHA1.Digest] = { if (heap.is_file) { using(FileChannel.open(heap.java_path, StandardOpenOption.READ)) { file => val len = file.size @@ -37,7 +37,7 @@ if (i == n) { val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset) val s = new String(buf.array(), sha1_prefix.length, SHA1.digest_length, UTF8.charset) - if (prefix == sha1_prefix) Some(s) else None + if (prefix == sha1_prefix) Some(SHA1.fake_digest(s)) else None } else None } @@ -47,10 +47,10 @@ else None } - def write_digest(heap: Path): String = + def write_digest(heap: Path): SHA1.Digest = read_digest(heap) getOrElse { - val s = SHA1.digest(heap).toString - File.append(heap, sha1_prefix + s) - s + val digest = SHA1.digest(heap) + File.append(heap, sha1_prefix + digest.toString) + digest } } diff -r a197d583bf9f -r 6784eaef7d0c src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Feb 06 11:05:35 2023 +0100 +++ b/src/Pure/Thy/sessions.scala Mon Feb 06 12:58:45 2023 +0100 @@ -1408,8 +1408,11 @@ def find_heap(name: String): Option[Path] = input_dirs.map(_ + heap(name)).find(_.is_file) - def find_heap_digest(name: String): Option[String] = - find_heap(name).flatMap(ML_Heap.read_digest) + def find_heap_shasum(name: String): String = + (for { + path <- find_heap(name) + digest <- ML_Heap.read_digest(path) + } yield SHA1.shasum(digest, name) + "\n").getOrElse("") def the_heap(name: String): Path = find_heap(name) getOrElse @@ -1563,8 +1566,8 @@ stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache.compress) stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache.compress) stmt.string(8) = build.sources - stmt.string(9) = cat_lines(build.input_heaps) - stmt.string(10) = build.output_heap getOrElse "" + stmt.string(9) = build.input_heaps + stmt.string(10) = build.output_heap stmt.int(11) = build.return_code stmt.string(12) = build.uuid stmt.execute() @@ -1606,8 +1609,8 @@ Some( Build.Session_Info( res.string(Session_Info.sources), - split_lines(res.string(Session_Info.input_heaps)), - res.string(Session_Info.output_heap) match { case "" => None case s => Some(s) }, + res.string(Session_Info.input_heaps), + res.string(Session_Info.output_heap), res.int(Session_Info.return_code), uuid)) } diff -r a197d583bf9f -r 6784eaef7d0c src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Feb 06 11:05:35 2023 +0100 +++ b/src/Pure/Tools/build.scala Mon Feb 06 12:58:45 2023 +0100 @@ -19,8 +19,8 @@ sealed case class Session_Info( sources: String, - input_heaps: List[String], - output_heap: Option[String], + input_heaps: String, + output_heap: String, return_code: Int, uuid: String ) { @@ -271,7 +271,7 @@ // scheduler loop case class Result( current: Boolean, - heap_digest: Option[String], + output_heap: String, process: Option[Process_Result], info: Sessions.Info ) { @@ -298,7 +298,7 @@ @tailrec def loop( pending: Queue, - running: Map[String, (List[String], Build_Job)], + running: Map[String, (String, Build_Job)], results: Map[String, Result] ): Map[String, Result] = { def used_node(i: Int): Boolean = @@ -315,7 +315,7 @@ case Some((session_name, (input_heaps, job))) => //{{{ finish job - val (process_result, heap_digest) = job.join + val (process_result, output_heap) = job.join val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) val process_result_tail = { @@ -346,7 +346,7 @@ build_log = if (process_result.timeout) build_log.error("Timeout") else build_log, build = - Session_Info(build_deps.sources_shasum(session_name), input_heaps, heap_digest, + Session_Info(build_deps.sources_shasum(session_name), input_heaps, output_heap, process_result.rc, UUID.random().toString))) // messages @@ -363,7 +363,7 @@ loop(pending - session_name, running - session_name, results + - (session_name -> Result(false, heap_digest, Some(process_result_tail), job.info))) + (session_name -> Result(false, output_heap, Some(process_result_tail), job.info))) //}}} case None if running.size < (max_jobs max 1) => //{{{ check/start next job @@ -372,32 +372,32 @@ val ancestor_results = build_deps.sessions_structure.build_requirements(List(session_name)). filterNot(_ == session_name).map(results(_)) - val ancestor_heaps = + val input_heaps = if (ancestor_results.isEmpty) { - List(SHA1.digest(Path.explode("$POLYML_EXE")).toString) + SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) + "\n" } - else ancestor_results.flatMap(_.heap_digest) + else ancestor_results.map(_.output_heap).mkString val do_store = build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name) - val (current, heap_digest) = { + val (current, output_heap) = { store.try_open_database(session_name) match { case Some(db) => using(db)(store.read_build(_, session_name)) match { case Some(build) => - val heap_digest = store.find_heap_digest(session_name) + val output_heap = store.find_heap_shasum(session_name) val current = !fresh_build && build.ok && build.sources == build_deps.sources_shasum(session_name) && - build.input_heaps == ancestor_heaps && - build.output_heap == heap_digest && - !(do_store && heap_digest.isEmpty) - (current, heap_digest) - case None => (false, None) + build.input_heaps == input_heaps && + build.output_heap == output_heap && + !(do_store && output_heap.isEmpty) + (current, output_heap) + case None => (false, "") } - case None => (false, None) + case None => (false, "") } } val all_current = current && ancestor_results.forall(_.current) @@ -405,13 +405,13 @@ if (all_current) { loop(pending - session_name, running, results + - (session_name -> Result(true, heap_digest, Some(Process_Result(0)), info))) + (session_name -> Result(true, output_heap, Some(Process_Result(0)), info))) } else if (no_build) { progress.echo_if(verbose, "Skipping " + session_name + " ...") loop(pending - session_name, running, results + - (session_name -> Result(false, heap_digest, Some(Process_Result(1)), info))) + (session_name -> Result(false, output_heap, Some(Process_Result(1)), info))) } else if (ancestor_results.forall(_.ok) && !progress.stopped) { progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...") @@ -424,12 +424,12 @@ val job = new Build_Job(progress, build_deps.background(session_name), store, do_store, log, session_setup, numa_node, queue.command_timings(session_name)) - loop(pending, running + (session_name -> (ancestor_heaps, job)), results) + loop(pending, running + (session_name -> (input_heaps, job)), results) } else { progress.echo(session_name + " CANCELLED") loop(pending - session_name, running, - results + (session_name -> Result(false, heap_digest, None, info))) + results + (session_name -> Result(false, output_heap, None, info))) } case None => sleep(); loop(pending, running, results) } diff -r a197d583bf9f -r 6784eaef7d0c src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon Feb 06 11:05:35 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Mon Feb 06 12:58:45 2023 +0100 @@ -570,7 +570,7 @@ else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } - def join: (Process_Result, Option[String]) = { + def join: (Process_Result, String) = { val result1 = future_result.join val was_timeout = @@ -591,6 +591,12 @@ } else None - (result2, heap_digest) + val heap_shasum = + heap_digest match { + case None => "" + case Some(digest) => SHA1.shasum(digest, session_name) + "\n" + } + + (result2, heap_shasum) } }