src/Pure/Tools/scala_build.scala
author wenzelm
Wed, 12 Feb 2025 00:40:57 +0100
changeset 82142 508a673c87ac
parent 79980 ee04ce2ac13f
permissions -rw-r--r--
removed unused imports;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Tools/scala_build.scala
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     3
75661
2d153e052aea tuned comments;
wenzelm
parents: 75660
diff changeset
     4
Manage and build Isabelle/Scala/Java modules.
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     5
*/
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     6
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     7
package isabelle
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     8
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
     9
74061
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    10
import java.io.{ByteArrayOutputStream, PrintStream}
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
    11
import java.nio.file.{Path => JPath}
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    12
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    13
import scala.jdk.CollectionConverters._
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    14
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    15
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    16
object Scala_Build {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    17
  class Context private[Scala_Build](java_context: isabelle.setup.Build.Context) {
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    18
    override def toString: String = java_context.toString
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    19
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    20
    def is_module(path: Path): Boolean = {
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    21
      val module_name = java_context.module_name()
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    22
      module_name.nonEmpty && File.eq(java_context.path(module_name).toFile, path.file)
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    23
    }
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    24
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    25
    def module_result: Option[Path] = {
74062
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    26
      java_context.module_result() match {
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    27
        case "" => None
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    28
        case module => Some(File.path(java_context.path(module).toFile))
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    29
      }
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    30
    }
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    31
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    32
    def sources: List[Path] =
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    33
      java_context.sources().asScala.toList.map(s => File.path(java_context.path(s).toFile))
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    34
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    35
    def requirements: List[Path] =
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    36
      (for {
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    37
        s <- java_context.requirements().asScala.iterator
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    38
        p <- java_context.requirement_paths(s).asScala.iterator
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    39
      } yield (File.path(p.toFile))).toList
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    40
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
    41
    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
    42
      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
    43
      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
    44
    ): 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
    45
      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
    46
      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
    47
74061
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    48
      val output0 = new ByteArrayOutputStream
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    49
      val output = new PrintStream(output0)
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    50
      def get_output(): String = {
74061
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    51
        output.flush()
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    52
        Library.trim_line(output0.toString(UTF8.charset))
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    53
      }
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
    54
74061
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    55
      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
    56
        isabelle.setup.Build.build(java_classpath, output, java_context, fresh)
74061
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    57
        get_output()
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    58
      }
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    59
      catch { case ERROR(msg) => cat_error(get_output(), msg) }
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    60
    }
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    61
  }
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    62
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    63
  def context(dir: Path,
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    64
    component: Boolean = false,
74060
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    65
    no_title: Boolean = false,
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    66
    do_build: Boolean = false,
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    67
    module: Option[Path] = None
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    68
  ): Context = {
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    69
    val props_name =
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    70
      if (component) isabelle.setup.Build.COMPONENT_BUILD_PROPS
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    71
      else isabelle.setup.Build.BUILD_PROPS
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    72
    val props_path = dir + Path.explode(props_name)
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    73
79980
ee04ce2ac13f clarified signature;
wenzelm
parents: 77027
diff changeset
    74
    val props = File.read_props(props_path)
74060
8cd746a5c291 clarified signature: more operations;
wenzelm
parents: 74057
diff changeset
    75
    if (no_title) props.remove(isabelle.setup.Build.TITLE)
74057
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    76
    if (do_build) props.remove(isabelle.setup.Build.NO_BUILD)
22ad3ac2152c clarified properties: "module" and "no_build";
wenzelm
parents: 74056
diff changeset
    77
    if (module.isDefined) props.put(isabelle.setup.Build.MODULE, File.standard_path(module.get))
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    78
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
    79
    new Context(new isabelle.setup.Build.Context(dir.java_path, props, props_path.implode))
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    80
  }
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
    81
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    82
  sealed case class Result(output: String, jar_bytes: Bytes, jar_path: Option[Path]) {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    83
    def write(): Unit = {
74062
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    84
      if (jar_path.isDefined) {
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    85
        Isabelle_System.make_directory(jar_path.get.dir)
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    86
        Bytes.write(jar_path.get, jar_bytes)
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    87
      }
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    88
    }
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    89
  }
74061
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    90
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 74062
diff changeset
    91
  def build_result(dir: Path, component: Boolean = false): Result = {
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    92
    Isabelle_System.with_tmp_file("result", "jar") { tmp_file =>
74061
203dfa8bc0fc clarified compiler output: allow multithreaded execution;
wenzelm
parents: 74060
diff changeset
    93
      val output =
75657
900b76040211 clarified signature;
wenzelm
parents: 75654
diff changeset
    94
        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
    95
          module = Some(tmp_file)).build(classpath = Classpath().jars.map(File.path))
74062
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    96
      val jar_bytes = Bytes.read(tmp_file)
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    97
      val jar_path = context(dir, component = component).module_result
4dbac13d89a5 clarified signature;
wenzelm
parents: 74061
diff changeset
    98
      Result(output, jar_bytes, jar_path)
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    99
    }
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
   100
  }
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
   101
75660
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   102
  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
   103
    val here = Scala_Project.here
77027
ac7af931189f support Session argument for Scala.Fun;
wenzelm
parents: 75869
diff changeset
   104
    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
   105
      args match {
75687
c8dc5d1adc7b removed obsolete commands;
wenzelm
parents: 75678
diff changeset
   106
        case List(dir) =>
c8dc5d1adc7b removed obsolete commands;
wenzelm
parents: 75678
diff changeset
   107
          val result = build_result(Path.explode(dir.text))
75660
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   108
          val jar_name =
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   109
            result.jar_path match {
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   110
              case Some(path) => path.file_name
75678
58b161746645 clarified names;
wenzelm
parents: 75661
diff changeset
   111
              case None => "scala_build.jar"
75660
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   112
            }
75678
58b161746645 clarified names;
wenzelm
parents: 75661
diff changeset
   113
          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
   114
        case _ => error("Bad arguments")
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   115
      }
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   116
  }
45d3497c0baa support for Isabelle/Scala/Java modules in Isabelle/ML;
wenzelm
parents: 75657
diff changeset
   117
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
   118
  def component_contexts(): List[Context] =
74056
fb8d5c0133c9 clarified signature;
wenzelm
parents: 74055
diff changeset
   119
    isabelle.setup.Build.component_contexts().asScala.toList.map(new Context(_))
74055
0ee44ed80290 clarified signature;
wenzelm
parents:
diff changeset
   120
}