clarified compiler output: allow multithreaded execution;
authorwenzelm
Sat, 24 Jul 2021 19:55:10 +0200
changeset 74061 203dfa8bc0fc
parent 74060 8cd746a5c291
child 74062 4dbac13d89a5
clarified compiler output: allow multithreaded execution;
Admin/components/components.sha1
Admin/components/main
src/Pure/Tools/scala_build.scala
src/Tools/Setup/src/Build.java
src/Tools/Setup/src/Setup.java
--- a/Admin/components/components.sha1	Sat Jul 24 18:07:07 2021 +0200
+++ b/Admin/components/components.sha1	Sat Jul 24 19:55:10 2021 +0200
@@ -133,6 +133,7 @@
 14f8508bcae9140815bb23e430e26d2cbc504b81  isabelle_setup-20210717.tar.gz
 ca801d5c380ea896ee32b309ff19ae5f34538963  isabelle_setup-20210718.tar.gz
 ac9739e38e4fbbfce1a71a0987a57b22f83922d3  isabelle_setup-20210724-1.tar.gz
+4554679cc8ea31e539655810a14d14216b383d0e  isabelle_setup-20210724-2.tar.gz
 127a75ae33e97480d352087fcb9b47a632d77169  isabelle_setup-20210724.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56  jdk-11.0.10+9.tar.gz
--- a/Admin/components/main	Sat Jul 24 18:07:07 2021 +0200
+++ b/Admin/components/main	Sat Jul 24 19:55:10 2021 +0200
@@ -8,7 +8,7 @@
 flatlaf-1.2
 idea-icons-20210508
 isabelle_fonts-20210322
-isabelle_setup-20210724-1
+isabelle_setup-20210724-2
 jdk-15.0.2+7
 jedit-20210724
 jfreechart-1.5.1
--- a/src/Pure/Tools/scala_build.scala	Sat Jul 24 18:07:07 2021 +0200
+++ b/src/Pure/Tools/scala_build.scala	Sat Jul 24 19:55:10 2021 +0200
@@ -8,6 +8,7 @@
 
 
 import java.util.{Properties => JProperties}
+import java.io.{ByteArrayOutputStream, PrintStream}
 import java.nio.file.Files
 
 import scala.jdk.CollectionConverters._
@@ -34,8 +35,25 @@
         p <- java_context.requirement_paths(s).asScala.iterator
       } yield (File.path(p.toFile))).toList
 
-    def build(fresh: Boolean = false): Unit =
-      isabelle.setup.Build.build(java_context, fresh)
+    def build(fresh: Boolean = false): String =
+    {
+      val output0 = new ByteArrayOutputStream
+      val output = new PrintStream(output0)
+      def get_output(): String =
+      {
+        output.flush()
+        Library.trim_line(output0.toString(UTF8.charset))
+      }
+      try {
+        Console.withOut(output) {
+          Console.withErr(output) {
+            isabelle.setup.Build.build(output, java_context, fresh)
+          }
+        }
+        get_output()
+      }
+      catch { case ERROR(msg) => cat_error(get_output(), msg) }
+    }
   }
 
   def context(dir: Path,
@@ -63,18 +81,22 @@
     component: Boolean = false,
     no_title: Boolean = false,
     do_build: Boolean = false,
-    module: Option[Path] = None): Unit =
+    module: Option[Path] = None): String =
   {
     context(dir, component = component, no_title = no_title, do_build = do_build, module = module)
       .build(fresh = fresh)
   }
 
-  def build_result(dir: Path, component: Boolean = false): Bytes =
+  sealed case class Result(output: String, jar: Bytes)
+
+  def build_result(dir: Path, component: Boolean = false): Result =
   {
     Isabelle_System.with_tmp_file("result", "jar")(tmp_file =>
     {
-      build(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file))
-      Bytes.read(tmp_file)
+      val output =
+        build(dir, component = component, no_title = true, do_build = true, module = Some(tmp_file))
+      val jar = Bytes.read(tmp_file)
+      Result(output, jar)
     })
   }
 
