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