diff --git a/etc/build.props b/etc/build.props --- a/etc/build.props +++ b/etc/build.props @@ -1,291 +1,292 @@ 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/ \ lib/logo/isabelle_transparent-32.gif:isabelle/ \ lib/logo/isabelle_transparent.gif:isabelle/ sources = \ src/HOL/SPARK/Tools/spark.scala \ src/HOL/Tools/ATP/system_on_tptp.scala \ src/HOL/Tools/Mirabelle/mirabelle.scala \ src/HOL/Tools/Nitpick/kodkod.scala \ src/Pure/Admin/afp.scala \ src/Pure/Admin/build_csdp.scala \ src/Pure/Admin/build_cygwin.scala \ src/Pure/Admin/build_doc.scala \ src/Pure/Admin/build_e.scala \ src/Pure/Admin/build_fonts.scala \ src/Pure/Admin/build_history.scala \ src/Pure/Admin/build_jcef.scala \ src/Pure/Admin/build_jdk.scala \ src/Pure/Admin/build_jedit.scala \ src/Pure/Admin/build_log.scala \ src/Pure/Admin/build_polyml.scala \ src/Pure/Admin/build_release.scala \ src/Pure/Admin/build_spass.scala \ src/Pure/Admin/build_sqlite.scala \ src/Pure/Admin/build_status.scala \ src/Pure/Admin/build_vampire.scala \ src/Pure/Admin/build_verit.scala \ src/Pure/Admin/build_zipperposition.scala \ src/Pure/Admin/check_sources.scala \ src/Pure/Admin/ci_profile.scala \ src/Pure/Admin/isabelle_cronjob.scala \ src/Pure/Admin/isabelle_devel.scala \ src/Pure/Admin/jenkins.scala \ src/Pure/Admin/other_isabelle.scala \ src/Pure/Concurrent/consumer_thread.scala \ src/Pure/Concurrent/counter.scala \ src/Pure/Concurrent/delay.scala \ src/Pure/Concurrent/event_timer.scala \ src/Pure/Concurrent/future.scala \ src/Pure/Concurrent/isabelle_thread.scala \ src/Pure/Concurrent/mailbox.scala \ src/Pure/Concurrent/par_list.scala \ src/Pure/Concurrent/synchronized.scala \ src/Pure/GUI/color_value.scala \ src/Pure/GUI/desktop_app.scala \ src/Pure/GUI/gui.scala \ src/Pure/GUI/gui_thread.scala \ src/Pure/GUI/popup.scala \ src/Pure/GUI/wrap_panel.scala \ src/Pure/General/antiquote.scala \ src/Pure/General/bytes.scala \ src/Pure/General/cache.scala \ src/Pure/General/codepoint.scala \ src/Pure/General/comment.scala \ src/Pure/General/completion.scala \ src/Pure/General/csv.scala \ src/Pure/General/date.scala \ src/Pure/General/exn.scala \ src/Pure/General/file.scala \ src/Pure/General/file_watcher.scala \ src/Pure/General/graph.scala \ src/Pure/General/graph_display.scala \ src/Pure/General/graphics_file.scala \ src/Pure/General/http.scala \ src/Pure/General/json.scala \ src/Pure/General/linear_set.scala \ src/Pure/General/logger.scala \ src/Pure/General/long_name.scala \ src/Pure/General/mailman.scala \ src/Pure/General/mercurial.scala \ src/Pure/General/multi_map.scala \ src/Pure/General/output.scala \ src/Pure/General/path.scala \ src/Pure/General/position.scala \ src/Pure/General/pretty.scala \ src/Pure/General/properties.scala \ src/Pure/General/rdf.scala \ src/Pure/General/scan.scala \ src/Pure/General/sha1.scala \ src/Pure/General/sql.scala \ src/Pure/General/ssh.scala \ src/Pure/General/symbol.scala \ src/Pure/General/time.scala \ src/Pure/General/timing.scala \ src/Pure/General/untyped.scala \ src/Pure/General/url.scala \ src/Pure/General/utf8.scala \ src/Pure/General/uuid.scala \ src/Pure/General/value.scala \ src/Pure/General/word.scala \ src/Pure/General/xz.scala \ src/Pure/Isar/document_structure.scala \ src/Pure/Isar/keyword.scala \ src/Pure/Isar/line_structure.scala \ src/Pure/Isar/outer_syntax.scala \ src/Pure/Isar/parse.scala \ src/Pure/Isar/token.scala \ src/Pure/ML/ml_console.scala \ src/Pure/ML/ml_lex.scala \ src/Pure/ML/ml_process.scala \ src/Pure/ML/ml_profiling.scala \ src/Pure/ML/ml_statistics.scala \ src/Pure/ML/ml_syntax.scala \ src/Pure/PIDE/byte_message.scala \ src/Pure/PIDE/command.scala \ src/Pure/PIDE/command_span.scala \ src/Pure/PIDE/document.scala \ src/Pure/PIDE/document_id.scala \ src/Pure/PIDE/document_status.scala \ src/Pure/PIDE/editor.scala \ src/Pure/PIDE/headless.scala \ src/Pure/PIDE/line.scala \ src/Pure/PIDE/markup.scala \ src/Pure/PIDE/markup_tree.scala \ src/Pure/PIDE/protocol.scala \ src/Pure/PIDE/protocol_handlers.scala \ src/Pure/PIDE/protocol_message.scala \ src/Pure/PIDE/prover.scala \ src/Pure/PIDE/query_operation.scala \ src/Pure/PIDE/rendering.scala \ src/Pure/PIDE/resources.scala \ src/Pure/PIDE/session.scala \ src/Pure/PIDE/text.scala \ src/Pure/PIDE/xml.scala \ src/Pure/PIDE/yxml.scala \ src/Pure/ROOT.scala \ src/Pure/System/bash.scala \ src/Pure/System/command_line.scala \ src/Pure/System/components.scala \ src/Pure/System/executable.scala \ src/Pure/System/getopts.scala \ src/Pure/System/isabelle_charset.scala \ src/Pure/System/isabelle_fonts.scala \ src/Pure/System/isabelle_platform.scala \ src/Pure/System/isabelle_process.scala \ src/Pure/System/isabelle_system.scala \ src/Pure/System/isabelle_tool.scala \ src/Pure/System/java_statistics.scala \ src/Pure/System/linux.scala \ src/Pure/System/mingw.scala \ src/Pure/System/numa.scala \ src/Pure/System/options.scala \ src/Pure/System/platform.scala \ src/Pure/System/posix_interrupt.scala \ src/Pure/System/process_result.scala \ src/Pure/System/progress.scala \ src/Pure/System/scala.scala \ src/Pure/System/system_channel.scala \ src/Pure/System/tty_loop.scala \ src/Pure/Thy/bibtex.scala \ src/Pure/Thy/document_build.scala \ src/Pure/Thy/export.scala \ src/Pure/Thy/export_theory.scala \ src/Pure/Thy/file_format.scala \ src/Pure/Thy/html.scala \ src/Pure/Thy/latex.scala \ src/Pure/Thy/presentation.scala \ src/Pure/Thy/sessions.scala \ src/Pure/Thy/thy_element.scala \ src/Pure/Thy/thy_header.scala \ src/Pure/Thy/thy_syntax.scala \ src/Pure/Tools/build.scala \ src/Pure/Tools/build_docker.scala \ src/Pure/Tools/build_job.scala \ src/Pure/Tools/check_keywords.scala \ src/Pure/Tools/debugger.scala \ src/Pure/Tools/doc.scala \ src/Pure/Tools/dump.scala \ src/Pure/Tools/fontforge.scala \ src/Pure/Tools/java_monitor.scala \ src/Pure/Tools/logo.scala \ src/Pure/Tools/mkroot.scala \ src/Pure/Tools/phabricator.scala \ src/Pure/Tools/print_operation.scala \ src/Pure/Tools/profiling_report.scala \ + src/Pure/Tools/scala_build.scala \ src/Pure/Tools/scala_project.scala \ src/Pure/Tools/server.scala \ src/Pure/Tools/server_commands.scala \ src/Pure/Tools/simplifier_trace.scala \ src/Pure/Tools/spell_checker.scala \ src/Pure/Tools/task_statistics.scala \ src/Pure/Tools/update.scala \ src/Pure/Tools/update_cartouches.scala \ src/Pure/Tools/update_comments.scala \ src/Pure/Tools/update_header.scala \ src/Pure/Tools/update_then.scala \ src/Pure/Tools/update_theorems.scala \ src/Pure/library.scala \ src/Pure/pure_thy.scala \ src/Pure/term.scala \ src/Pure/term_xml.scala \ src/Pure/thm_name.scala \ src/Tools/Graphview/graph_file.scala \ src/Tools/Graphview/graph_panel.scala \ src/Tools/Graphview/graphview.scala \ src/Tools/Graphview/layout.scala \ src/Tools/Graphview/main_panel.scala \ src/Tools/Graphview/metrics.scala \ src/Tools/Graphview/model.scala \ src/Tools/Graphview/mutator.scala \ src/Tools/Graphview/mutator_dialog.scala \ src/Tools/Graphview/mutator_event.scala \ src/Tools/Graphview/popups.scala \ src/Tools/Graphview/shapes.scala \ src/Tools/Graphview/tree_panel.scala \ src/Tools/VSCode/src/build_vscode.scala \ src/Tools/VSCode/src/channel.scala \ src/Tools/VSCode/src/dynamic_output.scala \ src/Tools/VSCode/src/language_server.scala \ src/Tools/VSCode/src/lsp.scala \ src/Tools/VSCode/src/preview_panel.scala \ src/Tools/VSCode/src/state_panel.scala \ src/Tools/VSCode/src/textmate_grammar.scala \ src/Tools/VSCode/src/vscode_model.scala \ src/Tools/VSCode/src/vscode_rendering.scala \ src/Tools/VSCode/src/vscode_resources.scala \ src/Tools/VSCode/src/vscode_spell_checker.scala \ src/Tools/jEdit/src/active.scala \ src/Tools/jEdit/src/base_plugin.scala \ src/Tools/jEdit/src/completion_popup.scala \ src/Tools/jEdit/src/context_menu.scala \ src/Tools/jEdit/src/debugger_dockable.scala \ src/Tools/jEdit/src/dockable.scala \ src/Tools/jEdit/src/document_model.scala \ src/Tools/jEdit/src/document_view.scala \ src/Tools/jEdit/src/documentation_dockable.scala \ src/Tools/jEdit/src/fold_handling.scala \ src/Tools/jEdit/src/font_info.scala \ src/Tools/jEdit/src/graphview_dockable.scala \ src/Tools/jEdit/src/info_dockable.scala \ src/Tools/jEdit/src/isabelle.scala \ src/Tools/jEdit/src/isabelle_encoding.scala \ src/Tools/jEdit/src/isabelle_export.scala \ src/Tools/jEdit/src/isabelle_options.scala \ src/Tools/jEdit/src/isabelle_session.scala \ src/Tools/jEdit/src/isabelle_vfs.scala \ src/Tools/jEdit/src/jedit_bibtex.scala \ src/Tools/jEdit/src/jedit_editor.scala \ src/Tools/jEdit/src/jedit_lib.scala \ src/Tools/jEdit/src/jedit_options.scala \ src/Tools/jEdit/src/jedit_rendering.scala \ src/Tools/jEdit/src/jedit_resources.scala \ src/Tools/jEdit/src/jedit_sessions.scala \ src/Tools/jEdit/src/jedit_spell_checker.scala \ src/Tools/jEdit/src/keymap_merge.scala \ src/Tools/jEdit/src/main.scala \ src/Tools/jEdit/src/main_plugin.scala \ src/Tools/jEdit/src/monitor_dockable.scala \ src/Tools/jEdit/src/output_dockable.scala \ src/Tools/jEdit/src/pide_docking_framework.scala \ src/Tools/jEdit/src/pretty_text_area.scala \ src/Tools/jEdit/src/pretty_tooltip.scala \ src/Tools/jEdit/src/process_indicator.scala \ src/Tools/jEdit/src/protocol_dockable.scala \ src/Tools/jEdit/src/query_dockable.scala \ src/Tools/jEdit/src/raw_output_dockable.scala \ src/Tools/jEdit/src/rich_text_area.scala \ src/Tools/jEdit/src/session_build.scala \ src/Tools/jEdit/src/simplifier_trace_dockable.scala \ src/Tools/jEdit/src/simplifier_trace_window.scala \ src/Tools/jEdit/src/sledgehammer_dockable.scala \ src/Tools/jEdit/src/state_dockable.scala \ src/Tools/jEdit/src/status_widget.scala \ src/Tools/jEdit/src/symbols_dockable.scala \ src/Tools/jEdit/src/syntax_style.scala \ src/Tools/jEdit/src/syslog_dockable.scala \ src/Tools/jEdit/src/text_overview.scala \ src/Tools/jEdit/src/text_structure.scala \ src/Tools/jEdit/src/theories_dockable.scala \ src/Tools/jEdit/src/timing_dockable.scala \ src/Tools/jEdit/src/token_markup.scala services = \ isabelle.Bibtex$File_Format \ isabelle.Document_Build$Build_Engine \ isabelle.Document_Build$LuaLaTeX_Engine \ isabelle.Document_Build$PDFLaTeX_Engine \ isabelle.ML_Statistics$Handler \ isabelle.Print_Operation$Handler \ isabelle.Scala$Handler \ isabelle.Scala_Functions \ isabelle.Server_Commands \ isabelle.Sessions$File_Format \ isabelle.Simplifier_Trace$Handler \ isabelle.Tools \ isabelle.nitpick.Kodkod$Handler \ isabelle.nitpick.Scala_Functions \ isabelle.spark.SPARK$Load_Command1 \ isabelle.spark.SPARK$Load_Command2 diff --git a/src/Pure/Tools/scala_build.scala b/src/Pure/Tools/scala_build.scala new file mode 100644 --- /dev/null +++ b/src/Pure/Tools/scala_build.scala @@ -0,0 +1,47 @@ +/* Title: Pure/Tools/scala_build.scala + Author: Makarius + +Manage and build Isabelle/Scala/Java components. +*/ + +package isabelle + + +import java.util.{Properties => JProperties} +import java.nio.file.Files + +import scala.jdk.CollectionConverters._ + + +object Scala_Build +{ + type Context = isabelle.setup.Build.Context + + def context(dir: Path, + component: Boolean = false, + more_props: Properties.T = Nil): Context = + { + val props_name = + if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS + else isabelle.setup.Build.BUILD_PROPS + val props_path = dir + Path.explode(props_name) + + val props = new JProperties + props.load(Files.newBufferedReader(props_path.java_path)) + for ((a, b) <- more_props) props.put(a, b) + + new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode) + } + + def build(dir: Path, + fresh: Boolean = false, + component: Boolean = false, + more_props: Properties.T = Nil): Unit = + { + isabelle.setup.Build.build( + context(dir, component = component, more_props = more_props), fresh) + } + + def component_contexts(): List[Context] = + isabelle.setup.Build.component_contexts().asScala.toList +} diff --git a/src/Pure/Tools/scala_project.scala b/src/Pure/Tools/scala_project.scala --- a/src/Pure/Tools/scala_project.scala +++ b/src/Pure/Tools/scala_project.scala @@ -1,200 +1,195 @@ /* Title: Pure/Tools/scala_project.scala Author: Makarius Manage Isabelle/Scala/Java project sources, with output to Gradle for IntelliJ IDEA. */ package isabelle import scala.jdk.CollectionConverters._ object Scala_Project { /* groovy syntax */ def groovy_string(s: String): String = { s.map(c => c match { case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c case _ => c.toString }).mkString("'", "", "'") } /* file and directories */ - def plugin_contexts(): List[isabelle.setup.Build.Context] = + def plugin_contexts(): List[Scala_Build.Context] = for (plugin <- List("jedit_base", "jedit_main")) - yield { - val dir = Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin) - isabelle.setup.Build.directory_context(dir.java_path) - } + yield Scala_Build.context(Path.explode("$ISABELLE_HOME/src/Tools/jEdit") + Path.basic(plugin)) lazy val isabelle_files: (List[Path], List[Path]) = { - val contexts = - isabelle.setup.Build.component_contexts().asScala.toList ::: - plugin_contexts() + val contexts = Scala_Build.component_contexts() ::: plugin_contexts() val jars1 = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")) val jars2 = (for { context <- contexts.iterator s <- context.requirements().asScala.iterator path <- context.requirement_paths(s).asScala.iterator } yield File.path(path.toFile)).toList val jar_files = Library.distinct(jars1 ::: jars2).filterNot(path => contexts.exists(context => { val name: String = context.module_name() name.nonEmpty && File.eq(context.path(name).toFile, path.file) })) val source_files = (for { context <- contexts.iterator file <- context.sources.asScala.iterator if file.endsWith(".scala") || file.endsWith(".java") } yield File.path(context.path(file).toFile)).toList (jar_files, source_files) } lazy val isabelle_scala_files: Map[String, Path] = { - val context = isabelle.setup.Build.component_context(Path.ISABELLE_HOME.java_path) + val context = Scala_Build.context(Path.ISABELLE_HOME, component = true) context.sources().asScala.iterator.foldLeft(Map.empty[String, Path]) { case (map, name) => if (name.endsWith(".scala")) { val path = File.path(context.path(name).toFile) val base = path.base.implode map.get(base) match { case None => map + (base -> path) case Some(path2) => error("Conflicting base names: " + path + " vs. " + path2) } } else map } } /* compile-time position */ def here: Here = { val exn = new Exception exn.getStackTrace.toList match { case _ :: caller :: _ => val name = proper_string(caller.getFileName).getOrElse("") val line = caller.getLineNumber new Here(name, line) case _ => new Here("", 0) } } class Here private[Scala_Project](name: String, line: Int) { override def toString: String = name + ":" + line def position: Position.T = isabelle_scala_files.get(name) match { case Some(path) => Position.Line_File(line, path.implode) case None => Position.none } } /* scala project */ def package_dir(source_file: Path): Option[Path] = { val is_java = source_file.file_name.endsWith(".java") val lines = split_lines(File.read(source_file)) val Package = """\s*\bpackage\b\s*(?:object\b\s*)?((?:\w|\.)+)\b.*""".r lines.collectFirst( { case Package(name) => if (is_java) Path.explode(space_explode('.', name).mkString("/")) else Path.basic(name) }) } def the_package_dir(source_file: Path): Path = package_dir(source_file) getOrElse error("Failed to guess package from " + source_file) def scala_project(project_dir: Path, symlinks: Boolean = false): Unit = { if (symlinks && Platform.is_windows) error("Cannot create symlinks on Windows") if (project_dir.is_file || project_dir.is_dir) error("Project directory already exists: " + project_dir) val java_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/java")) val scala_src_dir = Isabelle_System.make_directory(project_dir + Path.explode("src/main/scala")) val (jar_files, source_files) = isabelle_files isabelle_scala_files for (source <- source_files) { val dir = if (source.file_name.endsWith(".java")) java_src_dir else scala_src_dir val target = dir + the_package_dir(source) Isabelle_System.make_directory(target) if (symlinks) Isabelle_System.symlink(source, target) else Isabelle_System.copy_file(source, target) } File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n") File.write(project_dir + Path.explode("build.gradle"), """plugins { id 'scala' } repositories { mavenCentral() } dependencies { implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """' compile files( """ + jar_files.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n ", ")") + """ } """) } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit", Scala_Project.here, args => { var symlinks = false val getopts = Getopts(""" Usage: isabelle scala_project [OPTIONS] PROJECT_DIR Options are: -L make symlinks to original scala files Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs such as IntelliJ IDEA. """, "L" -> (_ => symlinks = true)) val more_args = getopts(args) val project_dir = more_args match { case List(dir) => Path.explode(dir) case _ => getopts.usage() } scala_project(project_dir, symlinks = symlinks) }) } diff --git a/src/Tools/Setup/src/Build.java b/src/Tools/Setup/src/Build.java --- a/src/Tools/Setup/src/Build.java +++ b/src/Tools/Setup/src/Build.java @@ -1,568 +1,559 @@ /* 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)); } + props.load(Files.newBufferedReader(props_path)); return new Context(dir, props, props_path.toString()); } public static List component_contexts() throws IOException, InterruptedException { List result = new LinkedList(); 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 get_list(String name) { List list = new LinkedList(); for (String s : _props.getProperty(name, "").split("\\s+")) { if (!s.isEmpty()) { list.add(s); } } 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"); } 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 requirement_paths(String s) throws IOException, InterruptedException { 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)); 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 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 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, ""); } } /** compile sources **/ private static void add_options(List 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 deps, List sources) throws IOException, InterruptedException { ArrayList args = new ArrayList(); 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 deps, List sources) throws IOException, InterruptedException { JavaCompiler compiler = ToolProvider.getSystemJavaCompiler(); StandardJavaFileManager file_manager = compiler.getStandardFileManager(null, Locale.ROOT, StandardCharsets.UTF_8); List options = new LinkedList(); 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 java_sources = new LinkedList(); 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 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 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 classpath() throws IOException, InterruptedException { List result = new LinkedList(); for (Context context : component_contexts()) { String module = context.module(); if (!module.isEmpty()) { result.add(context.path(module)); } } return List.copyOf(result); } public static List services() throws IOException, InterruptedException { List result = new LinkedList(); 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 requirements = context.requirements(); List resources = context.resources(); List sources = context.sources(); 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) { List 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 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); /* 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 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); } } }