store errors in build db;
authorwenzelm
Fri May 26 15:19:21 2017 +0200 (2017-05-26)
changeset 659345f202ba9f590
parent 65933 f3e4f9e6c485
child 65935 73c099fa96a4
store errors in build db;
src/Pure/Admin/build_log.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.ML
src/Pure/library.ML
     1.1 --- a/src/Pure/Admin/build_log.scala	Fri May 26 11:51:45 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Fri May 26 15:19:21 2017 +0200
     1.3 @@ -258,12 +258,11 @@
     1.4      def parse_props(text: String): Properties.T =
     1.5        xml_cache.props(Properties.decode_lines(XML.Decode.properties(YXML.parse_body(text))))
     1.6  
     1.7 +    def filter_lines(marker: String): List[String] =
     1.8 +      for (line <- lines; s <- Library.try_unprefix(marker, line)) yield s
     1.9 +
    1.10      def filter_props(marker: String): List[Properties.T] =
    1.11 -      for {
    1.12 -        line <- lines
    1.13 -        s <- Library.try_unprefix(marker, line)
    1.14 -        if YXML.detect(s)
    1.15 -      } yield parse_props(s)
    1.16 +      for (s <- filter_lines(marker) if YXML.detect(s)) yield parse_props(s)
    1.17  
    1.18      def find_props(marker: String): Option[Properties.T] =
    1.19        find_line(marker) match {
    1.20 @@ -599,7 +598,8 @@
    1.21      session_timing: Properties.T,
    1.22      command_timings: List[Properties.T],
    1.23      ml_statistics: List[Properties.T],
    1.24 -    task_statistics: List[Properties.T])
    1.25 +    task_statistics: List[Properties.T],
    1.26 +    errors: List[String])
    1.27  
    1.28    private def parse_session_info(
    1.29      log_file: Log_File,
    1.30 @@ -611,7 +611,8 @@
    1.31        session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
    1.32        command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
    1.33        ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
    1.34 -      task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil)
    1.35 +      task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil,
    1.36 +      errors = log_file.filter_lines("\ferror_message = ").map(Library.decode_lines(_)))
    1.37    }
    1.38  
    1.39  
     2.1 --- a/src/Pure/Thy/sessions.scala	Fri May 26 11:51:45 2017 +0200
     2.2 +++ b/src/Pure/Thy/sessions.scala	Fri May 26 15:19:21 2017 +0200
     2.3 @@ -735,8 +735,9 @@
     2.4      val command_timings = SQL.Column.bytes("command_timings")
     2.5      val ml_statistics = SQL.Column.bytes("ml_statistics")
     2.6      val task_statistics = SQL.Column.bytes("task_statistics")
     2.7 +    val errors = SQL.Column.bytes("errors")
     2.8      val build_log_columns =
     2.9 -      List(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    2.10 +      List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
    2.11  
    2.12      // Build.Session_Info
    2.13      val sources = SQL.Column.string("sources")
    2.14 @@ -814,6 +815,14 @@
    2.15  
    2.16      /* session info */
    2.17  
    2.18 +    def compress_errors(errors: List[String]): Option[Bytes] =
    2.19 +      if (errors.isEmpty) None
    2.20 +      else Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).compress())
    2.21 +
    2.22 +    def uncompress_errors(bytes: Bytes): List[String] =
    2.23 +      if (bytes.isEmpty) Nil
    2.24 +      else XML.Decode.list(YXML.string_of_body(_))(YXML.parse_body(bytes.uncompress().text))
    2.25 +
    2.26      def write_session_info(
    2.27        db: SQL.Database,
    2.28        name: String,
    2.29 @@ -831,10 +840,11 @@
    2.30            stmt.bytes(3) = Properties.compress(build_log.command_timings)
    2.31            stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    2.32            stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    2.33 -          stmt.string(6) = cat_lines(build.sources)
    2.34 -          stmt.string(7) = cat_lines(build.input_heaps)
    2.35 -          stmt.string(8) = build.output_heap getOrElse ""
    2.36 -          stmt.int(9) = build.return_code
    2.37 +          stmt.bytes(6) = compress_errors(build_log.errors)
    2.38 +          stmt.string(7) = cat_lines(build.sources)
    2.39 +          stmt.string(8) = cat_lines(build.input_heaps)
    2.40 +          stmt.string(9) = build.output_heap getOrElse ""
    2.41 +          stmt.int(10) = build.return_code
    2.42            stmt.execute()
    2.43          })
    2.44        }
    2.45 @@ -861,7 +871,8 @@
    2.46          session_timing = read_session_timing(db, name),
    2.47          command_timings = if (command_timings) read_command_timings(db, name) else Nil,
    2.48          ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
    2.49 -        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil)
    2.50 +        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil,
    2.51 +        errors = uncompress_errors(read_bytes(db, name, Session_Info.errors)))
    2.52      }
    2.53  
    2.54      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
     3.1 --- a/src/Pure/Tools/build.ML	Fri May 26 11:51:45 2017 +0200
     3.2 +++ b/src/Pure/Tools/build.ML	Fri May 26 15:19:21 2017 +0200
     3.3 @@ -220,10 +220,12 @@
     3.4      val _ = SHA1.test_samples ();
     3.5      val _ = Options.load_default ();
     3.6      val _ = Isabelle_Process.init_options ();
     3.7 -    val args = decode_args (File.read (Path.explode args_file));
     3.8 +    val args as Args {name, ...} = decode_args (File.read (Path.explode args_file));
     3.9 +    fun error_message msg = writeln ("\ferror_message = " ^ encode_lines msg);
    3.10      val _ =
    3.11        Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
    3.12 -        build_session args;
    3.13 +        build_session args
    3.14 +      handle exn => (List.app (error_message o #2) (Runtime.exn_messages exn); Exn.reraise exn);
    3.15      val _ = Options.reset_default ();
    3.16    in () end;
    3.17  
     4.1 --- a/src/Pure/library.ML	Fri May 26 11:51:45 2017 +0200
     4.2 +++ b/src/Pure/library.ML	Fri May 26 15:19:21 2017 +0200
     4.3 @@ -147,6 +147,8 @@
     4.4    val trim_split_lines: string -> string list
     4.5    val replicate_string: int -> string -> string
     4.6    val translate_string: (string -> string) -> string -> string
     4.7 +  val encode_lines: string -> string
     4.8 +  val decode_lines: string -> string
     4.9    val align_right: string -> int -> string -> string
    4.10    val match_string: string -> string -> bool
    4.11  
    4.12 @@ -729,6 +731,9 @@
    4.13  
    4.14  fun translate_string f = String.translate (f o String.str);
    4.15  
    4.16 +val encode_lines = translate_string (fn "\n" => "\v" | c => c);
    4.17 +val decode_lines = translate_string (fn "\v" => "\n" | c => c);
    4.18 +
    4.19  fun align_right c k s =
    4.20    let
    4.21      val _ = if size c <> 1 orelse size s > k