# HG changeset patch # User wenzelm # Date 1626522141 -7200 # Node ID 0701ff55780d7250bbc34c66eaa24ebb6c661094 # Parent 77cc23b550e93cfdf99029f13a0d9af97224d1aa clarified build_props: empty module means no build; clarified signature; clarified errors; diff -r 77cc23b550e9 -r 0701ff55780d Admin/components/components.sha1 --- a/Admin/components/components.sha1 Sat Jul 17 12:59:47 2021 +0200 +++ b/Admin/components/components.sha1 Sat Jul 17 13:42:21 2021 +0200 @@ -128,6 +128,7 @@ d2c9fd7b73457a460111edd6eb93a133272935fb isabelle_setup-20210715.tar.gz a5f478ba1088f67c2c86dc2fa7764b6d884e5ae5 isabelle_setup-20210716-1.tar.gz 79fad009cb22aa5e7cb4aed3c810ad5f61790293 isabelle_setup-20210716.tar.gz +14f8508bcae9140815bb23e430e26d2cbc504b81 isabelle_setup-20210717.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 77cc23b550e9 -r 0701ff55780d Admin/components/main --- a/Admin/components/main Sat Jul 17 12:59:47 2021 +0200 +++ b/Admin/components/main Sat Jul 17 13:42:21 2021 +0200 @@ -8,7 +8,7 @@ flatlaf-1.2 idea-icons-20210508 isabelle_fonts-20210322 -isabelle_setup-20210716-1 +isabelle_setup-20210717 jdk-15.0.2+7 jedit-20210715 jfreechart-1.5.1 diff -r 77cc23b550e9 -r 0701ff55780d Admin/etc/build.props --- a/Admin/etc/build.props Sat Jul 17 12:59:47 2021 +0200 +++ b/Admin/etc/build.props Sat Jul 17 13:42:21 2021 +0200 @@ -1,4 +1,3 @@ -description = Isabelle/Scala/Admin -lib = $ISABELLE_HOME/lib/classes -name = isabelle_admin +title = Isabelle/Scala/Admin +module = $ISABELLE_HOME/lib/classes/isabelle_admin.jar services = isabelle.Admin_Tools diff -r 77cc23b550e9 -r 0701ff55780d etc/build.props --- a/etc/build.props Sat Jul 17 12:59:47 2021 +0200 +++ b/etc/build.props Sat Jul 17 13:42:21 2021 +0200 @@ -1,6 +1,5 @@ -description = Isabelle/Scala -lib = lib/classes -name = isabelle +title = Isabelle/Scala +module = $ISABELLE_HOME/lib/classes/isabelle.jar main = isabelle.jedit.Main resources = \ lib/services/java.nio.charset.spi.CharsetProvider:META-INF/services/ \ diff -r 77cc23b550e9 -r 0701ff55780d src/Tools/GraphBrowser/etc/build.props --- a/src/Tools/GraphBrowser/etc/build.props Sat Jul 17 12:59:47 2021 +0200 +++ b/src/Tools/GraphBrowser/etc/build.props Sat Jul 17 13:42:21 2021 +0200 @@ -1,6 +1,5 @@ -description = graph browser -lib = $ISABELLE_HOME/lib/classes -name = isabelle_graphbrowser +title = graph browser +module = $ISABELLE_HOME/lib/classes/isabelle_graphbrowser.jar javac_options = -source 7 -target 7 sources = \ awt/Border.java \ diff -r 77cc23b550e9 -r 0701ff55780d src/Tools/Setup/isabelle/setup/Build.java --- a/src/Tools/Setup/isabelle/setup/Build.java Sat Jul 17 12:59:47 2021 +0200 +++ b/src/Tools/Setup/isabelle/setup/Build.java Sat Jul 17 13:42:21 2021 +0200 @@ -55,17 +55,18 @@ throws IOException { Properties props = new Properties(); - props.load(Files.newBufferedReader(dir.resolve(BUILD_PROPS))); - return new Context(dir, props); + Path props_path = dir.resolve(BUILD_PROPS); + props.load(Files.newBufferedReader(props_path)); + return new Context(dir, props, props_path.toString()); } public static Context component_context(Path dir) throws IOException { Properties props = new Properties(); - Path build_props = dir.resolve(COMPONENT_BUILD_PROPS); - if (Files.exists(build_props)) { props.load(Files.newBufferedReader(build_props)); } - return new Context(dir, props); + Path props_path = dir.resolve(COMPONENT_BUILD_PROPS); + if (Files.exists(props_path)) { props.load(Files.newBufferedReader(props_path)); } + return new Context(dir, props, props_path.toString()); } public static List component_contexts() @@ -93,24 +94,36 @@ { private final Path _dir; private final Properties _props; + private final String _location; - public Context(Path dir, Properties props) + public Context(Path dir, Properties props, String location) { _dir = dir; _props = props; + _location = location; } @Override public String toString() { return _dir.toString(); } - public String name() { return _props.getProperty("name", _dir.toFile().getName()); } - public String description() { return _props.getProperty("description", name()); } + public String error_message(String msg) + { + if (_location == null || _location.isEmpty()) { + return msg; + } + else { + return msg +" (in " + Library.quote(_location) + ")"; + } + } - public String lib_name() { return _props.getProperty("lib", "lib") + "/" + name(); } - public String jar_name() { return lib_name() + ".jar"; } + public String title() { + String title = _props.getProperty("title", ""); + if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); } + else return title; + } + public String module() { return _props.getProperty("module", ""); } public String scalac_options() { return _props.getProperty("scalac_options", ""); } public String javac_options() { return _props.getProperty("javac_options", ""); } - public String main() { return _props.getProperty("main", ""); } private List get_list(String name) @@ -164,7 +177,7 @@ } else { throw new RuntimeException( - "Missing input file " + Environment.quote(file.toString())); + error_message("Missing input file " + Library.quote(file.toString()))); } } return sha_digest(sha, name); @@ -393,7 +406,8 @@ { List result = new LinkedList(); for (Context context : component_contexts()) { - result.add(context.path(context.jar_name())); + String module = context.module(); + if (!module.isEmpty()) { result.add(context.path(module)); } } return List.copyOf(result); } @@ -416,108 +430,116 @@ public static void build(Context context, boolean fresh) throws IOException, InterruptedException, NoSuchAlgorithmException { - String jar_name = context.jar_name(); - Path jar_path = context.path(jar_name); + String module = context.module(); + if (!module.isEmpty()) { + String title = context.title(); - List requirements = context.requirements(); - List resources = context.resources(); - List sources = context.sources(); + Path jar_path = context.path(module); + String jar_name = jar_path.toString(); + if (!jar_name.endsWith(".jar")) { + throw new RuntimeException( + context.error_message("Bad jar module " + Library.quote(jar_name))); + } + + if (context.is_vacuous()) { Files.deleteIfExists(jar_path); } + else { + List requirements = context.requirements(); + List resources = context.resources(); + List sources = context.sources(); - if (context.is_vacuous()) { Files.deleteIfExists(jar_path); } - else { - String shasum_old = get_shasum(jar_path); - String shasum; - List compiler_deps = new LinkedList(); - { - StringBuilder _shasum = new StringBuilder(); - _shasum.append(context.shasum_props()); - for (String s : requirements) { - if (s.startsWith("env:")) { - List paths = new LinkedList(); - for (String p : Environment.getenv(s.substring(4)).split(":", -1)) { - if (!p.isEmpty()) { - Path path = Path.of(Environment.platform_path(p)); - compiler_deps.add(path); - paths.add(path); + String shasum_old = get_shasum(jar_path); + String shasum; + List compiler_deps = new LinkedList(); + { + StringBuilder _shasum = new StringBuilder(); + _shasum.append(context.shasum_props()); + for (String s : requirements) { + if (s.startsWith("env:")) { + List paths = new LinkedList(); + for (String p : Environment.getenv(s.substring(4)).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))); + } + for (String s : sources) { _shasum.append(context.shasum(s)); } + shasum = _shasum.toString(); + } + if (fresh || !shasum_old.equals(shasum)) { + System.out.print("### Building " + title + " (" + jar_path + ") ...\n"); + + String isabelle_classpath = Environment.getenv("ISABELLE_CLASSPATH"); + + Path build_dir = Files.createTempDirectory("isabelle"); + try { + /* compile sources */ + + for (String s : isabelle_classpath.split(":", -1)) { + if (!s.isEmpty()) { + compiler_deps.add(Path.of(Environment.platform_path(s))); } } - _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))); - } - for (String s : sources) { _shasum.append(context.shasum(s)); } - shasum = _shasum.toString(); - } - if (fresh || !shasum_old.equals(shasum)) { - System.out.print( - "### Building " + context.description() + " (" + jar_path + ") ...\n"); - String isabelle_class_path = Environment.getenv("ISABELLE_CLASSPATH"); + List compiler_sources = new LinkedList(); + for (String s : sources) { compiler_sources.add(context.path(s)); } - Path build_dir = Files.createTempDirectory("isabelle"); - try { - /* compile sources */ - - for (String s : isabelle_class_path.split(":", -1)) { - if (!s.isEmpty()) { - compiler_deps.add(Path.of(Environment.platform_path(s))); - } - } + compile_scala_sources( + build_dir, context.scalac_options(), compiler_deps, compiler_sources); - List compiler_sources = new LinkedList(); - for (String s : sources) { compiler_sources.add(context.path(s)); } - - compile_scala_sources( - build_dir, context.scalac_options(), compiler_deps, compiler_sources); - - compiler_deps.add(build_dir); - compile_java_sources( - build_dir, context.javac_options(), compiler_deps, compiler_sources); + compiler_deps.add(build_dir); + compile_java_sources( + build_dir, context.javac_options(), compiler_deps, compiler_sources); - /* copy resources */ + /* copy resources */ - for (String s : context.resources()) { - String name = context.item_name(s); - String target = context.item_target(s); - Path file_name = Path.of(name).normalize().getFileName(); - Path target_path = Path.of(target).normalize(); + for (String s : context.resources()) { + String name = context.item_name(s); + String target = context.item_target(s); + Path file_name = Path.of(name).normalize().getFileName(); + Path target_path = Path.of(target).normalize(); - Path target_dir; - Path target_file; - { - if (target.endsWith("/") || target.endsWith("/.")) { - target_dir = build_dir.resolve(target_path); - target_file = target_dir.resolve(file_name); + Path target_dir; + Path target_file; + { + if (target.endsWith("/") || target.endsWith("/.")) { + target_dir = build_dir.resolve(target_path); + target_file = target_dir.resolve(file_name); + } + else { + target_file = build_dir.resolve(target_path); + target_dir = target_file.getParent(); + } } - else { - target_file = build_dir.resolve(target_path); - target_dir = target_file.getParent(); - } + Files.createDirectories(target_dir); + Files.copy(context.path(name), target_file, + StandardCopyOption.COPY_ATTRIBUTES); } - Files.createDirectories(target_dir); - Files.copy(context.path(name), target_file, - StandardCopyOption.COPY_ATTRIBUTES); - } - /* packaging */ + /* packaging */ - create_shasum(build_dir, shasum); - create_services(build_dir, context.services()); - create_jar(build_dir, context.main(), jar_path); - } - finally { - try (Stream walk = Files.walk(build_dir)) { - walk.sorted(Comparator.reverseOrder()) - .map(Path::toFile) - .forEach(File::delete); + create_shasum(build_dir, shasum); + create_services(build_dir, context.services()); + create_jar(build_dir, context.main(), jar_path); + } + finally { + try (Stream walk = Files.walk(build_dir)) { + walk.sorted(Comparator.reverseOrder()) + .map(Path::toFile) + .forEach(File::delete); + } } } } diff -r 77cc23b550e9 -r 0701ff55780d src/Tools/Setup/isabelle/setup/Environment.java --- a/src/Tools/Setup/isabelle/setup/Environment.java Sat Jul 17 12:59:47 2021 +0200 +++ b/src/Tools/Setup/isabelle/setup/Environment.java Sat Jul 17 13:42:21 2021 +0200 @@ -30,11 +30,6 @@ return System.getProperty("os.name", "").startsWith("Windows"); } - public static String quote(String s) - { - return "\"" + s + "\""; - } - /* system path representations */ @@ -139,7 +134,7 @@ String res = env.getOrDefault(var, ""); if (res.isEmpty()) { throw new RuntimeException( - "Bad Isabelle environment variable: " + quote(var)); + "Bad Isabelle environment variable: " + Library.quote(var)); } else check(null, res); } @@ -275,7 +270,9 @@ else { throw new RuntimeException("Unknown " + description + " directory"); } if ((new File(dir)).isDirectory()) { return dir; } - else { throw new RuntimeException("Bad " + description + " directory " + quote(dir)); } + else { + throw new RuntimeException("Bad " + description + " directory " + Library.quote(dir)); + } } private static void cygwin_exec(String isabelle_root, List cmd) diff -r 77cc23b550e9 -r 0701ff55780d src/Tools/Setup/isabelle/setup/Library.java --- a/src/Tools/Setup/isabelle/setup/Library.java Sat Jul 17 12:59:47 2021 +0200 +++ b/src/Tools/Setup/isabelle/setup/Library.java Sat Jul 17 13:42:21 2021 +0200 @@ -14,6 +14,11 @@ public class Library { + public static String quote(String s) + { + return "\"" + s + "\""; + } + public static String cat_lines(Iterable lines) { return String.join("\n", lines); diff -r 77cc23b550e9 -r 0701ff55780d src/Tools/Setup/isabelle/setup/Setup.java --- a/src/Tools/Setup/isabelle/setup/Setup.java Sat Jul 17 12:59:47 2021 +0200 +++ b/src/Tools/Setup/isabelle/setup/Setup.java Sat Jul 17 13:42:21 2021 +0200 @@ -53,7 +53,7 @@ for (String s : Build.services()) { echo(s); } break; default: - fail("Bad setup operation " + Environment.quote(op)); + fail("Bad setup operation " + Library.quote(op)); break; } } diff -r 77cc23b550e9 -r 0701ff55780d src/Tools/jEdit/jedit_base/build.props --- a/src/Tools/jEdit/jedit_base/build.props Sat Jul 17 12:59:47 2021 +0200 +++ b/src/Tools/jEdit/jedit_base/build.props Sat Jul 17 13:42:21 2021 +0200 @@ -1,6 +1,5 @@ -description = Isabelle/jEdit base plugin -lib = $JEDIT_SETTINGS/jars -name = isabelle_jedit_base +title = Isabelle/jEdit base plugin +module = $JEDIT_SETTINGS/jars/isabelle_jedit_base.jar requirements = \ env:ISABELLE_SCALA_JAR \ env:JEDIT_JARS diff -r 77cc23b550e9 -r 0701ff55780d src/Tools/jEdit/jedit_main/build.props --- a/src/Tools/jEdit/jedit_main/build.props Sat Jul 17 12:59:47 2021 +0200 +++ b/src/Tools/jEdit/jedit_main/build.props Sat Jul 17 13:42:21 2021 +0200 @@ -1,6 +1,5 @@ -description = Isabelle/jEdit main plugin -lib = $JEDIT_SETTINGS/jars -name = isabelle_jedit_main +title = Isabelle/jEdit main plugin +module = $JEDIT_SETTINGS/jars/isabelle_jedit_main.jar requirements = \ env:ISABELLE_SCALA_JAR \ env:JEDIT_JARS