| author | wenzelm | 
| Tue, 18 Jul 2023 12:50:34 +0200 | |
| changeset 78392 | 27c2fa1db6ed | 
| parent 77027 | ac7af931189f | 
| child 79980 | ee04ce2ac13f | 
| 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  | 
| 77027 | 107  | 
def invoke(session: Session, args: List[Bytes]): List[Bytes] =  | 
| 
75660
 
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  | 
}  |