# HG changeset patch # User wenzelm # Date 1648033376 -3600 # Node ID 216c2ac23a8401b431dc97ace249f92a9991f4ad # Parent 6ed34e2e04ddfd64c7a962c5f6d46ac7a4005c04 clarified signature; diff -r 6ed34e2e04dd -r 216c2ac23a84 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed Mar 23 11:40:34 2022 +0100 +++ b/Admin/components/components.sha1 Wed Mar 23 12:02:56 2022 +0100 @@ -148,6 +148,7 @@ 309909ec6d43ae460338e9af54c1b2a48adcb1ec isabelle_setup-20210726.tar.gz a14ce46c62c64c3413f3cc9239242e33570d0f3d isabelle_setup-20210922.tar.gz b22066a9dcde6f813352dcf6404ac184440a22df isabelle_setup-20211109.tar.gz +91c5d29e9fa40aee015e8e65ffea043e218c2fc5 isabelle_setup-20220323.tar.gz 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz diff -r 6ed34e2e04dd -r 216c2ac23a84 Admin/components/main --- a/Admin/components/main Wed Mar 23 11:40:34 2022 +0100 +++ b/Admin/components/main Wed Mar 23 12:02:56 2022 +0100 @@ -9,7 +9,7 @@ flatlaf-1.6.4 idea-icons-20210508 isabelle_fonts-20211004 -isabelle_setup-20211109 +isabelle_setup-20220323 jdk-17.0.2+8 jedit-20211103 jfreechart-1.5.3 diff -r 6ed34e2e04dd -r 216c2ac23a84 src/Pure/General/sha1.scala --- a/src/Pure/General/sha1.scala Wed Mar 23 11:40:34 2022 +0100 +++ b/src/Pure/General/sha1.scala Wed Mar 23 12:02:56 2022 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/General/sha1.scala Author: Makarius -Digest strings according to SHA-1 (see RFC 3174). +SHA-1 message digest according to RFC 3174. */ package isabelle @@ -9,8 +9,8 @@ import java.io.{File => JFile, FileInputStream} import java.security.MessageDigest -import java.util.Locale -import java.math.BigInteger + +import isabelle.setup.{Build => Setup_Build} object SHA1 @@ -26,38 +26,27 @@ override def toString: String = rep } - private def sha1_digest(sha: MessageDigest): Digest = - new Digest(String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest()))) + def fake_digest(rep: String): Digest = new Digest(rep) - def fake(rep: String): Digest = new Digest(rep) + def make_digest(body: MessageDigest => Unit): Digest = + { + val digest_body = new Setup_Build.Digest_Body { def apply(sha: MessageDigest): Unit = body(sha)} + new Digest(Setup_Build.make_digest(digest_body)) + } def digest(file: JFile): Digest = - { - val digest = MessageDigest.getInstance("SHA") - - using(new FileInputStream(file))(stream => - { - val buf = new Array[Byte](65536) - var m = 0 - do { - m = stream.read(buf, 0, buf.length) - if (m != -1) digest.update(buf, 0, m) - } while (m != -1) - }) - - sha1_digest(digest) - } + make_digest(sha => using(new FileInputStream(file))(stream => + { + val buf = new Array[Byte](65536) + var m = 0 + do { + m = stream.read(buf, 0, buf.length) + if (m != -1) sha.update(buf, 0, m) + } while (m != -1) + })) def digest(path: Path): Digest = digest(path.file) - - def digest(bytes: Array[Byte]): Digest = - { - val digest = MessageDigest.getInstance("SHA") - digest.update(bytes) - - sha1_digest(digest) - } - + 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 = diff -r 6ed34e2e04dd -r 216c2ac23a84 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Wed Mar 23 11:40:34 2022 +0100 +++ b/src/Pure/Thy/document_build.scala Wed Mar 23 12:02:56 2022 +0100 @@ -81,7 +81,7 @@ { val name = res.string(Data.name) val sources = res.string(Data.sources) - Document_Input(name, SHA1.fake(sources)) + Document_Input(name, SHA1.fake_digest(sources)) }).toList) } @@ -96,7 +96,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(sources), log_xz, pdf)) + Some(Document_Output(name, SHA1.fake_digest(sources), log_xz, pdf)) } else None }) diff -r 6ed34e2e04dd -r 216c2ac23a84 src/Tools/Setup/src/Build.java --- a/src/Tools/Setup/src/Build.java Wed Mar 23 11:40:34 2022 +0100 +++ b/src/Tools/Setup/src/Build.java Wed Mar 23 12:02:56 2022 +0100 @@ -8,7 +8,6 @@ import java.io.BufferedOutputStream; -import java.io.ByteArrayOutputStream; import java.io.CharArrayWriter; import java.io.File; import java.io.IOException; @@ -44,6 +43,30 @@ public class Build { + /** SHA1 digest **/ + + @FunctionalInterface + public interface Digest_Body + { + void apply(MessageDigest sha) throws IOException, InterruptedException; + } + + public static String make_digest(Digest_Body body) + throws NoSuchAlgorithmException, IOException, InterruptedException + { + MessageDigest sha = MessageDigest.getInstance("SHA"); + body.apply(sha); + return String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); + } + + public static String make_shasum(String name, Digest_Body body) + throws NoSuchAlgorithmException, IOException, InterruptedException + { + return make_digest(body) + " " + name + "\n"; + } + + + /** context **/ public static String BUILD_PROPS = "build.props"; @@ -77,12 +100,6 @@ return List.copyOf(result); } - private static String sha_digest(MessageDigest sha, String name) - { - String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); - return digest + " " + name + "\n"; - } - public static class Context { private final Path _dir; @@ -181,37 +198,37 @@ } public String shasum(String name, List paths) - throws IOException, NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { - MessageDigest sha = MessageDigest.getInstance("SHA"); - for (Path file : paths) { - if (Files.isRegularFile(file)) { - sha.update(Files.readAllBytes(file)); - } - else { - throw new RuntimeException( - error_message("Bad input file " + Library.quote(file.toString()))); - } - } - return sha_digest(sha, name); + return make_shasum(name, sha -> + { + for (Path file : paths) { + if (Files.isRegularFile(file)) { + sha.update(Files.readAllBytes(file)); + } + else { + throw new RuntimeException( + error_message("Bad input file " + Library.quote(file.toString()))); + } + } + }); } public String shasum(String file) - throws IOException, NoSuchAlgorithmException, InterruptedException + throws NoSuchAlgorithmException, IOException, InterruptedException { return shasum(file, List.of(path(file))); } public String shasum_props() - throws NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { TreeMap sorted = new TreeMap(); for (Object x : _props.entrySet()) { sorted.put(x.toString(), _props.get(x)); } - MessageDigest sha = MessageDigest.getInstance("SHA"); - sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8)); - return sha_digest(sha, ""); + return make_shasum("", + sha -> sha.update(sorted.toString().getBytes(StandardCharsets.UTF_8))); } } @@ -423,7 +440,7 @@ /** build **/ public static void build(PrintStream output, Context context, boolean fresh) - throws IOException, InterruptedException, NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { String module = context.module_result(); if (!module.isEmpty()) { @@ -532,7 +549,7 @@ } public static void build_components(PrintStream output, boolean fresh) - throws IOException, InterruptedException, NoSuchAlgorithmException + throws NoSuchAlgorithmException, IOException, InterruptedException { for (Context context : component_contexts()) { build(output, context, fresh);