--- a/Admin/components/components.sha1 Mon Feb 06 15:41:23 2023 +0000
+++ b/Admin/components/components.sha1 Mon Feb 06 21:32:22 2023 +0100
@@ -164,6 +164,7 @@
171df3eb58bdac4cc495f773b797fa578f7d4be6 isabelle_setup-20220817.tar.gz
7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz
cb9f061ccd7c6f90d00c8aa115aeea8679f3f996 isabelle_setup-20221028.tar.gz
+f582c621471583d06e00007c6acc01376c7395af isabelle_setup-20230206.tar.gz
0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz
@@ -493,6 +494,7 @@
c4666a6d8080b5e376b50471fd2d9edeb1f9c988 vscode_extension-20220324.tar.gz
86c952d739d1eb868be88898982d4870a3d8c2dc vscode_extension-20220325.tar.gz
5293b9e77e5c887d449b671828b133fad4f18632 vscode_extension-20220829.tar.gz
+0d9551ffeb968813b6017278fa7ab9bd6062883f vscode_extension-20230206.tar.gz
67b271186631f84efd97246bf85f6d8cfaa5edfd vscodium-1.65.2.tar.gz
c439ab741e0cc49354cc03aa9af501202a5a38e3 vscodium-1.70.1.tar.gz
81d21dfd0ea5c58f375301f5166be9dbf8921a7a windows_app-20130716.tar.gz
--- a/Admin/components/main Mon Feb 06 15:41:23 2023 +0000
+++ b/Admin/components/main Mon Feb 06 21:32:22 2023 +0100
@@ -12,7 +12,7 @@
foiltex-2.1.4b
idea-icons-20210508
isabelle_fonts-20211004
-isabelle_setup-20221028
+isabelle_setup-20230206
jdk-17.0.6
jedit-20211103
jfreechart-1.5.3
@@ -35,7 +35,7 @@
stack-2.7.3
vampire-4.6
verit-2021.06.2-rmx
-vscode_extension-20220829
+vscode_extension-20230206
vscodium-1.70.1
xz-java-1.9
z3-4.4.0_4.4.1
--- a/etc/settings Mon Feb 06 15:41:23 2023 +0000
+++ b/etc/settings Mon Feb 06 21:32:22 2023 +0100
@@ -66,6 +66,7 @@
isabelle_directory '~'
isabelle_directory '$ISABELLE_HOME_USER'
isabelle_directory '~~'
+isabelle_directory '$ISABELLE_COMPONENTS_BASE'
ISABELLE_COMPONENT_REPOSITORY="https://isabelle.sketis.net/components"
ISABELLE_COMPONENTS_BASE="$USER_HOME/.isabelle/contrib"
--- a/src/Pure/Admin/build_history.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Admin/build_history.scala Mon Feb 06 21:32:22 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
}
--- a/src/Pure/General/file.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/General/file.scala Mon Feb 06 21:32:22 2023 +0100
@@ -55,8 +55,7 @@
/* symbolic path representation, e.g. "~~/src/Pure/ROOT.ML" */
def symbolic_path(path: Path): String = {
- val directories =
- Library.space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
+ val directories = space_explode(':', Isabelle_System.getenv("ISABELLE_DIRECTORIES")).reverse
val full_name = standard_path(path)
directories.view.flatMap(a =>
try {
@@ -75,10 +74,7 @@
/* platform files */
def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
- def absolute_name(file: JFile): String = absolute(file).getPath
-
def canonical(file: JFile): JFile = file.getCanonicalFile
- def canonical_name(file: JFile): String = canonical(file).getPath
def path(file: JFile): Path = Path.explode(standard_path(file))
def path(java_path: JPath): Path = path(java_path.toFile)
--- a/src/Pure/General/mercurial.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/General/mercurial.scala Mon Feb 06 21:32:22 2023 +0100
@@ -248,7 +248,7 @@
def tags(rev: String = "tip"): String = {
val result = identify(rev, options = "-t")
- Library.space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
+ space_explode(' ', result).filterNot(_ == "tip").mkString(" ")
}
def paths(args: String = "", options: String = ""): List[String] =
--- a/src/Pure/General/sha1.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/General/sha1.scala Mon Feb 06 21:32:22 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
@@ -22,7 +24,6 @@
case other: Digest => rep == other.toString
case _ => false
}
- def shasum(name: String): String = rep + " " + name
}
def fake_digest(rep: String): Digest = new Digest(rep)
@@ -47,8 +48,42 @@
def digest(bytes: Array[Byte]): Digest = make_digest(_.update(bytes))
def digest(bytes: Bytes): Digest = bytes.sha1_digest
def digest(string: String): Digest = digest(Bytes(string))
- def digest_set(digests: List[Digest]): Digest =
- digest(cat_lines(digests.map(_.toString).sorted))
val digest_length: Int = digest("").toString.length
+
+
+ /* 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 :::(other: Shasum): Shasum = new Shasum(other.rep ::: rep)
+
+ 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)
+ def shasum_sorted(args: List[(Digest, String)]): Shasum =
+ flat_shasum(args.sortBy(_._2).map(shasum))
}
--- a/src/Pure/ML/ml_heap.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/ML/ml_heap.scala Mon Feb 06 21:32:22 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
}
}
--- a/src/Pure/ML/ml_statistics.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/ML/ml_statistics.scala Mon Feb 06 21:32:22 2023 +0100
@@ -54,7 +54,7 @@
consume: Properties.T => Unit = Console.println
): Unit = {
def progress_stdout(line: String): Unit = {
- val props = Library.space_explode(',', line).flatMap(Properties.Eq.unapply)
+ val props = space_explode(',', line).flatMap(Properties.Eq.unapply)
if (props.nonEmpty) consume(props)
}
--- a/src/Pure/PIDE/document_editor.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/PIDE/document_editor.scala Mon Feb 06 21:32:22 2023 +0100
@@ -17,8 +17,8 @@
def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output")
def document_output(name: String): Path = document_output_dir() + Path.basic(name)
- object Meta_Data {
- def read(name: String = document_name): Option[Meta_Data] = {
+ object Meta_Info {
+ def read(name: String = document_name): Option[Meta_Info] = {
val json_path = document_output(name).json
if (json_path.is_file) {
val json = JSON.parse(File.read(json_path))
@@ -28,7 +28,7 @@
log <- JSON.string(json, "log")
pdf <- JSON.string(json, "pdf")
} yield {
- Meta_Data(name,
+ Meta_Info(name,
SortedSet.from(selection),
SHA1.fake_digest(sources),
SHA1.fake_digest(log),
@@ -53,7 +53,7 @@
}
}
- sealed case class Meta_Data(
+ sealed case class Meta_Info(
name: String,
selection: SortedSet[String],
sources: SHA1.Digest,
@@ -77,7 +77,7 @@
val output = document_output(name)
File.write(output.log, doc.log)
Bytes.write(output.pdf, doc.pdf)
- Meta_Data.write(selection, doc, name = name)
+ Meta_Info.write(selection, doc, name = name)
}
def view_document(name: String = document_name): Unit = {
@@ -171,9 +171,9 @@
val variant = document_session.get_variant
val directory = engine.prepare_directory(context, tmp_dir, variant, verbose = true)
val ok =
- Meta_Data.read() match {
- case Some(meta_data) =>
- meta_data.check_files() && meta_data.sources == directory.sources
+ Meta_Info.read() match {
+ case Some(meta_info) =>
+ meta_info.check_files() && meta_info.sources == directory.sources
case None => false
}
if (!ok) {
--- a/src/Pure/System/components.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/System/components.scala Mon Feb 06 21:32:22 2023 +0100
@@ -217,19 +217,19 @@
val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1")
- sealed case class SHA1_Digest(digest: SHA1.Digest, name: String) {
- override def toString: String = digest.shasum(name)
+ sealed case class SHA1_Entry(digest: SHA1.Digest, name: String) {
+ override def toString: String = SHA1.shasum(digest, name).toString
}
- def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] =
+ def read_components_sha1(lines: List[String] = Nil): List[SHA1_Entry] =
(proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line =>
Word.explode(line) match {
case Nil => None
- case List(sha1, name) => Some(SHA1_Digest(SHA1.fake_digest(sha1), name))
+ case List(sha1, name) => Some(SHA1_Entry(SHA1.fake_digest(sha1), name))
case _ => error("Bad components.sha1 entry: " + quote(line))
})
- def write_components_sha1(entries: List[SHA1_Digest]): Unit =
+ def write_components_sha1(entries: List[SHA1_Entry]): Unit =
File.write(components_sha1, entries.sortBy(_.name).mkString("", "\n", "\n"))
@@ -243,7 +243,7 @@
def write_components(lines: List[String]): Unit = {
Isabelle_System.make_directory(components_path.dir)
- File.write(components_path, Library.terminate_lines(lines))
+ File.write(components_path, terminate_lines(lines))
}
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
@@ -384,7 +384,7 @@
yield {
val name = archive.file_name
progress.echo("Digesting local " + name)
- SHA1_Digest(SHA1.digest(archive), name)
+ SHA1_Entry(SHA1.digest(archive), name)
}
val new_names = new_entries.map(_.name).toSet
--- a/src/Pure/System/executable.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/System/executable.scala Mon Feb 06 21:32:22 2023 +0100
@@ -20,7 +20,7 @@
val ldd_lines = {
val ldd = if (Platform.is_macos) "otool -L" else "ldd"
val script = mingw.bash_script(ldd + " " + File.bash_path(exe))
- Library.split_lines(Isabelle_System.bash(script, cwd = exe_dir.file).check.out)
+ split_lines(Isabelle_System.bash(script, cwd = exe_dir.file).check.out)
}
def lib_name(lib: String): String =
--- a/src/Pure/System/isabelle_system.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/System/isabelle_system.scala Mon Feb 06 21:32:22 2023 +0100
@@ -510,8 +510,7 @@
def open_external_file(name: String): Boolean = {
val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString
val external =
- ext.nonEmpty &&
- Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
+ ext.nonEmpty && space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext)
if (external) {
if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name))
else open(name)
--- a/src/Pure/Thy/bibtex.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/bibtex.scala Mon Feb 06 21:32:22 2023 +0100
@@ -202,7 +202,7 @@
override def toString: String = "Bibtex.Entries(" + entries.length + ")"
def ::: (other: Entries): Entries =
- new Entries(entries ::: other.entries, errors ::: other.errors)
+ new Entries(other.entries ::: entries, other.errors ::: errors)
}
object Session_Entries extends Scala.Fun("bibtex_session_entries") {
@@ -703,7 +703,7 @@
/* cite commands */
def cite_commands(options: Options): List[String] =
- Library.space_explode(',', options.string("document_cite_commands"))
+ space_explode(',', options.string("document_cite_commands"))
val CITE = "cite"
val NOCITE = "nocite"
@@ -828,7 +828,7 @@
val location =
if (loc.startsWith("[") && loc.endsWith("]")) loc.substring(1, loc.length - 1)
else loc
- val citations = Library.space_explode(',', m.group(3)).map(_.trim)
+ val citations = space_explode(',', m.group(3)).map(_.trim)
Regex.quoteReplacement(cite_antiquotation(name, location, citations))
})
--- a/src/Pure/Thy/browser_info.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/browser_info.scala Mon Feb 06 21:32:22 2023 +0100
@@ -36,16 +36,16 @@
}
- /* meta data within the file-system */
+ /* meta info within the file-system */
- object Meta_Data {
+ object Meta_Info {
/* directory */
val PATH: Path = Path.explode(".browser_info")
def check_directory(dir: Path): Unit = {
if (dir.is_dir && !(dir + PATH).is_dir && File.read_dir(dir).nonEmpty) {
- error("Existing content in " + dir.expand + " lacks " + PATH + " meta data.\n" +
+ error("Existing content in " + dir.expand + " lacks " + PATH + " meta info.\n" +
"To avoid potential disaster, it has not been changed automatically.\n" +
"If this is the intended directory, please move/remove/empty it manually.")
}
@@ -284,10 +284,10 @@
/* maintain presentation structure */
def update_chapter(session_name: String, session_description: String): Unit = synchronized {
- val dir = Meta_Data.init_directory(chapter_dir(session_name))
- Meta_Data.change(dir, Meta_Data.INDEX) { text =>
- val index0 = Meta_Data.Index.parse(text, "chapter")
- val item = Meta_Data.Item(session_name, description = session_description)
+ val dir = Meta_Info.init_directory(chapter_dir(session_name))
+ Meta_Info.change(dir, Meta_Info.INDEX) { text =>
+ val index0 = Meta_Info.Index.parse(text, "chapter")
+ val item = Meta_Info.Item(session_name, description = session_description)
val index = index0 + item
if (index != index0) {
@@ -311,17 +311,17 @@
}
def update_root(): Unit = synchronized {
- Meta_Data.init_directory(root_dir)
+ Meta_Info.init_directory(root_dir)
HTML.init_fonts(root_dir)
Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
root_dir + Path.explode("isabelle.gif"))
- Meta_Data.change(root_dir, Meta_Data.INDEX) { text =>
- val index0 = Meta_Data.Index.parse(text, "root")
+ Meta_Info.change(root_dir, Meta_Info.INDEX) { text =>
+ val index0 = Meta_Info.Index.parse(text, "root")
val index = {
val items1 =
sessions_structure.known_chapters
- .map(ch => Meta_Data.Item(ch.name, description = ch.description))
+ .map(ch => Meta_Info.Item(ch.name, description = ch.description))
val items2 = index0.items.filterNot(item => items1.exists(_.name == item.name))
index0.copy(items = items1 ::: items2)
}
@@ -559,8 +559,8 @@
val session_dir = context.session_dir(session_name).expand
progress.echo("Presenting " + session_name + " in " + session_dir + " ...")
- Meta_Data.init_directory(context.chapter_dir(session_name))
- Meta_Data.clean_directory(session_dir)
+ Meta_Info.init_directory(context.chapter_dir(session_name))
+ Meta_Info.clean_directory(session_dir)
val session = context.document_info.the_session(session_name)
@@ -662,7 +662,7 @@
context.contents("Theories", theories),
root = Some(context.root_dir))
- Meta_Data.set_build_uuid(session_dir, session.build_uuid)
+ Meta_Info.set_build_uuid(session_dir, session.build_uuid)
context.update_chapter(session_name, session_info.description)
}
@@ -688,7 +688,7 @@
case None => false
case Some(build) =>
val session_dir = context0.session_dir(session_name)
- !Meta_Data.check_build_uuid(session_dir, build.uuid)
+ !Meta_Info.check_build_uuid(session_dir, build.uuid)
}
}
}
--- a/src/Pure/Thy/document_build.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/document_build.scala Mon Feb 06 21:32:22 2023 +0100
@@ -19,7 +19,7 @@
object Document_Variant {
def parse(opt: String): Document_Variant =
- Library.space_explode('=', opt) match {
+ space_explode('=', opt) match {
case List(name) => Document_Variant(name, Latex.Tags.empty)
case List(name, tags) => Document_Variant(name, Latex.Tags(tags))
case _ => error("Malformed document variant: " + quote(opt))
@@ -30,10 +30,10 @@
def print: String = if (tags.toString.isEmpty) name else name + "=" + tags.toString
}
- sealed case class Document_Input(name: String, sources: SHA1.Digest)
+ sealed case class Document_Input(name: String, sources: SHA1.Shasum)
extends Document_Name { override def toString: String = name }
- sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes)
+ sealed case class Document_Output(name: String, sources: SHA1.Shasum, log_xz: Bytes, pdf: Bytes)
extends Document_Name {
override def toString: String = name
@@ -74,7 +74,7 @@
stmt.execute_query().iterator({ res =>
val name = res.string(Data.name)
val sources = res.string(Data.sources)
- Document_Input(name, SHA1.fake_digest(sources))
+ Document_Input(name, SHA1.fake_shasum(sources))
}).toList)
}
@@ -91,7 +91,7 @@
val sources = res.string(Data.sources)
val log_xz = res.bytes(Data.log_xz)
val pdf = res.bytes(Data.pdf)
- Some(Document_Output(name, SHA1.fake_digest(sources), log_xz, pdf))
+ Some(Document_Output(name, SHA1.fake_shasum(sources), log_xz, pdf))
}
else None
})
@@ -228,7 +228,7 @@
lazy val session_tex: File.Content = {
val path = Path.basic("session.tex")
val content =
- Library.terminate_lines(
+ terminate_lines(
session_document_theories.map(name => "\\input{" + tex_name(name) + "}"))
File.content(path, content)
}
@@ -304,9 +304,16 @@
val root_name1 = "root_" + doc.name
val root_name = if ((doc_dir + Path.explode(root_name1).tex).is_file) root_name1 else "root"
- val digests1 = List(doc.print, document_logo.toString, document_build).map(SHA1.digest)
- val digests2 = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest)
- val sources = SHA1.digest_set(digests1 ::: digests2)
+ val meta_info =
+ SHA1.shasum_meta_info(
+ SHA1.digest(List(doc.print, document_logo.toString, document_build).toString))
+
+ val manifest =
+ SHA1.shasum_sorted(
+ for (file <- File.find_files(doc_dir.file, follow_links = true))
+ yield SHA1.digest(file) -> File.path(doc_dir.java_path.relativize(file.toPath)).implode)
+
+ val sources = meta_info ::: manifest
/* derived material: without SHA1 digest */
@@ -338,7 +345,7 @@
doc_dir: Path,
doc: Document_Variant,
root_name: String,
- sources: SHA1.Digest
+ sources: SHA1.Shasum
) {
def root_name_script(ext: String = ""): String =
Bash.string(if (ext.isEmpty) root_name else root_name + "." + ext)
--- a/src/Pure/Thy/latex.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/latex.scala Mon Feb 06 21:32:22 2023 +0100
@@ -99,8 +99,7 @@
val standard = "document,theory,proof,ML,visible,-invisible,important,unimportant"
- private def explode(spec: String): List[String] =
- Library.space_explode(',', spec)
+ private def explode(spec: String): List[String] = space_explode(',', spec)
def apply(spec: String): Tags =
new Tags(spec,
@@ -142,7 +141,7 @@
\newcommand{\isafoldtag}[1]%
{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
-""" + Library.terminate_lines(tags))
+""" + terminate_lines(tags))
}
}
--- a/src/Pure/Thy/sessions.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Thy/sessions.scala Mon Feb 06 21:32:22 2023 +0100
@@ -142,6 +142,8 @@
", loaded_theories = " + loaded_theories.size +
", used_theories = " + used_theories.length
+ def all_sources: List[(Path, SHA1.Digest)] = imported_sources ::: session_sources
+
def all_document_theories: List[Document.Node.Name] =
proper_session_theories ::: document_theories
@@ -273,11 +275,14 @@
def apply(name: String): Base = session_bases(name)
def get(name: String): Option[Base] = session_bases.get(name)
- def imported_sources(name: String): List[SHA1.Digest] =
- session_bases(name).imported_sources.map(_._2)
-
- def session_sources(name: String): List[SHA1.Digest] =
- session_bases(name).session_sources.map(_._2)
+ def sources_shasum(name: String): SHA1.Shasum = {
+ val meta_info = SHA1.shasum_meta_info(sessions_structure(name).meta_digest)
+ val sources =
+ SHA1.shasum_sorted(
+ for ((path, digest) <- apply(name).all_sources)
+ yield digest -> File.symbolic_path(path))
+ meta_info ::: sources
+ }
def errors: List[String] =
(for {
@@ -684,7 +689,7 @@
def document_variants: List[Document_Build.Document_Variant] = {
val variants =
- Library.space_explode(':', options.string("document_variants")).
+ space_explode(':', options.string("document_variants")).
map(Document_Build.Document_Variant.parse)
val dups = Library.duplicates(variants.map(_.name))
@@ -1403,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): SHA1.Shasum =
+ (for {
+ path <- find_heap(name)
+ digest <- ML_Heap.read_digest(path)
+ } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum)
def the_heap(name: String): Path =
find_heap(name) getOrElse
@@ -1557,9 +1565,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) = cat_lines(build.input_heaps)
- stmt.string(10) = build.output_heap getOrElse ""
+ 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()
@@ -1600,9 +1608,9 @@
catch { case _: SQLException => "" }
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) },
+ 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))
}
--- a/src/Pure/Tools/build.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Tools/build.scala Mon Feb 06 21:32:22 2023 +0100
@@ -18,9 +18,9 @@
/* persistent build info */
sealed case class Session_Info(
- sources: String,
- input_heaps: List[String],
- output_heap: Option[String],
+ sources: SHA1.Shasum,
+ input_heaps: SHA1.Shasum,
+ output_heap: SHA1.Shasum,
return_code: Int,
uuid: String
) {
@@ -209,14 +209,6 @@
augment_options = augment_options)
val full_sessions_selection = full_sessions.imports_selection(selection)
- def sources_stamp(deps: Sessions.Deps, session_name: String): String = {
- val digests =
- full_sessions(session_name).meta_digest ::
- deps.session_sources(session_name) :::
- deps.imported_sources(session_name)
- SHA1.digest_set(digests).toString
- }
-
val build_deps = {
val deps0 =
Sessions.deps(full_sessions.selection(selection),
@@ -230,7 +222,7 @@
case Some(db) =>
using(db)(store.read_build(_, name)) match {
case Some(build)
- if build.ok && build.sources == sources_stamp(deps0, name) => None
+ if build.ok && build.sources == deps0.sources_shasum(name) => None
case _ => Some(name)
}
case None => Some(name)
@@ -279,7 +271,7 @@
// scheduler loop
case class Result(
current: Boolean,
- heap_digest: Option[String],
+ output_heap: SHA1.Shasum,
process: Option[Process_Result],
info: Sessions.Info
) {
@@ -306,7 +298,7 @@
@tailrec def loop(
pending: Queue,
- running: Map[String, (List[String], Build_Job)],
+ running: Map[String, (SHA1.Shasum, Build_Job)],
results: Map[String, Result]
): Map[String, Result] = {
def used_node(i: Int): Boolean =
@@ -323,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 = {
@@ -354,7 +346,7 @@
build_log =
if (process_result.timeout) build_log.error("Timeout") else build_log,
build =
- Session_Info(sources_stamp(build_deps, 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
@@ -371,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
@@ -380,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")))
}
- else ancestor_results.flatMap(_.heap_digest)
+ else SHA1.flat_shasum(ancestor_results.map(_.output_heap))
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 == sources_stamp(build_deps, 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.sources == build_deps.sources_shasum(session_name) &&
+ build.input_heaps == input_heaps &&
+ build.output_heap == output_heap &&
+ !(do_store && output_heap.is_empty)
+ (current, output_heap)
+ case None => (false, SHA1.no_shasum)
}
- case None => (false, None)
+ case None => (false, SHA1.no_shasum)
}
}
val all_current = current && ancestor_results.forall(_.current)
@@ -413,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 + " ...")
@@ -432,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)
}
--- a/src/Pure/Tools/build_job.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Tools/build_job.scala Mon Feb 06 21:32:22 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, SHA1.Shasum) = {
val result1 = future_result.join
val was_timeout =
@@ -585,12 +585,12 @@
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
+ else SHA1.no_shasum
- (result2, heap_digest)
+ (result2, heap_shasum)
}
}
--- a/src/Pure/Tools/dotnet_setup.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Pure/Tools/dotnet_setup.scala Mon Feb 06 21:32:22 2023 +0100
@@ -186,7 +186,7 @@
"V:" -> (arg => version = arg),
"f" -> (_ => force = true),
"n" -> (_ => dry_run = true),
- "p:" -> (arg => platforms = Library.space_explode(',', arg).map(check_platform_spec)),
+ "p:" -> (arg => platforms = space_explode(',', arg).map(check_platform_spec)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
--- a/src/Tools/Setup/src/Build.java Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/Setup/src/Build.java Mon Feb 06 21:32:22 2023 +0100
@@ -74,6 +74,7 @@
public static String BUILD_PROPS = "build.props";
public static String COMPONENT_BUILD_PROPS = "etc/build.props";
+ public static String META_INFO = "<meta_info>";
public static String TITLE = "title";
public static String MODULE = "module";
@@ -223,14 +224,14 @@
return shasum(file, List.of(path(file)));
}
- public String shasum_props()
+ public String shasum_meta_info()
throws NoSuchAlgorithmException, IOException, InterruptedException
{
TreeMap<String,Object> sorted = new TreeMap<String,Object>();
for (Object x : _props.entrySet()) {
sorted.put(x.toString(), _props.get(x));
}
- return make_shasum("<props>",
+ return make_shasum(META_INFO,
sha -> sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8)));
}
}
@@ -475,7 +476,7 @@
List<Path> compiler_deps = new LinkedList<Path>();
{
StringBuilder _shasum = new StringBuilder();
- _shasum.append(context.shasum_props());
+ _shasum.append(context.shasum_meta_info());
for (String s : requirements) {
List<Path> paths = context.requirement_paths(s);
compiler_deps.addAll(paths);
--- a/src/Tools/VSCode/src/build_vscode_extension.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala Mon Feb 06 21:32:22 2023 +0100
@@ -160,19 +160,19 @@
Isabelle_System.with_tmp_dir("build") { build_dir =>
val manifest_text = File.read(VSCode_Main.extension_dir + VSCode_Main.MANIFEST)
val manifest_entries = split_lines(manifest_text).filter(_.nonEmpty)
- val manifest_shasum: String = {
- val a = SHA1.digest(manifest_text).shasum("<MANIFEST>")
+ val manifest_shasum: SHA1.Shasum = {
+ val a = SHA1.shasum_meta_info(SHA1.digest(manifest_text))
val bs =
- for (entry <- manifest_entries)
- yield SHA1.digest(VSCode_Main.extension_dir + Path.explode(entry)).shasum(entry)
- terminate_lines(a :: bs)
+ for (name <- manifest_entries)
+ yield SHA1.shasum(SHA1.digest(VSCode_Main.extension_dir + Path.explode(name)), name)
+ SHA1.flat_shasum(a :: bs)
}
- for (entry <- manifest_entries) {
- val path = Path.explode(entry)
+ for (name <- manifest_entries) {
+ val path = Path.explode(name)
Isabelle_System.copy_file(VSCode_Main.extension_dir + path,
Isabelle_System.make_directory(build_dir + path.dir))
}
- File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum)
+ File.write(build_dir + VSCode_Main.MANIFEST.shasum, manifest_shasum.toString)
build_grammar(options, build_dir, logic = logic, dirs = dirs, progress = progress)
--- a/src/Tools/VSCode/src/build_vscodium.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/build_vscodium.scala Mon Feb 06 21:32:22 2023 +0100
@@ -426,7 +426,7 @@
for targeting Windows.
""",
"D:" -> (arg => target_dir = Path.explode(arg)),
- "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)),
+ "p:" -> (arg => platforms = space_explode(',', arg).map(Platform.Family.parse)),
"v" -> (_ => verbose = true))
val more_args = getopts(args)
--- a/src/Tools/VSCode/src/vscode_main.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/vscode_main.scala Mon Feb 06 21:32:22 2023 +0100
@@ -81,7 +81,7 @@
val MANIFEST: Path = Path.explode("MANIFEST")
- private def shasum_vsix(vsix_path: Path): String = {
+ private def shasum_vsix(vsix_path: Path): SHA1.Shasum = {
val name = "extension/MANIFEST.shasum"
def err(): Nothing = error("Cannot retrieve " + quote(name) + " from " + vsix_path)
if (vsix_path.is_file) {
@@ -91,16 +91,16 @@
case entry =>
zip_file.getInputStream(entry) match {
case null => err()
- case stream => File.read_stream(stream)
+ case stream => SHA1.fake_shasum(File.read_stream(stream))
}
})
}
else err()
}
- private def shasum_dir(dir: Path): Option[String] = {
+ private def shasum_dir(dir: Path): Option[SHA1.Shasum] = {
val path = dir + MANIFEST.shasum
- if (path.is_file) Some(File.read(path)) else None
+ if (path.is_file) Some(SHA1.fake_shasum(File.read(path))) else None
}
def locate_extension(): Option[Path] = {
--- a/src/Tools/VSCode/src/vscode_resources.scala Mon Feb 06 15:41:23 2023 +0000
+++ b/src/Tools/VSCode/src/vscode_resources.scala Mon Feb 06 21:32:22 2023 +0100
@@ -107,7 +107,7 @@
else if (path.is_basic && !prefix.endsWith("/") && !prefix.endsWith(JFile.separator))
prefix + JFile.separator + File.platform_path(path)
else if (path.is_basic) prefix + File.platform_path(path)
- else File.absolute_name(new JFile(prefix + JFile.separator + File.platform_path(path)))
+ else File.absolute(new JFile(prefix + JFile.separator + File.platform_path(path))).getPath
}
override def read_dir(dir: String): List[String] =