--- a/src/Tools/Setup/src/Build.java	Sat Jul 24 18:07:07 2021 +0200
+++ b/src/Tools/Setup/src/Build.java	Sat Jul 24 19:55:10 2021 +0200
@@ -8,12 +8,10 @@
 
 
 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;
@@ -234,18 +232,12 @@
         }
     }
 
-    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<Path> deps, List<Path> sources)
-        throws IOException, InterruptedException
+        PrintStream output,  // ignored, but see scala.Console.withOut/withErr
+        Path target_dir,
+        String more_options,
+        List<Path> deps,
+        List<Path> sources) throws IOException, InterruptedException
     {
         ArrayList<String> args = new ArrayList<String>();
         add_options(args, Environment.getenv("ISABELLE_SCALAC_OPTIONS"));
@@ -262,34 +254,17 @@
             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");
+            boolean ok = new MainClass().process(args.toArray(String[]::new));
+            if (!ok) { throw new RuntimeException("Failed to compiler Scala sources"); }
         }
     }
 
     public static void compile_java_sources(
-        Path target_dir, String more_options, List<Path> deps, List<Path> sources)
-        throws IOException, InterruptedException
+        PrintStream output,
+        Path target_dir,
+        String more_options,
+        List<Path> deps,
+        List<Path> sources) throws IOException, InterruptedException
     {
         JavaCompiler compiler = ToolProvider.getSystemJavaCompiler();
         StandardJavaFileManager file_manager =
@@ -316,7 +291,13 @@
             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");
+
+            String msg = Library.trim_line(out.toString());
+            if (ok) { if (!msg.isEmpty()) { output.print(msg + "\n"); } }
+            else {
+                throw new RuntimeException(
+                    (msg.isEmpty() ? "" : msg + "\n") + "Failed to compile Java sources");
+            }
         }
     }
 
@@ -446,7 +427,7 @@
 
     /** build **/
 
-    public static void build(Context context, boolean fresh)
+    public static void build(PrintStream output, Context context, boolean fresh)
         throws IOException, InterruptedException, NoSuchAlgorithmException
     {
         String module = context.module_result();
@@ -485,7 +466,7 @@
                 }
                 if (fresh || !shasum_old.equals(shasum)) {
                     if (!title.isEmpty()) {
-                        System.out.print("### Building " + title + " (" + jar_path + ") ...\n");
+                        output.print("### Building " + title + " (" + jar_path + ") ...\n");
                     }
 
                     String isabelle_classpath = Environment.getenv("ISABELLE_CLASSPATH");
@@ -503,12 +484,12 @@
                         List<Path> compiler_sources = new LinkedList<Path>();
                         for (String s : sources) { compiler_sources.add(context.path(s)); }
 
-                        compile_scala_sources(
-                            build_dir, context.scalac_options(), compiler_deps, compiler_sources);
+                        compile_scala_sources(output, 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);
+                        compile_java_sources(output, build_dir,
+                            context.javac_options(), compiler_deps, compiler_sources);
 
 
                         /* copy resources */
@@ -555,11 +536,11 @@
         }
     }
 
-    public static void build_components(boolean fresh)
+    public static void build_components(PrintStream output, boolean fresh)
         throws IOException, InterruptedException, NoSuchAlgorithmException
     {
         for (Context context : component_contexts()) {
-            build(context, fresh);
+            build(output, context, fresh);
         }
     }
 }
--- a/src/Tools/Setup/src/Setup.java	Sat Jul 24 18:07:07 2021 +0200
+++ b/src/Tools/Setup/src/Setup.java	Sat Jul 24 19:55:10 2021 +0200
@@ -38,11 +38,11 @@
             switch (op) {
                 case "build":
                     check_args(n == 1);
-                    Build.build_components(false);
+                    Build.build_components(System.err, false);
                     break;
                 case "build_fresh":
                     check_args(n == 1);
-                    Build.build_components(true);
+                    Build.build_components(System.err, true);
                     break;
                 case "classpath":
                     check_args(n == 1);