# HG changeset patch # User wenzelm # Date 1675691655 -3600 # Node ID d98a99e4eea94f91ee715f91e91ca5da1e65e8e7 # Parent 6784eaef7d0c1fd297989bc7dcd743b3cbdd9ef4 proper Shasum.digest, to emulate old form from build_history database; clarified signature: more explicit types; diff -r 6784eaef7d0c -r d98a99e4eea9 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Mon Feb 06 12:58:45 2023 +0100 +++ b/src/Pure/Admin/build_history.scala Mon Feb 06 14:54:15 2023 +0100 @@ -295,8 +295,8 @@ val session_sources = store.read_build(db, session_name).map(_.sources) match { - case Some(sources) if sources.length == SHA1.digest_length => - List("Sources " + session_name + " " + sources) + case Some(sources) if !sources.is_empty => + List("Sources " + session_name + " " + sources.digest.toString) case _ => Nil } diff -r 6784eaef7d0c -r d98a99e4eea9 src/Pure/General/sha1.scala --- a/src/Pure/General/sha1.scala Mon Feb 06 12:58:45 2023 +0100 +++ b/src/Pure/General/sha1.scala Mon Feb 06 14:54:15 2023 +0100 @@ -14,6 +14,8 @@ object SHA1 { + /* digest */ + final class Digest private[SHA1](rep: String) { override def toString: String = rep override def hashCode: Int = rep.hashCode @@ -52,6 +54,33 @@ val digest_length: Int = digest("").toString.length - def shasum(digest: Digest, name: String): String = digest.toString + " " + name - def shasum_meta_info(digest: Digest): String = shasum(digest, isabelle.setup.Build.META_INFO) + + /* shasum */ + + final class Shasum private[SHA1](private[SHA1] val rep: List[String]) { + override def equals(other: Any): Boolean = + other match { + case that: Shasum => rep.equals(that.rep) + case _ => false + } + override def hashCode: Int = rep.hashCode + override def toString: String = Library.terminate_lines(rep) + + def is_empty: Boolean = rep.isEmpty + + def digest: Digest = { + rep match { + case List(s) + if s.length == digest_length && s.forall(Symbol.is_ascii_hex) => fake_digest(s) + case _ => SHA1.digest(toString) + } + } + } + + val no_shasum: Shasum = new Shasum(Nil) + def flat_shasum(list: List[Shasum]): Shasum = new Shasum(list.flatMap(_.rep)) + def fake_shasum(text: String): Shasum = new Shasum(Library.trim_split_lines(text)) + + def shasum(digest: Digest, name: String): Shasum = new Shasum(List(digest.toString + " " + name)) + def shasum_meta_info(digest: Digest): Shasum = shasum(digest, isabelle.setup.Build.META_INFO) } diff -r 6784eaef7d0c -r d98a99e4eea9 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Feb 06 12:58:45 2023 +0100 +++ b/src/Pure/Thy/sessions.scala Mon Feb 06 14:54:15 2023 +0100 @@ -275,13 +275,14 @@ def apply(name: String): Base = session_bases(name) def get(name: String): Option[Base] = session_bases.get(name) - def sources_shasum(name: String): String = { + def sources_shasum(name: String): SHA1.Shasum = { val meta_info = SHA1.shasum_meta_info(sessions_structure(name).meta_digest) val sources = (for ((path, digest) <- apply(name).all_sources) yield (File.symbolic_path(path), digest)) .sortBy(_._1).map(p => SHA1.shasum(p._2, p._1)) - Library.terminate_lines(meta_info :: sources) + + SHA1.flat_shasum(meta_info :: sources) } def errors: List[String] = @@ -1408,11 +1409,11 @@ def find_heap(name: String): Option[Path] = input_dirs.map(_ + heap(name)).find(_.is_file) - def find_heap_shasum(name: String): String = + def find_heap_shasum(name: String): SHA1.Shasum = (for { path <- find_heap(name) digest <- ML_Heap.read_digest(path) - } yield SHA1.shasum(digest, name) + "\n").getOrElse("") + } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum) def the_heap(name: String): Path = find_heap(name) getOrElse @@ -1565,9 +1566,9 @@ stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache.compress) 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) = build.input_heaps - stmt.string(10) = build.output_heap + stmt.string(8) = build.sources.toString + stmt.string(9) = build.input_heaps.toString + stmt.string(10) = build.output_heap.toString stmt.int(11) = build.return_code stmt.string(12) = build.uuid stmt.execute() @@ -1608,9 +1609,9 @@ catch { case _: SQLException => "" } Some( Build.Session_Info( - res.string(Session_Info.sources), - res.string(Session_Info.input_heaps), - res.string(Session_Info.output_heap), + SHA1.fake_shasum(res.string(Session_Info.sources)), + SHA1.fake_shasum(res.string(Session_Info.input_heaps)), + SHA1.fake_shasum(res.string(Session_Info.output_heap)), res.int(Session_Info.return_code), uuid)) } diff -r 6784eaef7d0c -r d98a99e4eea9 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Feb 06 12:58:45 2023 +0100 +++ b/src/Pure/Tools/build.scala Mon Feb 06 14:54:15 2023 +0100 @@ -18,9 +18,9 @@ /* persistent build info */ sealed case class Session_Info( - sources: String, - input_heaps: String, - output_heap: String, + sources: SHA1.Shasum, + input_heaps: SHA1.Shasum, + output_heap: SHA1.Shasum, return_code: Int, uuid: String ) { @@ -271,7 +271,7 @@ // scheduler loop case class Result( current: Boolean, - output_heap: String, + output_heap: SHA1.Shasum, process: Option[Process_Result], info: Sessions.Info ) { @@ -298,7 +298,7 @@ @tailrec def loop( pending: Queue, - running: Map[String, (String, Build_Job)], + running: Map[String, (SHA1.Shasum, Build_Job)], results: Map[String, Result] ): Map[String, Result] = { def used_node(i: Int): Boolean = @@ -374,9 +374,9 @@ filterNot(_ == session_name).map(results(_)) val input_heaps = if (ancestor_results.isEmpty) { - SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) + "\n" + SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) } - else ancestor_results.map(_.output_heap).mkString + else SHA1.flat_shasum(ancestor_results.map(_.output_heap)) val do_store = build_heap || Sessions.is_pure(session_name) || queue.is_inner(session_name) @@ -393,11 +393,11 @@ build.sources == build_deps.sources_shasum(session_name) && build.input_heaps == input_heaps && build.output_heap == output_heap && - !(do_store && output_heap.isEmpty) + !(do_store && output_heap.is_empty) (current, output_heap) - case None => (false, "") + case None => (false, SHA1.no_shasum) } - case None => (false, "") + case None => (false, SHA1.no_shasum) } } val all_current = current && ancestor_results.forall(_.current) diff -r 6784eaef7d0c -r d98a99e4eea9 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon Feb 06 12:58:45 2023 +0100 +++ b/src/Pure/Tools/build_job.scala Mon Feb 06 14:54:15 2023 +0100 @@ -570,7 +570,7 @@ else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } - def join: (Process_Result, String) = { + def join: (Process_Result, SHA1.Shasum) = { val result1 = future_result.join val was_timeout = @@ -585,17 +585,11 @@ else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt")) else result1 - val heap_digest = + val heap_shasum = if (result2.ok && do_store && store.output_heap(session_name).is_file) { - Some(ML_Heap.write_digest(store.output_heap(session_name))) + SHA1.shasum(ML_Heap.write_digest(store.output_heap(session_name)), session_name) } - else None - - val heap_shasum = - heap_digest match { - case None => "" - case Some(digest) => SHA1.shasum(digest, session_name) + "\n" - } + else SHA1.no_shasum (result2, heap_shasum) }