| author | wenzelm | 
| Sun, 24 Mar 2024 19:14:56 +0100 | |
| changeset 79980 | ee04ce2ac13f | 
| parent 77027 | ac7af931189f | 
| child 82142 | 508a673c87ac | 
| permissions | -rw-r--r-- | 
| 74055 | 1 | /* Title: Pure/Tools/scala_build.scala | 
| 2 | Author: Makarius | |
| 3 | ||
| 75661 | 4 | Manage and build Isabelle/Scala/Java modules. | 
| 74055 | 5 | */ | 
| 6 | ||
| 7 | package isabelle | |
| 8 | ||
| 9 | ||
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 10 | import java.io.{ByteArrayOutputStream, PrintStream}
 | 
| 74055 | 11 | import java.nio.file.Files | 
| 75869 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 12 | import java.nio.file.{Path => JPath}
 | 
| 74055 | 13 | |
| 14 | import scala.jdk.CollectionConverters._ | |
| 15 | ||
| 16 | ||
| 75393 | 17 | object Scala_Build {
 | 
| 18 |   class Context private[Scala_Build](java_context: isabelle.setup.Build.Context) {
 | |
| 74057 | 19 | override def toString: String = java_context.toString | 
| 20 | ||
| 75393 | 21 |     def is_module(path: Path): Boolean = {
 | 
| 74057 | 22 | val module_name = java_context.module_name() | 
| 74056 | 23 | module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file) | 
| 24 | } | |
| 25 | ||
| 75393 | 26 |     def module_result: Option[Path] = {
 | 
| 74062 | 27 |       java_context.module_result() match {
 | 
| 28 | case "" => None | |
| 29 | case module => Some(File.path(java_context.path(module).toFile)) | |
| 30 | } | |
| 31 | } | |
| 32 | ||
| 74056 | 33 | def sources: List[Path] = | 
| 34 | java_context.sources().asScala.toList.map(s => File.path(java_context.path(s).toFile)) | |
| 35 | ||
| 36 | def requirements: List[Path] = | |
| 37 |       (for {
 | |
| 38 | s <- java_context.requirements().asScala.iterator | |
| 39 | p <- java_context.requirement_paths(s).asScala.iterator | |
| 40 | } yield (File.path(p.toFile))).toList | |
| 41 | ||
| 75869 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 42 | def build( | 
| 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 43 |       classpath: List[Path] = Path.split(Isabelle_System.getenv("ISABELLE_CLASSPATH")),
 | 
| 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 44 | fresh: Boolean = false | 
| 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 45 |     ): String = {
 | 
| 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 46 | val java_classpath = new java.util.LinkedList[JPath] | 
| 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 47 | classpath.foreach(path => java_classpath.add(path.java_path)) | 
| 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 48 | |
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 49 | val output0 = new ByteArrayOutputStream | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 50 | val output = new PrintStream(output0) | 
| 75393 | 51 |       def get_output(): String = {
 | 
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 52 | output.flush() | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 53 | Library.trim_line(output0.toString(UTF8.charset)) | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 54 | } | 
| 75869 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 55 | |
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 56 |       try {
 | 
| 75869 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 57 | isabelle.setup.Build.build(java_classpath, output, java_context, fresh) | 
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 58 | get_output() | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 59 | } | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 60 |       catch { case ERROR(msg) => cat_error(get_output(), msg) }
 | 
| 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 61 | } | 
| 74056 | 62 | } | 
| 74055 | 63 | |
| 64 | def context(dir: Path, | |
| 65 | component: Boolean = false, | |
| 74060 | 66 | no_title: Boolean = false, | 
| 74057 | 67 | do_build: Boolean = false, | 
| 75393 | 68 | module: Option[Path] = None | 
| 69 |   ): Context = {
 | |
| 74055 | 70 | val props_name = | 
| 71 | if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS | |
| 72 | else isabelle.setup.Build.BUILD_PROPS | |
| 73 | val props_path = dir + Path.explode(props_name) | |
| 74 | ||
| 79980 | 75 | val props = File.read_props(props_path) | 
| 74060 | 76 | if (no_title) props.remove(isabelle.setup.Build.TITLE) | 
| 74057 | 77 | if (do_build) props.remove(isabelle.setup.Build.NO_BUILD) | 
| 78 | if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get)) | |
| 74055 | 79 | |
| 74056 | 80 | new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode)) | 
| 74055 | 81 | } | 
| 82 | ||
| 75393 | 83 |   sealed case class Result(output: String, jar_bytes: Bytes, jar_path: Option[Path]) {
 | 
| 84 |     def write(): Unit = {
 | |
| 74062 | 85 |       if (jar_path.isDefined) {
 | 
| 86 | Isabelle_System.make_directory(jar_path.get.dir) | |
| 87 | Bytes.write(jar_path.get, jar_bytes) | |
| 88 | } | |
| 89 | } | |
| 90 | } | |
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 91 | |
| 75393 | 92 |   def build_result(dir: Path, component: Boolean = false): Result = {
 | 
| 75394 | 93 |     Isabelle_System.with_tmp_file("result", "jar") { tmp_file =>
 | 
| 74061 
203dfa8bc0fc
clarified compiler output: allow multithreaded execution;
 wenzelm parents: 
74060diff
changeset | 94 | val output = | 
| 75657 | 95 | context(dir, component = component, no_title = true, do_build = true, | 
| 75869 
ee2f93fa2440
proper Java/Scala compiler classpath (amending b42e20adaeed): ISABELLE_SETUP_CLASSPATH must not be included prematurely (breaks on Windows), instead use runtime Classpath().jars;
 wenzelm parents: 
75687diff
changeset | 96 | module = Some(tmp_file)).build(classpath = Classpath().jars.map(File.path)) | 
| 74062 | 97 | val jar_bytes = Bytes.read(tmp_file) | 
| 98 | val jar_path = context(dir, component = component).module_result | |
| 99 | Result(output, jar_bytes, jar_path) | |
| 75394 | 100 | } | 
| 74055 | 101 | } | 
| 102 | ||
| 75660 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 103 |   object Scala_Fun extends Scala.Fun("scala_build") with Scala.Bytes_Fun {
 | 
| 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 104 | val here = Scala_Project.here | 
| 77027 | 105 | def invoke(session: Session, args: List[Bytes]): List[Bytes] = | 
| 75660 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 106 |       args match {
 | 
| 75687 | 107 | case List(dir) => | 
| 108 | val result = build_result(Path.explode(dir.text)) | |
| 75660 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 109 | val jar_name = | 
| 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 110 |             result.jar_path match {
 | 
| 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 111 | case Some(path) => path.file_name | 
| 75678 | 112 | case None => "scala_build.jar" | 
| 75660 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 113 | } | 
| 75678 | 114 |           List(Bytes("classpath/" + jar_name), result.jar_bytes, Bytes(result.output))
 | 
| 75660 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 115 |         case _ => error("Bad arguments")
 | 
| 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 116 | } | 
| 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 117 | } | 
| 
45d3497c0baa
support for Isabelle/Scala/Java modules in Isabelle/ML;
 wenzelm parents: 
75657diff
changeset | 118 | |
| 74055 | 119 | def component_contexts(): List[Context] = | 
| 74056 | 120 | isabelle.setup.Build.component_contexts().asScala.toList.map(new Context(_)) | 
| 74055 | 121 | } |