--- a/Admin/lib/Tools/build_setup Sat Jul 17 21:31:15 2021 +0200
+++ b/Admin/lib/Tools/build_setup Sat Jul 17 21:40:57 2021 +0200
@@ -73,8 +73,8 @@
for SRC in "${SOURCES[@]}"
do
- ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC")"
- cp "$ISABELLE_HOME/src/Tools/Setup/isabelle/setup/$SRC" "$SOURCE_DIR"
+ ARGS["${#ARGS[@]}"]="$(platform_path "$ISABELLE_HOME/src/Tools/Setup/src/$SRC")"
+ cp "$ISABELLE_HOME/src/Tools/Setup/src/$SRC" "$SOURCE_DIR"
echo >> "$BUILD_PROPS" " \\"
echo -n >> "$BUILD_PROPS" " src/$SRC"
done
--- a/src/Tools/Setup/isabelle/setup/Build.java Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,568 +0,0 @@
-/* Title: Tools/Setup/isabelle/setup/Build.java
- Author: Makarius
-
-Build Isabelle/Scala/Java modules.
-*/
-
-package isabelle.setup;
-
-
-import java.io.BufferedOutputStream;
-import java.io.ByteArrayInputStream;
-import java.io.ByteArrayOutputStream;
-import java.io.CharArrayWriter;
-import java.io.File;
-import java.io.IOException;
-import java.io.InputStream;
-import java.io.PrintStream;
-import java.math.BigInteger;
-import java.nio.charset.StandardCharsets;
-import java.nio.file.Files;
-import java.nio.file.Path;
-import java.nio.file.StandardCopyOption;
-import java.security.MessageDigest;
-import java.security.NoSuchAlgorithmException;
-import java.util.ArrayList;
-import java.util.Comparator;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Locale;
-import java.util.Properties;
-import java.util.TreeMap;
-import java.util.jar.Attributes;
-import java.util.jar.JarEntry;
-import java.util.jar.JarFile;
-import java.util.jar.JarOutputStream;
-import java.util.jar.Manifest;
-import java.util.stream.Stream;
-
-import javax.tools.JavaCompiler;
-import javax.tools.JavaFileObject;
-import javax.tools.StandardJavaFileManager;
-import javax.tools.ToolProvider;
-
-import scala.tools.nsc.MainClass;
-
-
-public class Build
-{
- /** context **/
-
- public static String BUILD_PROPS = "build.props";
- public static String COMPONENT_BUILD_PROPS = "etc/build.props";
-
- public static Context directory_context(Path dir)
- throws IOException
- {
- Properties props = new Properties();
- 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 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<Context> component_contexts()
- throws IOException, InterruptedException
- {
- List<Context> result = new LinkedList<Context>();
- for (String p : Environment.getenv("ISABELLE_COMPONENTS").split(":", -1)) {
- if (!p.isEmpty()) {
- Path dir = Path.of(Environment.platform_path(p));
- if (Files.exists(dir.resolve(COMPONENT_BUILD_PROPS))) {
- result.add(component_context(dir));
- }
- }
- }
- 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;
- private final Properties _props;
- private final String _location;
-
- public Context(Path dir, Properties props, String location)
- {
- _dir = dir;
- _props = props;
- _location = location;
- }
-
- @Override public String toString() { return _dir.toString(); }
-
- public String error_message(String msg)
- {
- if (_location == null || _location.isEmpty()) {
- return msg;
- }
- else {
- return msg +" (in " + Library.quote(_location) + ")";
- }
- }
-
- public String title() {
- String title = _props.getProperty("title", "");
- if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); }
- else return title;
- }
-
- public String no_module() { return _props.getProperty("no_module", ""); }
- public String module() { return _props.getProperty("module", ""); }
- public String module_name() {
- if (!module().isEmpty() && !no_module().isEmpty()) {
- throw new RuntimeException(error_message("Conflict of module and no_module"));
- }
- if (!module().isEmpty()) { return module(); }
- else { return no_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<String> get_list(String name)
- {
- List<String> list = new LinkedList<String>();
- for (String s : _props.getProperty(name, "").split("\\s+")) {
- if (!s.isEmpty()) { list.add(s); }
- }
- return List.copyOf(list);
- }
- public List<String> requirements() { return get_list("requirements"); }
- public List<String> sources() { return get_list("sources"); }
- public List<String> resources() { return get_list("resources"); }
- public List<String> services() { return get_list("services"); }
-
- public boolean is_vacuous()
- {
- return sources().isEmpty() && resources().isEmpty() && services().isEmpty();
- }
-
- public Path path(String file)
- throws IOException, InterruptedException
- {
- return _dir.resolve(Environment.expand_platform_path(file));
- }
- public boolean exists(String file)
- throws IOException, InterruptedException
- {
- return Files.exists(path(file));
- }
-
- public List<Path> requirement_paths(String s)
- throws IOException, InterruptedException
- {
- if (s.startsWith("env:")) {
- List<Path> paths = new LinkedList<Path>();
- for (String p : Environment.getenv(s.substring(4)).split(":", -1)) {
- if (!p.isEmpty()) {
- Path path = Path.of(Environment.platform_path(p));
- paths.add(path);
- }
- }
- return List.copyOf(paths);
- }
- else { return List.of(path(s)); }
- }
-
- public String item_name(String s)
- {
- int i = s.indexOf(':');
- return i > 0 ? s.substring(0, i) : s;
- }
-
- public String item_target(String s)
- {
- int i = s.indexOf(':');
- return i > 0 ? s.substring(i + 1) : s;
- }
-
- public String shasum(String name, List<Path> paths)
- throws IOException, NoSuchAlgorithmException
- {
- MessageDigest sha = MessageDigest.getInstance("SHA");
- for (Path file : paths) {
- if (Files.exists(file)) {
- sha.update(Files.readAllBytes(file));
- }
- else {
- throw new RuntimeException(
- error_message("Missing input file " + Library.quote(file.toString())));
- }
- }
- return sha_digest(sha, name);
- }
-
- public String shasum(String file)
- throws IOException, NoSuchAlgorithmException, InterruptedException
- {
- return shasum(file, List.of(path(file)));
- }
-
- public String shasum_props()
- throws NoSuchAlgorithmException
- {
- TreeMap<String,Object> sorted = new TreeMap<String,Object>();
- 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, "<props>");
- }
- }
-
-
- /** compile sources **/
-
- private static void add_options(List<String> options_list, String options)
- {
- if (options != null) {
- for (String s : options.split("\\s+")) {
- if (!s.isEmpty()) { options_list.add(s); }
- }
- }
- }
-
- private static void compiler_result(boolean ok, String out, String what)
- {
- if (ok) { if (!out.isEmpty()) { System.err.println(out); } }
- else {
- String msg = "Failed to compile " + what + (out.isEmpty() ? "" : ":\n" + out);
- throw new RuntimeException(msg);
- }
- }
-
- public static void compile_scala_sources(
- Path target_dir, String more_options, List<Path> deps, List<Path> sources)
- throws IOException, InterruptedException
- {
- ArrayList<String> args = new ArrayList<String>();
- add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS"));
- add_options(args, more_options);
- args.add("-d");
- args.add(target_dir.toString());
- args.add("-bootclasspath");
- args.add(Environment.join_platform_paths(deps));
- args.add("--");
-
- boolean scala_sources = false;
- for (Path p : sources) {
- args.add(p.toString());
- if (p.toString().endsWith(".scala")) { scala_sources = true; }
- }
- if (scala_sources) {
- InputStream in_orig = System.in;
- PrintStream out_orig = System.out;
- PrintStream err_orig = System.err;
- ByteArrayInputStream in = new ByteArrayInputStream(new byte[0]);
- ByteArrayOutputStream out = new ByteArrayOutputStream();
-
- // Single-threaded context!
- boolean ok = false;
- try {
- PrintStream out_stream = new PrintStream(out);
- System.setIn(in);
- System.setOut(out_stream);
- System.setErr(out_stream);
- ok = new MainClass().process(args.toArray(String[]::new));
- out_stream.flush();
- }
- finally {
- System.setIn(in_orig);
- System.setOut(out_orig);
- System.setErr(err_orig);
- }
- compiler_result(ok, out.toString(StandardCharsets.UTF_8), "Scala sources");
- }
- }
-
- public static void compile_java_sources(
- Path target_dir, String more_options, List<Path> deps, List<Path> sources)
- throws IOException, InterruptedException
- {
- JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
- StandardJavaFileManager file_manager =
- compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8);
-
- List<String> options = new LinkedList<String>();
- add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS"));
- add_options(options, more_options);
- options.add("-d");
- options.add(target_dir.toString());
- options.add("-classpath");
- options.add(Environment.join_platform_paths(deps));
-
- List<JavaFileObject> java_sources = new LinkedList<JavaFileObject>();
- for (Path p : sources) {
- if (p.toString().endsWith(".java")) {
- for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) {
- java_sources.add(o);
- }
- }
- }
-
- if (!java_sources.isEmpty()) {
- CharArrayWriter out = new CharArrayWriter();
- boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call();
- out.flush();
- compiler_result(ok, out.toString(), "Java sources");
- }
- }
-
-
- /** shasum for jar content **/
-
- private static String SHASUM = "META-INF/isabelle/shasum";
-
- public static String get_shasum(Path jar_path)
- throws IOException
- {
- if (Files.exists(jar_path)) {
- try (JarFile jar_file = new JarFile(jar_path.toFile()))
- {
- JarEntry entry = jar_file.getJarEntry(SHASUM);
- if (entry != null) {
- byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
- return new String(bytes, StandardCharsets.UTF_8);
- }
- else { return ""; }
- }
- }
- else { return ""; }
- }
-
- public static void create_shasum(Path dir, String shasum)
- throws IOException
- {
- Path path = dir.resolve(SHASUM);
- Files.createDirectories(path.getParent());
- Files.writeString(path, shasum);
- }
-
-
- /** services **/
-
- private static String SERVICES = "META-INF/isabelle/services";
-
- public static List<String> get_services(Path jar_path)
- throws IOException
- {
- if (Files.exists(jar_path)) {
- try (JarFile jar_file = new JarFile(jar_path.toFile()))
- {
- JarEntry entry = jar_file.getJarEntry(SERVICES);
- if (entry != null) {
- byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
- return Library.split_lines(new String(bytes, StandardCharsets.UTF_8));
- }
- else { return List.of(); }
- }
- }
- else { return List.of(); }
- }
-
- public static void create_services(Path dir, List<String> services)
- throws IOException
- {
- if (!services.isEmpty()) {
- Path path = dir.resolve(SERVICES);
- Files.createDirectories(path.getParent());
- Files.writeString(path, Library.cat_lines(services));
- }
- }
-
-
- /** create jar **/
-
- public static void create_jar(Path dir, String main, Path jar)
- throws IOException
- {
- Files.createDirectories(dir.resolve(jar).getParent());
- Files.deleteIfExists(jar);
-
- Manifest manifest = new Manifest();
- Attributes attributes = manifest.getMainAttributes();
- attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0");
- attributes.put(new Attributes.Name("Created-By"),
- System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")");
- if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); }
-
- try (JarOutputStream out =
- new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest))
- {
- for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) {
- boolean is_dir = Files.isDirectory(path);
- boolean is_file = Files.isRegularFile(path);
- if (is_dir || is_file) {
- String name = Environment.slashes(dir.relativize(path).toString());
- if (!name.isEmpty()) {
- JarEntry entry = new JarEntry(is_dir ? name + "/" : name);
- entry.setTime(path.toFile().lastModified());
- out.putNextEntry(entry);
- if (is_file) { out.write(Files.readAllBytes(path)); }
- out.closeEntry();
- }
- }
- }
- }
- }
-
-
- /** classpath **/
-
- public static List<Path> classpath()
- throws IOException, InterruptedException
- {
- List<Path> result = new LinkedList<Path>();
- for (Context context : component_contexts()) {
- String module = context.module();
- if (!module.isEmpty()) { result.add(context.path(module)); }
- }
- return List.copyOf(result);
- }
-
- public static List<String> services()
- throws IOException, InterruptedException
- {
- List<String> result = new LinkedList<String>();
- for (Context context : component_contexts()) {
- for (String s : context.services()) {
- result.add(s);
- }
- }
- return List.copyOf(result);
- }
-
-
- /** build **/
-
- public static void build(Context context, boolean fresh)
- throws IOException, InterruptedException, NoSuchAlgorithmException
- {
- String module = context.module();
- if (!module.isEmpty()) {
- String title = context.title();
-
- 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<String> requirements = context.requirements();
- List<String> resources = context.resources();
- List<String> sources = context.sources();
-
- String shasum_old = get_shasum(jar_path);
- String shasum;
- List<Path> compiler_deps = new LinkedList<Path>();
- {
- StringBuilder _shasum = new StringBuilder();
- _shasum.append(context.shasum_props());
- for (String s : requirements) {
- List<Path> paths = context.requirement_paths(s);
- compiler_deps.addAll(paths);
- _shasum.append(context.shasum(s, paths));
- }
- 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)));
- }
- }
-
- List<Path> compiler_sources = new LinkedList<Path>();
- 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);
-
-
- /* 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();
-
- 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();
- }
- }
- Files.createDirectories(target_dir);
- Files.copy(context.path(name), target_file,
- StandardCopyOption.COPY_ATTRIBUTES);
- }
-
-
- /* packaging */
-
- create_shasum(build_dir, shasum);
- create_services(build_dir, context.services());
- create_jar(build_dir, context.main(), jar_path);
- }
- finally {
- try (Stream<Path> walk = Files.walk(build_dir)) {
- walk.sorted(Comparator.reverseOrder())
- .map(Path::toFile)
- .forEach(File::delete);
- }
- }
- }
- }
- }
- }
-
- public static void build_components(boolean fresh)
- throws IOException, InterruptedException, NoSuchAlgorithmException
- {
- for (Context context : component_contexts()) {
- build(context, fresh);
- }
- }
-}
--- a/src/Tools/Setup/isabelle/setup/Environment.java Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,453 +0,0 @@
-/* Title: Tools/Setup/isabelle/setup/Environment.scala
- Author: Makarius
-
-Fundamental Isabelle system environment: quasi-static module with
-optional init operation.
-*/
-
-package isabelle.setup;
-
-import java.io.File;
-import java.io.IOException;
-import java.nio.file.Files;
-import java.nio.file.Path;
-import java.util.HashMap;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Locale;
-import java.util.Map;
-import java.util.function.BiFunction;
-import java.util.regex.Matcher;
-import java.util.regex.Pattern;
-
-
-public class Environment
-{
- /** Support for Cygwin as POSIX emulation on Windows **/
-
- public static Boolean is_windows()
- {
- return System.getProperty("os.name", "").startsWith("Windows");
- }
-
-
-
- /* system path representations */
-
- public static String slashes(String s) { return s.replace('\\', '/'); }
-
- public static String standard_path(String cygwin_root, String platform_path)
- {
- if (is_windows()) {
- String backslashes = platform_path.replace('/', '\\');
-
- Pattern root_pattern =
- Pattern.compile("(?i)" + Pattern.quote(cygwin_root) + "(?:\\\\+|\\z)(.*)");
- Matcher root_matcher = root_pattern.matcher(backslashes);
-
- Pattern drive_pattern = Pattern.compile("([a-zA-Z]):\\\\*(.*)");
- Matcher drive_matcher = drive_pattern.matcher(backslashes);
-
- if (root_matcher.matches()) {
- String rest = root_matcher.group(1);
- return "/" + slashes(rest);
- }
- else if (drive_matcher.matches()) {
- String letter = drive_matcher.group(1).toLowerCase(Locale.ROOT);
- String rest = drive_matcher.group(2);
- return "/cygdrive/" + letter + (rest.isEmpty() ? "" : "/" + slashes(rest));
- }
- else { return slashes(backslashes); }
- }
- else { return platform_path; }
- }
-
- private static class Expand_Platform_Path
- {
- private String _cygwin_root;
- private StringBuilder _result = new StringBuilder();
-
- public Expand_Platform_Path(String cygwin_root)
- {
- _cygwin_root = cygwin_root;
- }
-
- public String result() { return _result.toString(); }
-
- void clear() { _result.setLength(0); }
- void add(char c) { _result.append(c); }
- void add(String s) { _result.append(s); }
- void separator()
- {
- int n = _result.length();
- if (n > 0 && _result.charAt(n - 1) != File.separatorChar) {
- add(File.separatorChar);
- }
- }
-
- public String check_root(String standard_path)
- {
- String rest = standard_path;
- boolean is_root = standard_path.startsWith("/");
-
- if (is_windows()) {
- Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)");
- Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path);
-
- Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)");
- Matcher named_root_matcher = named_root_pattern.matcher(standard_path);
-
- if (cygdrive_matcher.matches()) {
- String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT);
- rest = cygdrive_matcher.group(2);
- clear();
- add(drive);
- add(':');
- add(File.separatorChar);
- }
- else if (named_root_matcher.matches()) {
- String root = named_root_matcher.group(1);
- rest = named_root_matcher.group(2);
- clear();
- add(File.separatorChar);
- add(File.separatorChar);
- add(root);
- }
- else if (is_root) {
- clear();
- add(_cygwin_root);
- }
- }
- else if (is_root) {
- clear();
- add(File.separatorChar);
- }
- return rest;
- }
-
- public void check_rest(Map<String,String> env, String main)
- throws IOException, InterruptedException
- {
- for (String p : main.split("/", -1)) {
- if (env != null && p.startsWith("$")) {
- String var = p.substring(1);
- String res = env.getOrDefault(var, "");
- if (res.isEmpty()) {
- throw new RuntimeException(
- "Bad Isabelle environment variable: " + Library.quote(var));
- }
- else check(null, res);
- }
- else if (!p.isEmpty()) {
- separator();
- add(p);
- }
- }
- }
-
- public void check(Map<String,String> env, String path)
- throws IOException, InterruptedException
- {
- check_rest(env, check_root(path));
- }
- }
-
- public static String expand_platform_path(
- Map<String,String> env, String cygwin_root, String standard_path)
- throws IOException, InterruptedException
- {
- Expand_Platform_Path expand = new Expand_Platform_Path(cygwin_root);
- expand.check(env, standard_path);
- return expand.result();
- }
-
- public static String join_platform_paths(List<Path> paths)
- {
- List<String> strs = new LinkedList<String>();
- for (Path p : paths) { strs.add(p.toString()); }
- return String.join(File.pathSeparator, strs);
- }
-
- public static String join_standard_paths(List<Path> paths)
- throws IOException, InterruptedException
- {
- List<String> strs = new LinkedList<String>();
- for (Path p : paths) { strs.add(standard_path(p.toString())); }
- return String.join(":", strs);
- }
-
-
- /* raw process */
-
- public static ProcessBuilder process_builder(
- List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
- {
- ProcessBuilder builder = new ProcessBuilder();
-
- // fragile on Windows:
- // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
- builder.command(cmd);
-
- if (cwd != null) builder.directory(cwd);
- if (env != null) {
- builder.environment().clear();
- builder.environment().putAll(env);
- }
- builder.redirectErrorStream(redirect);
-
- return builder;
- }
-
- public static class Exec_Result
- {
- private final int _rc;
- private final String _out;
- private final String _err;
-
- Exec_Result(int rc, String out, String err)
- {
- _rc = rc;
- _out = Library.trim_line(out);
- _err = Library.trim_line(err);
- }
-
- public int rc() { return _rc; }
- public boolean ok() { return _rc == 0; }
- public String out() { return _out; }
- public String err() { return _err; }
- }
-
- public static Exec_Result exec_process(
- List<String> command_line,
- File cwd,
- Map<String,String> env,
- boolean redirect) throws IOException, InterruptedException
- {
- Path out_file = Files.createTempFile(null, null);
- Path err_file = Files.createTempFile(null, null);
- Exec_Result res;
- try {
- ProcessBuilder builder = process_builder(command_line, cwd, env, redirect);
- builder.redirectOutput(out_file.toFile());
- builder.redirectError(err_file.toFile());
-
- Process proc = builder.start();
- proc.getOutputStream().close();
- try { proc.waitFor(); }
- finally {
- proc.getInputStream().close();
- proc.getErrorStream().close();
- proc.destroy();
- Thread.interrupted();
- }
-
- int rc = proc.exitValue();
- String out = Files.readString(out_file);
- String err = Files.readString(err_file);
- res = new Exec_Result(rc, out, err);
- }
- finally {
- Files.deleteIfExists(out_file);
- Files.deleteIfExists(err_file);
- }
- return res;
- }
-
-
- /* init (e.g. after extraction via 7zip) */
-
- private static String bootstrap_directory(
- String preference, String variable, String property, String description)
- {
- String a = preference; // explicit argument
- String b = System.getenv(variable); // e.g. inherited from running isabelle tool
- String c = System.getProperty(property); // e.g. via JVM application boot process
- String dir;
-
- if (a != null && !a.isEmpty()) { dir = a; }
- else if (b != null && !b.isEmpty()) { dir = b; }
- else if (c != null && !c.isEmpty()) { dir = c; }
- else { throw new RuntimeException("Unknown " + description + " directory"); }
-
- if ((new File(dir)).isDirectory()) { return dir; }
- else {
- throw new RuntimeException("Bad " + description + " directory " + Library.quote(dir));
- }
- }
-
- private static void cygwin_exec(String isabelle_root, List<String> cmd)
- throws IOException, InterruptedException
- {
- File cwd = new File(isabelle_root);
- Map<String,String> env = new HashMap<String,String>(System.getenv());
- env.put("CYGWIN", "nodosfilewarning");
- Exec_Result res = exec_process(cmd, cwd, env, true);
- if (!res.ok()) throw new RuntimeException(res.out());
- }
-
- public static void cygwin_link(String content, File target) throws IOException
- {
- Path target_path = target.toPath();
- Files.writeString(target_path, "!<symlink>" + content + "\u0000");
- Files.setAttribute(target_path, "dos:system", true);
- }
-
- public static void cygwin_init(String isabelle_root, String cygwin_root)
- throws IOException, InterruptedException
- {
- if (is_windows()) {
- File uninitialized_file = new File(cygwin_root, "isabelle\\uninitialized");
- boolean uninitialized = uninitialized_file.isFile() && uninitialized_file.delete();
-
- if (uninitialized) {
- Path symlinks_path = (new File(cygwin_root + "\\isabelle\\symlinks")).toPath();
- String[] symlinks = Files.readAllLines(symlinks_path).toArray(new String[0]);
-
- // recover symlinks
- int i = 0;
- int m = symlinks.length;
- int n = (m > 0 && symlinks[m - 1].isEmpty()) ? m - 1 : m;
- while (i < n) {
- if (i + 1 < n) {
- String target = symlinks[i];
- String content = symlinks[i + 1];
- cygwin_link(content, new File(isabelle_root, target));
- i += 2;
- } else { throw new RuntimeException("Unbalanced symlinks list"); }
- }
-
- cygwin_exec(isabelle_root,
- List.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"));
- cygwin_exec(isabelle_root,
- List.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"));
- }
- }
- }
-
-
- /* implicit settings environment */
-
- private static volatile Map<String,String> _settings = null;
-
- public static Map<String,String> settings()
- throws IOException, InterruptedException
- {
- if (_settings == null) { init("", ""); } // unsynchronized check
- return _settings;
- }
-
- public static String getenv(String name)
- throws IOException, InterruptedException
- {
- return settings().getOrDefault(name, "");
- }
-
- public static synchronized void init(String _isabelle_root, String _cygwin_root)
- throws IOException, InterruptedException
- {
- if (_settings == null) {
- String isabelle_root =
- bootstrap_directory(_isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root");
-
- String cygwin_root = "";
- if (is_windows()) {
- cygwin_root = bootstrap_directory(_cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root");
- cygwin_init(isabelle_root, cygwin_root);
- }
-
- Map<String,String> env = new HashMap<String,String>(System.getenv());
-
- BiFunction<String,String,Void> env_default =
- (String a, String b) -> { if (!b.isEmpty()) env.putIfAbsent(a, b); return null; };
-
- String temp_windows = is_windows() ? System.getenv("TEMP") : null;
-
- env_default.apply("CYGWIN_ROOT", cygwin_root);
- env_default.apply("TEMP_WINDOWS",
- (temp_windows != null && temp_windows.contains("\\")) ? temp_windows : "");
- env_default.apply("ISABELLE_JDK_HOME",
- standard_path(cygwin_root, System.getProperty("java.home", "")));
- env_default.apply("HOME", System.getProperty("user.home", ""));
- env_default.apply("ISABELLE_APP", System.getProperty("isabelle.app", ""));
-
- Map<String,String> settings = new HashMap<String,String>();
- Path settings_file = Files.createTempFile(null, null);
- try {
- List<String> cmd = new LinkedList<String>();
- if (is_windows()) {
- cmd.add(cygwin_root + "\\bin\\bash");
- cmd.add("-l");
- cmd.add(standard_path(cygwin_root, isabelle_root + "\\bin\\isabelle"));
- } else {
- cmd.add(isabelle_root + "/bin/isabelle");
- }
- cmd.add("getenv");
- cmd.add("-d");
- cmd.add(settings_file.toString());
-
- Exec_Result res = exec_process(cmd, null, env, true);
- if (!res.ok()) throw new RuntimeException(res.out());
-
- for (String s : Files.readString(settings_file).split("\u0000", -1)) {
- int i = s.indexOf('=');
- if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
- else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
- }
- }
- finally { Files.delete(settings_file); }
-
- if (is_windows()) { settings.put("CYGWIN_ROOT", cygwin_root); }
-
- settings.put("PATH", settings.get("PATH_JVM"));
- settings.remove("PATH_JVM");
-
- _settings = Map.copyOf(settings);
- }
- }
-
-
- /* Cygwin root (after init) */
-
- public static String cygwin_root()
- throws IOException, InterruptedException
- {
- return getenv("CYGWIN_ROOT");
- }
-
- public static String standard_path(String platform_path)
- throws IOException, InterruptedException
- {
- return standard_path(cygwin_root(), platform_path);
- }
-
- public static String expand_platform_path(String standard_path)
- throws IOException, InterruptedException
- {
- return expand_platform_path(settings(), cygwin_root(), standard_path);
- }
-
- public static String platform_path(String standard_path)
- throws IOException, InterruptedException
- {
- return expand_platform_path(null, cygwin_root(), standard_path);
- }
-
-
- /* kill process (via bash) */
-
- static public boolean kill_process(String group_pid, String signal)
- throws IOException, InterruptedException
- {
- List<String> cmd = new LinkedList<String>();
- if (is_windows()) {
- cmd.add(cygwin_root() + "\\bin\\bash.exe");
- }
- else {
- cmd.add("/usr/bin/env");
- cmd.add("bash");
- }
- cmd.add("-c");
- cmd.add("kill -" + signal + " -" + group_pid);
- return exec_process(cmd, null, null, false).ok();
- }
-}
--- a/src/Tools/Setup/isabelle/setup/Exn.java Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-/* Title: Tools/Setup/isabelle/setup/Exn.java
- Author: Makarius
-
-Support for exceptions (arbitrary throwables).
-*/
-
-package isabelle.setup;
-
-
-import java.io.IOException;
-import java.util.LinkedList;
-import java.util.List;
-
-
-public class Exn
-{
- /* interrupts */
-
- public static boolean is_interrupt(Throwable exn)
- {
- boolean found_interrupt = false;
- Throwable e = exn;
- while (!found_interrupt && e != null) {
- found_interrupt = e instanceof InterruptedException;
- e = e.getCause();
- }
- return found_interrupt;
- }
-
- public static int INTERRUPT_RETURN_CODE = 130;
-
- public static int return_code(Throwable exn, int rc)
- {
- return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc;
- }
-
-
- /* message */
-
- public static String message(Throwable exn)
- {
- String msg = exn.getMessage();
-
- if (exn.getClass() == RuntimeException.class)
- {
- return msg == null || msg.isEmpty() ? "Error" : msg;
- }
- else if (exn instanceof IOException)
- {
- return msg == null || msg.isEmpty() ? "I/O error" : "I/O error: " + msg;
- }
- else if (exn instanceof RuntimeException && !msg.isEmpty()) { return msg; }
- else if (exn instanceof InterruptedException) { return "Interrupt"; }
- else { return exn.toString(); }
- }
-
-
- /* print */
-
- public static String trace(Throwable exn)
- {
- List<String> list = new LinkedList<String>();
- for (StackTraceElement elem : exn.getStackTrace()) {
- list.add(elem.toString());
- }
- return Library.cat_lines(list);
- }
-
- public static boolean debug()
- {
- return System.getProperty("isabelle.debug", "").equals("true");
- }
-
- public static String print(Throwable exn)
- {
- return debug() ? message(exn) + "\n" + trace(exn) : message(exn);
- }
-
- public static String print_error(Throwable exn)
- {
- return Library.prefix_lines("*** ", print(exn));
- }
-}
--- a/src/Tools/Setup/isabelle/setup/Library.java Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-/* Title: Tools/Setup/isabelle/setup/Library.java
- Author: Makarius
-
-Basic library.
-*/
-
-package isabelle.setup;
-
-
-import java.util.Arrays;
-import java.util.LinkedList;
-import java.util.List;
-
-
-public class Library
-{
- public static String quote(String s)
- {
- return "\"" + s + "\"";
- }
-
- public static String cat_lines(Iterable<? extends CharSequence> lines)
- {
- return String.join("\n", lines);
- }
-
- public static List<String> split_lines(String str)
- {
- if (str.isEmpty()) { return List.of(); }
- else {
- List<String> result = new LinkedList<String>();
- result.addAll(Arrays.asList(str.split("\\n")));
- return List.copyOf(result);
- }
- }
-
- public static String prefix_lines(String prfx, String str)
- {
- if (str.isEmpty()) { return str; }
- else {
- List<String> lines = new LinkedList<String>();
- for (String line : split_lines(str)) { lines.add(prfx + line); }
- return cat_lines(lines);
- }
- }
-
- public static String trim_line(String s)
- {
- if (s.endsWith("\r\n")) { return s.substring(0, s.length() - 2); }
- else if (s.endsWith("\r") || s.endsWith("\n")) { return s.substring(0, s.length() - 1); }
- else { return s; }
- }
-}
\ No newline at end of file
--- a/src/Tools/Setup/isabelle/setup/Setup.java Sat Jul 17 21:31:15 2021 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-/* Title: Tools/Setup/isabelle/setup/Setup.java
- Author: Makarius
-
-Isabelle setup tool: bootstrap from generic Java environment.
-*/
-
-package isabelle.setup;
-
-
-class Setup
-{
- private static void echo(String msg)
- {
- System.out.print(msg + "\n");
- }
- private static void echo_err(String msg)
- {
- System.err.print(msg + "\n");
- }
- private static void fail(String msg)
- {
- echo_err(msg);
- System.exit(2);
- }
-
- private static void check_args(boolean b)
- {
- if (!b) { fail("Bad command-line arguments"); }
- }
-
- public static void main(String[] args)
- {
- int n = args.length;
- check_args(n > 0);
-
- String op = args[0];
- try {
- switch (op) {
- case "build":
- check_args(n == 1);
- Build.build_components(false);
- break;
- case "build_fresh":
- check_args(n == 1);
- Build.build_components(true);
- break;
- case "classpath":
- check_args(n == 1);
- echo(Environment.join_standard_paths(Build.classpath()));
- break;
- case "services":
- check_args(n == 1);
- for (String s : Build.services()) { echo(s); }
- break;
- default:
- fail("Bad setup operation " + Library.quote(op));
- break;
- }
- }
- catch (Throwable exn) {
- echo_err(Exn.print_error(exn));
- System.exit(Exn.return_code(exn, 2));
- }
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Build.java Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,568 @@
+/* Title: Tools/Setup/src/Build.java
+ Author: Makarius
+
+Build Isabelle/Scala/Java modules.
+*/
+
+package isabelle.setup;
+
+
+import java.io.BufferedOutputStream;
+import java.io.ByteArrayInputStream;
+import java.io.ByteArrayOutputStream;
+import java.io.CharArrayWriter;
+import java.io.File;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.PrintStream;
+import java.math.BigInteger;
+import java.nio.charset.StandardCharsets;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.StandardCopyOption;
+import java.security.MessageDigest;
+import java.security.NoSuchAlgorithmException;
+import java.util.ArrayList;
+import java.util.Comparator;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Locale;
+import java.util.Properties;
+import java.util.TreeMap;
+import java.util.jar.Attributes;
+import java.util.jar.JarEntry;
+import java.util.jar.JarFile;
+import java.util.jar.JarOutputStream;
+import java.util.jar.Manifest;
+import java.util.stream.Stream;
+
+import javax.tools.JavaCompiler;
+import javax.tools.JavaFileObject;
+import javax.tools.StandardJavaFileManager;
+import javax.tools.ToolProvider;
+
+import scala.tools.nsc.MainClass;
+
+
+public class Build
+{
+ /** context **/
+
+ public static String BUILD_PROPS = "build.props";
+ public static String COMPONENT_BUILD_PROPS = "etc/build.props";
+
+ public static Context directory_context(Path dir)
+ throws IOException
+ {
+ Properties props = new Properties();
+ 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 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<Context> component_contexts()
+ throws IOException, InterruptedException
+ {
+ List<Context> result = new LinkedList<Context>();
+ for (String p : Environment.getenv("ISABELLE_COMPONENTS").split(":", -1)) {
+ if (!p.isEmpty()) {
+ Path dir = Path.of(Environment.platform_path(p));
+ if (Files.exists(dir.resolve(COMPONENT_BUILD_PROPS))) {
+ result.add(component_context(dir));
+ }
+ }
+ }
+ 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;
+ private final Properties _props;
+ private final String _location;
+
+ public Context(Path dir, Properties props, String location)
+ {
+ _dir = dir;
+ _props = props;
+ _location = location;
+ }
+
+ @Override public String toString() { return _dir.toString(); }
+
+ public String error_message(String msg)
+ {
+ if (_location == null || _location.isEmpty()) {
+ return msg;
+ }
+ else {
+ return msg +" (in " + Library.quote(_location) + ")";
+ }
+ }
+
+ public String title() {
+ String title = _props.getProperty("title", "");
+ if (title.isEmpty()) { throw new RuntimeException(error_message("Missing title")); }
+ else return title;
+ }
+
+ public String no_module() { return _props.getProperty("no_module", ""); }
+ public String module() { return _props.getProperty("module", ""); }
+ public String module_name() {
+ if (!module().isEmpty() && !no_module().isEmpty()) {
+ throw new RuntimeException(error_message("Conflict of module and no_module"));
+ }
+ if (!module().isEmpty()) { return module(); }
+ else { return no_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<String> get_list(String name)
+ {
+ List<String> list = new LinkedList<String>();
+ for (String s : _props.getProperty(name, "").split("\\s+")) {
+ if (!s.isEmpty()) { list.add(s); }
+ }
+ return List.copyOf(list);
+ }
+ public List<String> requirements() { return get_list("requirements"); }
+ public List<String> sources() { return get_list("sources"); }
+ public List<String> resources() { return get_list("resources"); }
+ public List<String> services() { return get_list("services"); }
+
+ public boolean is_vacuous()
+ {
+ return sources().isEmpty() && resources().isEmpty() && services().isEmpty();
+ }
+
+ public Path path(String file)
+ throws IOException, InterruptedException
+ {
+ return _dir.resolve(Environment.expand_platform_path(file));
+ }
+ public boolean exists(String file)
+ throws IOException, InterruptedException
+ {
+ return Files.exists(path(file));
+ }
+
+ public List<Path> requirement_paths(String s)
+ throws IOException, InterruptedException
+ {
+ if (s.startsWith("env:")) {
+ List<Path> paths = new LinkedList<Path>();
+ for (String p : Environment.getenv(s.substring(4)).split(":", -1)) {
+ if (!p.isEmpty()) {
+ Path path = Path.of(Environment.platform_path(p));
+ paths.add(path);
+ }
+ }
+ return List.copyOf(paths);
+ }
+ else { return List.of(path(s)); }
+ }
+
+ public String item_name(String s)
+ {
+ int i = s.indexOf(':');
+ return i > 0 ? s.substring(0, i) : s;
+ }
+
+ public String item_target(String s)
+ {
+ int i = s.indexOf(':');
+ return i > 0 ? s.substring(i + 1) : s;
+ }
+
+ public String shasum(String name, List<Path> paths)
+ throws IOException, NoSuchAlgorithmException
+ {
+ MessageDigest sha = MessageDigest.getInstance("SHA");
+ for (Path file : paths) {
+ if (Files.exists(file)) {
+ sha.update(Files.readAllBytes(file));
+ }
+ else {
+ throw new RuntimeException(
+ error_message("Missing input file " + Library.quote(file.toString())));
+ }
+ }
+ return sha_digest(sha, name);
+ }
+
+ public String shasum(String file)
+ throws IOException, NoSuchAlgorithmException, InterruptedException
+ {
+ return shasum(file, List.of(path(file)));
+ }
+
+ public String shasum_props()
+ throws NoSuchAlgorithmException
+ {
+ TreeMap<String,Object> sorted = new TreeMap<String,Object>();
+ 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, "<props>");
+ }
+ }
+
+
+ /** compile sources **/
+
+ private static void add_options(List<String> options_list, String options)
+ {
+ if (options != null) {
+ for (String s : options.split("\\s+")) {
+ if (!s.isEmpty()) { options_list.add(s); }
+ }
+ }
+ }
+
+ private static void compiler_result(boolean ok, String out, String what)
+ {
+ if (ok) { if (!out.isEmpty()) { System.err.println(out); } }
+ else {
+ String msg = "Failed to compile " + what + (out.isEmpty() ? "" : ":\n" + out);
+ throw new RuntimeException(msg);
+ }
+ }
+
+ public static void compile_scala_sources(
+ Path target_dir, String more_options, List<Path> deps, List<Path> sources)
+ throws IOException, InterruptedException
+ {
+ ArrayList<String> args = new ArrayList<String>();
+ add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS"));
+ add_options(args, more_options);
+ args.add("-d");
+ args.add(target_dir.toString());
+ args.add("-bootclasspath");
+ args.add(Environment.join_platform_paths(deps));
+ args.add("--");
+
+ boolean scala_sources = false;
+ for (Path p : sources) {
+ args.add(p.toString());
+ if (p.toString().endsWith(".scala")) { scala_sources = true; }
+ }
+ if (scala_sources) {
+ InputStream in_orig = System.in;
+ PrintStream out_orig = System.out;
+ PrintStream err_orig = System.err;
+ ByteArrayInputStream in = new ByteArrayInputStream(new byte[0]);
+ ByteArrayOutputStream out = new ByteArrayOutputStream();
+
+ // Single-threaded context!
+ boolean ok = false;
+ try {
+ PrintStream out_stream = new PrintStream(out);
+ System.setIn(in);
+ System.setOut(out_stream);
+ System.setErr(out_stream);
+ ok = new MainClass().process(args.toArray(String[]::new));
+ out_stream.flush();
+ }
+ finally {
+ System.setIn(in_orig);
+ System.setOut(out_orig);
+ System.setErr(err_orig);
+ }
+ compiler_result(ok, out.toString(StandardCharsets.UTF_8), "Scala sources");
+ }
+ }
+
+ public static void compile_java_sources(
+ Path target_dir, String more_options, List<Path> deps, List<Path> sources)
+ throws IOException, InterruptedException
+ {
+ JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
+ StandardJavaFileManager file_manager =
+ compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8);
+
+ List<String> options = new LinkedList<String>();
+ add_options(options, Environment.getenv("ISABELLE_JAVAC_OPTIONS"));
+ add_options(options, more_options);
+ options.add("-d");
+ options.add(target_dir.toString());
+ options.add("-classpath");
+ options.add(Environment.join_platform_paths(deps));
+
+ List<JavaFileObject> java_sources = new LinkedList<JavaFileObject>();
+ for (Path p : sources) {
+ if (p.toString().endsWith(".java")) {
+ for (JavaFileObject o : file_manager.getJavaFileObjectsFromPaths(List.of(p))) {
+ java_sources.add(o);
+ }
+ }
+ }
+
+ if (!java_sources.isEmpty()) {
+ CharArrayWriter out = new CharArrayWriter();
+ boolean ok = compiler.getTask(out, file_manager, null, options, null, java_sources).call();
+ out.flush();
+ compiler_result(ok, out.toString(), "Java sources");
+ }
+ }
+
+
+ /** shasum for jar content **/
+
+ private static String SHASUM = "META-INF/isabelle/shasum";
+
+ public static String get_shasum(Path jar_path)
+ throws IOException
+ {
+ if (Files.exists(jar_path)) {
+ try (JarFile jar_file = new JarFile(jar_path.toFile()))
+ {
+ JarEntry entry = jar_file.getJarEntry(SHASUM);
+ if (entry != null) {
+ byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
+ return new String(bytes, StandardCharsets.UTF_8);
+ }
+ else { return ""; }
+ }
+ }
+ else { return ""; }
+ }
+
+ public static void create_shasum(Path dir, String shasum)
+ throws IOException
+ {
+ Path path = dir.resolve(SHASUM);
+ Files.createDirectories(path.getParent());
+ Files.writeString(path, shasum);
+ }
+
+
+ /** services **/
+
+ private static String SERVICES = "META-INF/isabelle/services";
+
+ public static List<String> get_services(Path jar_path)
+ throws IOException
+ {
+ if (Files.exists(jar_path)) {
+ try (JarFile jar_file = new JarFile(jar_path.toFile()))
+ {
+ JarEntry entry = jar_file.getJarEntry(SERVICES);
+ if (entry != null) {
+ byte[] bytes = jar_file.getInputStream(entry).readAllBytes();
+ return Library.split_lines(new String(bytes, StandardCharsets.UTF_8));
+ }
+ else { return List.of(); }
+ }
+ }
+ else { return List.of(); }
+ }
+
+ public static void create_services(Path dir, List<String> services)
+ throws IOException
+ {
+ if (!services.isEmpty()) {
+ Path path = dir.resolve(SERVICES);
+ Files.createDirectories(path.getParent());
+ Files.writeString(path, Library.cat_lines(services));
+ }
+ }
+
+
+ /** create jar **/
+
+ public static void create_jar(Path dir, String main, Path jar)
+ throws IOException
+ {
+ Files.createDirectories(dir.resolve(jar).getParent());
+ Files.deleteIfExists(jar);
+
+ Manifest manifest = new Manifest();
+ Attributes attributes = manifest.getMainAttributes();
+ attributes.put(Attributes.Name.MANIFEST_VERSION, "1.0");
+ attributes.put(new Attributes.Name("Created-By"),
+ System.getProperty("java.version") + " (" + System.getProperty("java.vendor") + ")");
+ if (!main.isEmpty()) { attributes.put(Attributes.Name.MAIN_CLASS, main); }
+
+ try (JarOutputStream out =
+ new JarOutputStream(new BufferedOutputStream(Files.newOutputStream(jar)), manifest))
+ {
+ for (Path path : Files.walk(dir).sorted().toArray(Path[]::new)) {
+ boolean is_dir = Files.isDirectory(path);
+ boolean is_file = Files.isRegularFile(path);
+ if (is_dir || is_file) {
+ String name = Environment.slashes(dir.relativize(path).toString());
+ if (!name.isEmpty()) {
+ JarEntry entry = new JarEntry(is_dir ? name + "/" : name);
+ entry.setTime(path.toFile().lastModified());
+ out.putNextEntry(entry);
+ if (is_file) { out.write(Files.readAllBytes(path)); }
+ out.closeEntry();
+ }
+ }
+ }
+ }
+ }
+
+
+ /** classpath **/
+
+ public static List<Path> classpath()
+ throws IOException, InterruptedException
+ {
+ List<Path> result = new LinkedList<Path>();
+ for (Context context : component_contexts()) {
+ String module = context.module();
+ if (!module.isEmpty()) { result.add(context.path(module)); }
+ }
+ return List.copyOf(result);
+ }
+
+ public static List<String> services()
+ throws IOException, InterruptedException
+ {
+ List<String> result = new LinkedList<String>();
+ for (Context context : component_contexts()) {
+ for (String s : context.services()) {
+ result.add(s);
+ }
+ }
+ return List.copyOf(result);
+ }
+
+
+ /** build **/
+
+ public static void build(Context context, boolean fresh)
+ throws IOException, InterruptedException, NoSuchAlgorithmException
+ {
+ String module = context.module();
+ if (!module.isEmpty()) {
+ String title = context.title();
+
+ 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<String> requirements = context.requirements();
+ List<String> resources = context.resources();
+ List<String> sources = context.sources();
+
+ String shasum_old = get_shasum(jar_path);
+ String shasum;
+ List<Path> compiler_deps = new LinkedList<Path>();
+ {
+ StringBuilder _shasum = new StringBuilder();
+ _shasum.append(context.shasum_props());
+ for (String s : requirements) {
+ List<Path> paths = context.requirement_paths(s);
+ compiler_deps.addAll(paths);
+ _shasum.append(context.shasum(s, paths));
+ }
+ 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)));
+ }
+ }
+
+ List<Path> compiler_sources = new LinkedList<Path>();
+ 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);
+
+
+ /* 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();
+
+ 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();
+ }
+ }
+ Files.createDirectories(target_dir);
+ Files.copy(context.path(name), target_file,
+ StandardCopyOption.COPY_ATTRIBUTES);
+ }
+
+
+ /* packaging */
+
+ create_shasum(build_dir, shasum);
+ create_services(build_dir, context.services());
+ create_jar(build_dir, context.main(), jar_path);
+ }
+ finally {
+ try (Stream<Path> walk = Files.walk(build_dir)) {
+ walk.sorted(Comparator.reverseOrder())
+ .map(Path::toFile)
+ .forEach(File::delete);
+ }
+ }
+ }
+ }
+ }
+ }
+
+ public static void build_components(boolean fresh)
+ throws IOException, InterruptedException, NoSuchAlgorithmException
+ {
+ for (Context context : component_contexts()) {
+ build(context, fresh);
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Environment.java Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,453 @@
+/* Title: Tools/Setup/src/Environment.scala
+ Author: Makarius
+
+Fundamental Isabelle system environment: quasi-static module with
+optional init operation.
+*/
+
+package isabelle.setup;
+
+import java.io.File;
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.util.HashMap;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Locale;
+import java.util.Map;
+import java.util.function.BiFunction;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+
+public class Environment
+{
+ /** Support for Cygwin as POSIX emulation on Windows **/
+
+ public static Boolean is_windows()
+ {
+ return System.getProperty("os.name", "").startsWith("Windows");
+ }
+
+
+
+ /* system path representations */
+
+ public static String slashes(String s) { return s.replace('\\', '/'); }
+
+ public static String standard_path(String cygwin_root, String platform_path)
+ {
+ if (is_windows()) {
+ String backslashes = platform_path.replace('/', '\\');
+
+ Pattern root_pattern =
+ Pattern.compile("(?i)" + Pattern.quote(cygwin_root) + "(?:\\\\+|\\z)(.*)");
+ Matcher root_matcher = root_pattern.matcher(backslashes);
+
+ Pattern drive_pattern = Pattern.compile("([a-zA-Z]):\\\\*(.*)");
+ Matcher drive_matcher = drive_pattern.matcher(backslashes);
+
+ if (root_matcher.matches()) {
+ String rest = root_matcher.group(1);
+ return "/" + slashes(rest);
+ }
+ else if (drive_matcher.matches()) {
+ String letter = drive_matcher.group(1).toLowerCase(Locale.ROOT);
+ String rest = drive_matcher.group(2);
+ return "/cygdrive/" + letter + (rest.isEmpty() ? "" : "/" + slashes(rest));
+ }
+ else { return slashes(backslashes); }
+ }
+ else { return platform_path; }
+ }
+
+ private static class Expand_Platform_Path
+ {
+ private String _cygwin_root;
+ private StringBuilder _result = new StringBuilder();
+
+ public Expand_Platform_Path(String cygwin_root)
+ {
+ _cygwin_root = cygwin_root;
+ }
+
+ public String result() { return _result.toString(); }
+
+ void clear() { _result.setLength(0); }
+ void add(char c) { _result.append(c); }
+ void add(String s) { _result.append(s); }
+ void separator()
+ {
+ int n = _result.length();
+ if (n > 0 && _result.charAt(n - 1) != File.separatorChar) {
+ add(File.separatorChar);
+ }
+ }
+
+ public String check_root(String standard_path)
+ {
+ String rest = standard_path;
+ boolean is_root = standard_path.startsWith("/");
+
+ if (is_windows()) {
+ Pattern cygdrive_pattern = Pattern.compile("/cygdrive/([a-zA-Z])($|/.*)");
+ Matcher cygdrive_matcher = cygdrive_pattern.matcher(standard_path);
+
+ Pattern named_root_pattern = Pattern.compile("//+([^/]*)(.*)");
+ Matcher named_root_matcher = named_root_pattern.matcher(standard_path);
+
+ if (cygdrive_matcher.matches()) {
+ String drive = cygdrive_matcher.group(1).toUpperCase(Locale.ROOT);
+ rest = cygdrive_matcher.group(2);
+ clear();
+ add(drive);
+ add(':');
+ add(File.separatorChar);
+ }
+ else if (named_root_matcher.matches()) {
+ String root = named_root_matcher.group(1);
+ rest = named_root_matcher.group(2);
+ clear();
+ add(File.separatorChar);
+ add(File.separatorChar);
+ add(root);
+ }
+ else if (is_root) {
+ clear();
+ add(_cygwin_root);
+ }
+ }
+ else if (is_root) {
+ clear();
+ add(File.separatorChar);
+ }
+ return rest;
+ }
+
+ public void check_rest(Map<String,String> env, String main)
+ throws IOException, InterruptedException
+ {
+ for (String p : main.split("/", -1)) {
+ if (env != null && p.startsWith("$")) {
+ String var = p.substring(1);
+ String res = env.getOrDefault(var, "");
+ if (res.isEmpty()) {
+ throw new RuntimeException(
+ "Bad Isabelle environment variable: " + Library.quote(var));
+ }
+ else check(null, res);
+ }
+ else if (!p.isEmpty()) {
+ separator();
+ add(p);
+ }
+ }
+ }
+
+ public void check(Map<String,String> env, String path)
+ throws IOException, InterruptedException
+ {
+ check_rest(env, check_root(path));
+ }
+ }
+
+ public static String expand_platform_path(
+ Map<String,String> env, String cygwin_root, String standard_path)
+ throws IOException, InterruptedException
+ {
+ Expand_Platform_Path expand = new Expand_Platform_Path(cygwin_root);
+ expand.check(env, standard_path);
+ return expand.result();
+ }
+
+ public static String join_platform_paths(List<Path> paths)
+ {
+ List<String> strs = new LinkedList<String>();
+ for (Path p : paths) { strs.add(p.toString()); }
+ return String.join(File.pathSeparator, strs);
+ }
+
+ public static String join_standard_paths(List<Path> paths)
+ throws IOException, InterruptedException
+ {
+ List<String> strs = new LinkedList<String>();
+ for (Path p : paths) { strs.add(standard_path(p.toString())); }
+ return String.join(":", strs);
+ }
+
+
+ /* raw process */
+
+ public static ProcessBuilder process_builder(
+ List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
+ {
+ ProcessBuilder builder = new ProcessBuilder();
+
+ // fragile on Windows:
+ // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160
+ builder.command(cmd);
+
+ if (cwd != null) builder.directory(cwd);
+ if (env != null) {
+ builder.environment().clear();
+ builder.environment().putAll(env);
+ }
+ builder.redirectErrorStream(redirect);
+
+ return builder;
+ }
+
+ public static class Exec_Result
+ {
+ private final int _rc;
+ private final String _out;
+ private final String _err;
+
+ Exec_Result(int rc, String out, String err)
+ {
+ _rc = rc;
+ _out = Library.trim_line(out);
+ _err = Library.trim_line(err);
+ }
+
+ public int rc() { return _rc; }
+ public boolean ok() { return _rc == 0; }
+ public String out() { return _out; }
+ public String err() { return _err; }
+ }
+
+ public static Exec_Result exec_process(
+ List<String> command_line,
+ File cwd,
+ Map<String,String> env,
+ boolean redirect) throws IOException, InterruptedException
+ {
+ Path out_file = Files.createTempFile(null, null);
+ Path err_file = Files.createTempFile(null, null);
+ Exec_Result res;
+ try {
+ ProcessBuilder builder = process_builder(command_line, cwd, env, redirect);
+ builder.redirectOutput(out_file.toFile());
+ builder.redirectError(err_file.toFile());
+
+ Process proc = builder.start();
+ proc.getOutputStream().close();
+ try { proc.waitFor(); }
+ finally {
+ proc.getInputStream().close();
+ proc.getErrorStream().close();
+ proc.destroy();
+ Thread.interrupted();
+ }
+
+ int rc = proc.exitValue();
+ String out = Files.readString(out_file);
+ String err = Files.readString(err_file);
+ res = new Exec_Result(rc, out, err);
+ }
+ finally {
+ Files.deleteIfExists(out_file);
+ Files.deleteIfExists(err_file);
+ }
+ return res;
+ }
+
+
+ /* init (e.g. after extraction via 7zip) */
+
+ private static String bootstrap_directory(
+ String preference, String variable, String property, String description)
+ {
+ String a = preference; // explicit argument
+ String b = System.getenv(variable); // e.g. inherited from running isabelle tool
+ String c = System.getProperty(property); // e.g. via JVM application boot process
+ String dir;
+
+ if (a != null && !a.isEmpty()) { dir = a; }
+ else if (b != null && !b.isEmpty()) { dir = b; }
+ else if (c != null && !c.isEmpty()) { dir = c; }
+ else { throw new RuntimeException("Unknown " + description + " directory"); }
+
+ if ((new File(dir)).isDirectory()) { return dir; }
+ else {
+ throw new RuntimeException("Bad " + description + " directory " + Library.quote(dir));
+ }
+ }
+
+ private static void cygwin_exec(String isabelle_root, List<String> cmd)
+ throws IOException, InterruptedException
+ {
+ File cwd = new File(isabelle_root);
+ Map<String,String> env = new HashMap<String,String>(System.getenv());
+ env.put("CYGWIN", "nodosfilewarning");
+ Exec_Result res = exec_process(cmd, cwd, env, true);
+ if (!res.ok()) throw new RuntimeException(res.out());
+ }
+
+ public static void cygwin_link(String content, File target) throws IOException
+ {
+ Path target_path = target.toPath();
+ Files.writeString(target_path, "!<symlink>" + content + "\u0000");
+ Files.setAttribute(target_path, "dos:system", true);
+ }
+
+ public static void cygwin_init(String isabelle_root, String cygwin_root)
+ throws IOException, InterruptedException
+ {
+ if (is_windows()) {
+ File uninitialized_file = new File(cygwin_root, "isabelle\\uninitialized");
+ boolean uninitialized = uninitialized_file.isFile() && uninitialized_file.delete();
+
+ if (uninitialized) {
+ Path symlinks_path = (new File(cygwin_root + "\\isabelle\\symlinks")).toPath();
+ String[] symlinks = Files.readAllLines(symlinks_path).toArray(new String[0]);
+
+ // recover symlinks
+ int i = 0;
+ int m = symlinks.length;
+ int n = (m > 0 && symlinks[m - 1].isEmpty()) ? m - 1 : m;
+ while (i < n) {
+ if (i + 1 < n) {
+ String target = symlinks[i];
+ String content = symlinks[i + 1];
+ cygwin_link(content, new File(isabelle_root, target));
+ i += 2;
+ } else { throw new RuntimeException("Unbalanced symlinks list"); }
+ }
+
+ cygwin_exec(isabelle_root,
+ List.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall"));
+ cygwin_exec(isabelle_root,
+ List.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall"));
+ }
+ }
+ }
+
+
+ /* implicit settings environment */
+
+ private static volatile Map<String,String> _settings = null;
+
+ public static Map<String,String> settings()
+ throws IOException, InterruptedException
+ {
+ if (_settings == null) { init("", ""); } // unsynchronized check
+ return _settings;
+ }
+
+ public static String getenv(String name)
+ throws IOException, InterruptedException
+ {
+ return settings().getOrDefault(name, "");
+ }
+
+ public static synchronized void init(String _isabelle_root, String _cygwin_root)
+ throws IOException, InterruptedException
+ {
+ if (_settings == null) {
+ String isabelle_root =
+ bootstrap_directory(_isabelle_root, "ISABELLE_ROOT", "isabelle.root", "Isabelle root");
+
+ String cygwin_root = "";
+ if (is_windows()) {
+ cygwin_root = bootstrap_directory(_cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root");
+ cygwin_init(isabelle_root, cygwin_root);
+ }
+
+ Map<String,String> env = new HashMap<String,String>(System.getenv());
+
+ BiFunction<String,String,Void> env_default =
+ (String a, String b) -> { if (!b.isEmpty()) env.putIfAbsent(a, b); return null; };
+
+ String temp_windows = is_windows() ? System.getenv("TEMP") : null;
+
+ env_default.apply("CYGWIN_ROOT", cygwin_root);
+ env_default.apply("TEMP_WINDOWS",
+ (temp_windows != null && temp_windows.contains("\\")) ? temp_windows : "");
+ env_default.apply("ISABELLE_JDK_HOME",
+ standard_path(cygwin_root, System.getProperty("java.home", "")));
+ env_default.apply("HOME", System.getProperty("user.home", ""));
+ env_default.apply("ISABELLE_APP", System.getProperty("isabelle.app", ""));
+
+ Map<String,String> settings = new HashMap<String,String>();
+ Path settings_file = Files.createTempFile(null, null);
+ try {
+ List<String> cmd = new LinkedList<String>();
+ if (is_windows()) {
+ cmd.add(cygwin_root + "\\bin\\bash");
+ cmd.add("-l");
+ cmd.add(standard_path(cygwin_root, isabelle_root + "\\bin\\isabelle"));
+ } else {
+ cmd.add(isabelle_root + "/bin/isabelle");
+ }
+ cmd.add("getenv");
+ cmd.add("-d");
+ cmd.add(settings_file.toString());
+
+ Exec_Result res = exec_process(cmd, null, env, true);
+ if (!res.ok()) throw new RuntimeException(res.out());
+
+ for (String s : Files.readString(settings_file).split("\u0000", -1)) {
+ int i = s.indexOf('=');
+ if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
+ else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }
+ }
+ }
+ finally { Files.delete(settings_file); }
+
+ if (is_windows()) { settings.put("CYGWIN_ROOT", cygwin_root); }
+
+ settings.put("PATH", settings.get("PATH_JVM"));
+ settings.remove("PATH_JVM");
+
+ _settings = Map.copyOf(settings);
+ }
+ }
+
+
+ /* Cygwin root (after init) */
+
+ public static String cygwin_root()
+ throws IOException, InterruptedException
+ {
+ return getenv("CYGWIN_ROOT");
+ }
+
+ public static String standard_path(String platform_path)
+ throws IOException, InterruptedException
+ {
+ return standard_path(cygwin_root(), platform_path);
+ }
+
+ public static String expand_platform_path(String standard_path)
+ throws IOException, InterruptedException
+ {
+ return expand_platform_path(settings(), cygwin_root(), standard_path);
+ }
+
+ public static String platform_path(String standard_path)
+ throws IOException, InterruptedException
+ {
+ return expand_platform_path(null, cygwin_root(), standard_path);
+ }
+
+
+ /* kill process (via bash) */
+
+ static public boolean kill_process(String group_pid, String signal)
+ throws IOException, InterruptedException
+ {
+ List<String> cmd = new LinkedList<String>();
+ if (is_windows()) {
+ cmd.add(cygwin_root() + "\\bin\\bash.exe");
+ }
+ else {
+ cmd.add("/usr/bin/env");
+ cmd.add("bash");
+ }
+ cmd.add("-c");
+ cmd.add("kill -" + signal + " -" + group_pid);
+ return exec_process(cmd, null, null, false).ok();
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Exn.java Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,83 @@
+/* Title: Tools/Setup/src/Exn.java
+ Author: Makarius
+
+Support for exceptions (arbitrary throwables).
+*/
+
+package isabelle.setup;
+
+
+import java.io.IOException;
+import java.util.LinkedList;
+import java.util.List;
+
+
+public class Exn
+{
+ /* interrupts */
+
+ public static boolean is_interrupt(Throwable exn)
+ {
+ boolean found_interrupt = false;
+ Throwable e = exn;
+ while (!found_interrupt && e != null) {
+ found_interrupt = e instanceof InterruptedException;
+ e = e.getCause();
+ }
+ return found_interrupt;
+ }
+
+ public static int INTERRUPT_RETURN_CODE = 130;
+
+ public static int return_code(Throwable exn, int rc)
+ {
+ return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc;
+ }
+
+
+ /* message */
+
+ public static String message(Throwable exn)
+ {
+ String msg = exn.getMessage();
+
+ if (exn.getClass() == RuntimeException.class)
+ {
+ return msg == null || msg.isEmpty() ? "Error" : msg;
+ }
+ else if (exn instanceof IOException)
+ {
+ return msg == null || msg.isEmpty() ? "I/O error" : "I/O error: " + msg;
+ }
+ else if (exn instanceof RuntimeException && !msg.isEmpty()) { return msg; }
+ else if (exn instanceof InterruptedException) { return "Interrupt"; }
+ else { return exn.toString(); }
+ }
+
+
+ /* print */
+
+ public static String trace(Throwable exn)
+ {
+ List<String> list = new LinkedList<String>();
+ for (StackTraceElement elem : exn.getStackTrace()) {
+ list.add(elem.toString());
+ }
+ return Library.cat_lines(list);
+ }
+
+ public static boolean debug()
+ {
+ return System.getProperty("isabelle.debug", "").equals("true");
+ }
+
+ public static String print(Throwable exn)
+ {
+ return debug() ? message(exn) + "\n" + trace(exn) : message(exn);
+ }
+
+ public static String print_error(Throwable exn)
+ {
+ return Library.prefix_lines("*** ", print(exn));
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Library.java Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,53 @@
+/* Title: Tools/Setup/src/Library.java
+ Author: Makarius
+
+Basic library.
+*/
+
+package isabelle.setup;
+
+
+import java.util.Arrays;
+import java.util.LinkedList;
+import java.util.List;
+
+
+public class Library
+{
+ public static String quote(String s)
+ {
+ return "\"" + s + "\"";
+ }
+
+ public static String cat_lines(Iterable<? extends CharSequence> lines)
+ {
+ return String.join("\n", lines);
+ }
+
+ public static List<String> split_lines(String str)
+ {
+ if (str.isEmpty()) { return List.of(); }
+ else {
+ List<String> result = new LinkedList<String>();
+ result.addAll(Arrays.asList(str.split("\\n")));
+ return List.copyOf(result);
+ }
+ }
+
+ public static String prefix_lines(String prfx, String str)
+ {
+ if (str.isEmpty()) { return str; }
+ else {
+ List<String> lines = new LinkedList<String>();
+ for (String line : split_lines(str)) { lines.add(prfx + line); }
+ return cat_lines(lines);
+ }
+ }
+
+ public static String trim_line(String s)
+ {
+ if (s.endsWith("\r\n")) { return s.substring(0, s.length() - 2); }
+ else if (s.endsWith("\r") || s.endsWith("\n")) { return s.substring(0, s.length() - 1); }
+ else { return s; }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Setup/src/Setup.java Sat Jul 17 21:40:57 2021 +0200
@@ -0,0 +1,65 @@
+/* Title: Tools/Setup/src/Setup.java
+ Author: Makarius
+
+Isabelle setup tool: bootstrap from generic Java environment.
+*/
+
+package isabelle.setup;
+
+
+class Setup
+{
+ private static void echo(String msg)
+ {
+ System.out.print(msg + "\n");
+ }
+ private static void echo_err(String msg)
+ {
+ System.err.print(msg + "\n");
+ }
+ private static void fail(String msg)
+ {
+ echo_err(msg);
+ System.exit(2);
+ }
+
+ private static void check_args(boolean b)
+ {
+ if (!b) { fail("Bad command-line arguments"); }
+ }
+
+ public static void main(String[] args)
+ {
+ int n = args.length;
+ check_args(n > 0);
+
+ String op = args[0];
+ try {
+ switch (op) {
+ case "build":
+ check_args(n == 1);
+ Build.build_components(false);
+ break;
+ case "build_fresh":
+ check_args(n == 1);
+ Build.build_components(true);
+ break;
+ case "classpath":
+ check_args(n == 1);
+ echo(Environment.join_standard_paths(Build.classpath()));
+ break;
+ case "services":
+ check_args(n == 1);
+ for (String s : Build.services()) { echo(s); }
+ break;
+ default:
+ fail("Bad setup operation " + Library.quote(op));
+ break;
+ }
+ }
+ catch (Throwable exn) {
+ echo_err(Exn.print_error(exn));
+ System.exit(Exn.return_code(exn, 2));
+ }
+ }
+}