# HG changeset patch # User wenzelm # Date 1625774828 -7200 # Node ID 731ab64bae972a6296c4544149322ae544b880ea # Parent 75b29d65228e12b07cef737391a92519a8894dc0 more compiler_deps via "requirements", notably jar list from settings; proper Files.createDirectories; diff -r 75b29d65228e -r 731ab64bae97 src/Tools/Setup/isabelle/setup/Build.java --- a/src/Tools/Setup/isabelle/setup/Build.java Thu Jul 08 16:27:35 2021 +0200 +++ b/src/Tools/Setup/isabelle/setup/Build.java Thu Jul 08 22:07:08 2021 +0200 @@ -69,6 +69,7 @@ } return List.copyOf(list); } + public List requirements() { return get_list("requirements"); } public List sources() { return get_list("sources"); } public List resources() { return get_list("resources"); } public List services() { return get_list("services"); } @@ -91,16 +92,28 @@ return i > 0 ? s.substring(i + 1) : s; } + public String shasum(String name, List paths) + throws IOException, NoSuchAlgorithmException + { + boolean exists = false; + MessageDigest sha = MessageDigest.getInstance("SHA"); + for (Path file : paths) { + if (Files.exists(file)) { + exists = true; + sha.update(Files.readAllBytes(file)); + } + } + if (exists) { + String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); + return digest + " " + name + "\n"; + } + else { return ""; } + } + public String shasum(String file) throws IOException, NoSuchAlgorithmException { - if (exists(file)) { - MessageDigest sha = MessageDigest.getInstance("SHA"); - sha.update(Files.readAllBytes(path(file))); - String digest = String.format(Locale.ROOT, "%040x", new BigInteger(1, sha.digest())); - return digest + " " + file + "\n"; - } - else { return ""; } + return shasum(file, List.of(path(file))); } } @@ -152,7 +165,7 @@ throws IOException { Path path = dir.resolve(SHASUM); - Files.createDirectories(dir.getParent()); + Files.createDirectories(path.getParent()); Files.writeString(path, shasum); } @@ -199,8 +212,9 @@ String jar_name = context.jar_name(); Path jar_path = context.path(jar_name); + List requirements = context.requirements(); + List resources = context.resources(); List sources = context.sources(); - List resources = context.resources(); Files.deleteIfExists(context.shasum_path()); @@ -210,8 +224,26 @@ else { String shasum_old = get_shasum(jar_path); String shasum; + List compiler_deps = new LinkedList(); { StringBuilder _shasum = new StringBuilder(); + for (String s : requirements) { + if (s.startsWith("@$")) { + List paths = new LinkedList(); + for (String p : Environment.getenv(s.substring(2)).split(":", -1)) { + if (!p.isEmpty()) { + Path path = Path.of(Environment.platform_path(p)); + compiler_deps.add(path); + paths.add(path); + } + } + _shasum.append(context.shasum(s, paths)); + } + else { + compiler_deps.add(context.path(s)); + _shasum.append(context.shasum(s)); + } + } for (String s : resources) { _shasum.append(context.shasum(context.item_name(s))); } @@ -229,7 +261,6 @@ try { /* compile sources */ - List compiler_deps = new LinkedList(); for (String s : isabelle_class_path.split(":", -1)) { if (!s.isEmpty()) { compiler_deps.add(Path.of(Environment.platform_path(s)));