provide theory timing information, similar to command timing but always considered relevant;
authorwenzelm
Mon Oct 16 14:32:09 2017 +0200 (2017-10-16 ago)
changeset 668739953ae603a23
parent 66872 69afe45a6062
child 66874 0b8da0fc9563
provide theory timing information, similar to command timing but always considered relevant;
src/Pure/Admin/build_log.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/session.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Admin/build_log.scala	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_log.scala	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -283,9 +283,11 @@
     1.4  
     1.5      def parse_session_info(
     1.6          command_timings: Boolean = false,
     1.7 +        theory_timings: Boolean = false,
     1.8          ml_statistics: Boolean = false,
     1.9          task_statistics: Boolean = false): Session_Info =
    1.10 -      Build_Log.parse_session_info(log_file, command_timings, ml_statistics, task_statistics)
    1.11 +      Build_Log.parse_session_info(
    1.12 +        log_file, command_timings, theory_timings, ml_statistics, task_statistics)
    1.13    }
    1.14  
    1.15  
    1.16 @@ -446,6 +448,7 @@
    1.17  
    1.18    /** build info: toplevel output of isabelle build or Admin/build_history **/
    1.19  
    1.20 +  val THEORY_TIMING_MARKER = "\ftheory_timing = "
    1.21    val ML_STATISTICS_MARKER = "\fML_statistics = "
    1.22    val ERROR_MESSAGE_MARKER = "\ferror_message = "
    1.23    val SESSION_NAME = "session_name"
    1.24 @@ -612,6 +615,7 @@
    1.25    sealed case class Session_Info(
    1.26      session_timing: Properties.T,
    1.27      command_timings: List[Properties.T],
    1.28 +    theory_timings: List[Properties.T],
    1.29      ml_statistics: List[Properties.T],
    1.30      task_statistics: List[Properties.T],
    1.31      errors: List[String])
    1.32 @@ -619,12 +623,14 @@
    1.33    private def parse_session_info(
    1.34      log_file: Log_File,
    1.35      command_timings: Boolean,
    1.36 +    theory_timings: Boolean,
    1.37      ml_statistics: Boolean,
    1.38      task_statistics: Boolean): Session_Info =
    1.39    {
    1.40      Session_Info(
    1.41        session_timing = log_file.find_props("\fTiming = ") getOrElse Nil,
    1.42        command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil,
    1.43 +      theory_timings = if (theory_timings) log_file.filter_props(THEORY_TIMING_MARKER) else Nil,
    1.44        ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil,
    1.45        task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil,
    1.46        errors = log_file.filter_lines(ERROR_MESSAGE_MARKER).map(Library.decode_lines(_)))
     2.1 --- a/src/Pure/PIDE/markup.ML	Mon Oct 16 14:21:14 2017 +0200
     2.2 +++ b/src/Pure/PIDE/markup.ML	Mon Oct 16 14:32:09 2017 +0200
     2.3 @@ -194,6 +194,7 @@
     2.4    val ML_statistics: Properties.entry
     2.5    val task_statistics: Properties.entry
     2.6    val command_timing: Properties.entry
     2.7 +  val theory_timing: Properties.entry
     2.8    val loading_theory: string -> Properties.T
     2.9    val dest_loading_theory: Properties.T -> string option
    2.10    val build_session_finished: Properties.T
    2.11 @@ -619,6 +620,8 @@
    2.12  
    2.13  val command_timing = (functionN, "command_timing");
    2.14  
    2.15 +val theory_timing = (functionN, "theory_timing");
    2.16 +
    2.17  fun loading_theory name = [("function", "loading_theory"), ("name", name)];
    2.18  
    2.19  fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
     3.1 --- a/src/Pure/PIDE/markup.scala	Mon Oct 16 14:21:14 2017 +0200
     3.2 +++ b/src/Pure/PIDE/markup.scala	Mon Oct 16 14:32:09 2017 +0200
     3.3 @@ -392,9 +392,11 @@
     3.4    }
     3.5  
     3.6  
     3.7 -  /* command timing */
     3.8 +  /* protocol functions */
     3.9  
    3.10 -  val COMMAND_TIMING = "command_timing"
    3.11 +  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
    3.12 +
    3.13 +  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
    3.14  
    3.15  
    3.16    /* command indentation */
     4.1 --- a/src/Pure/PIDE/protocol.scala	Mon Oct 16 14:21:14 2017 +0200
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Oct 16 14:32:09 2017 +0200
     4.3 @@ -113,7 +113,7 @@
     4.4    {
     4.5      def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] =
     4.6        props match {
     4.7 -        case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args =>
     4.8 +        case Markup.COMMAND_TIMING :: args =>
     4.9            (args, args) match {
    4.10              case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing))
    4.11              case _ => None
    4.12 @@ -123,6 +123,22 @@
    4.13    }
    4.14  
    4.15  
    4.16 +  /* theory timing */
    4.17 +
    4.18 +  object Theory_Timing
    4.19 +  {
    4.20 +    def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
    4.21 +      props match {
    4.22 +        case Markup.THEORY_TIMING :: args =>
    4.23 +          (args, args) match {
    4.24 +            case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
    4.25 +            case _ => None
    4.26 +          }
    4.27 +        case _ => None
    4.28 +      }
    4.29 +  }
    4.30 +
    4.31 +
    4.32    /* node status */
    4.33  
    4.34    sealed case class Node_Status(
     5.1 --- a/src/Pure/PIDE/session.scala	Mon Oct 16 14:21:14 2017 +0200
     5.2 +++ b/src/Pure/PIDE/session.scala	Mon Oct 16 14:32:09 2017 +0200
     5.3 @@ -432,6 +432,9 @@
     5.4                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
     5.5                  accumulate(state_id, xml_cache.elem(message))
     5.6  
     5.7 +              case Protocol.Theory_Timing(_, _) =>
     5.8 +                // FIXME
     5.9 +
    5.10                case Markup.Assign_Update =>
    5.11                  msg.text match {
    5.12                    case Protocol.Assign_Update(id, update) =>
     6.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 16 14:21:14 2017 +0200
     6.2 +++ b/src/Pure/Thy/sessions.scala	Mon Oct 16 14:32:09 2017 +0200
     6.3 @@ -829,11 +829,13 @@
     6.4      // Build_Log.Session_Info
     6.5      val session_timing = SQL.Column.bytes("session_timing")
     6.6      val command_timings = SQL.Column.bytes("command_timings")
     6.7 +    val theory_timings = SQL.Column.bytes("theory_timings")
     6.8      val ml_statistics = SQL.Column.bytes("ml_statistics")
     6.9      val task_statistics = SQL.Column.bytes("task_statistics")
    6.10      val errors = SQL.Column.bytes("errors")
    6.11      val build_log_columns =
    6.12 -      List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors)
    6.13 +      List(session_name, session_timing, command_timings, theory_timings,
    6.14 +        ml_statistics, task_statistics, errors)
    6.15  
    6.16      // Build.Session_Info
    6.17      val sources = SQL.Column.string("sources")
    6.18 @@ -926,13 +928,14 @@
    6.19            stmt.string(1) = name
    6.20            stmt.bytes(2) = Properties.encode(build_log.session_timing)
    6.21            stmt.bytes(3) = Properties.compress(build_log.command_timings)
    6.22 -          stmt.bytes(4) = Properties.compress(build_log.ml_statistics)
    6.23 -          stmt.bytes(5) = Properties.compress(build_log.task_statistics)
    6.24 -          stmt.bytes(6) = Build_Log.compress_errors(build_log.errors)
    6.25 -          stmt.string(7) = build.sources
    6.26 -          stmt.string(8) = cat_lines(build.input_heaps)
    6.27 -          stmt.string(9) = build.output_heap getOrElse ""
    6.28 -          stmt.int(10) = build.return_code
    6.29 +          stmt.bytes(4) = Properties.compress(build_log.theory_timings)
    6.30 +          stmt.bytes(5) = Properties.compress(build_log.ml_statistics)
    6.31 +          stmt.bytes(6) = Properties.compress(build_log.task_statistics)
    6.32 +          stmt.bytes(7) = Build_Log.compress_errors(build_log.errors)
    6.33 +          stmt.string(8) = build.sources
    6.34 +          stmt.string(9) = cat_lines(build.input_heaps)
    6.35 +          stmt.string(10) = build.output_heap getOrElse ""
    6.36 +          stmt.int(11) = build.return_code
    6.37            stmt.execute()
    6.38          })
    6.39        }
    6.40 @@ -944,6 +947,9 @@
    6.41      def read_command_timings(db: SQL.Database, name: String): List[Properties.T] =
    6.42        read_properties(db, name, Session_Info.command_timings)
    6.43  
    6.44 +    def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] =
    6.45 +      read_properties(db, name, Session_Info.theory_timings)
    6.46 +
    6.47      def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] =
    6.48        read_properties(db, name, Session_Info.ml_statistics)
    6.49  
     7.1 --- a/src/Pure/Thy/thy_info.ML	Mon Oct 16 14:21:14 2017 +0200
     7.2 +++ b/src/Pure/Thy/thy_info.ML	Mon Oct 16 14:32:09 2017 +0200
     7.3 @@ -301,10 +301,17 @@
     7.4        Execution.running Document_ID.none exec_id [] orelse
     7.5          raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id);
     7.6  
     7.7 +    val timing_start = Timing.start ();
     7.8 +
     7.9      val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path);
    7.10      val (theory, present, weight) =
    7.11        eval_thy document symbols last_timing update_time dir header text_pos text
    7.12          (if name = Context.PureN then [Context.the_global_context ()] else parents);
    7.13 +
    7.14 +    val timing_result = Timing.result timing_start;
    7.15 +    val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
    7.16 +    val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
    7.17 +
    7.18      fun commit () = update_thy deps theory;
    7.19    in
    7.20      Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight}
     8.1 --- a/src/Pure/Tools/build.ML	Mon Oct 16 14:21:14 2017 +0200
     8.2 +++ b/src/Pure/Tools/build.ML	Mon Oct 16 14:32:09 2017 +0200
     8.3 @@ -92,6 +92,8 @@
     8.4              | NONE => ())
     8.5            else ()
     8.6          end
     8.7 +      else if function = Markup.theory_timing then
     8.8 +        inline_message (#2 function) args
     8.9        else
    8.10          (case Markup.dest_loading_theory props of
    8.11            SOME name => writeln ("\floading_theory = " ^ name)
     9.1 --- a/src/Pure/Tools/build.scala	Mon Oct 16 14:21:14 2017 +0200
     9.2 +++ b/src/Pure/Tools/build.scala	Mon Oct 16 14:32:09 2017 +0200
     9.3 @@ -537,7 +537,10 @@
     9.4                    build_log =
     9.5                      Build_Log.Log_File(name, process_result.out_lines).
     9.6                        parse_session_info(
     9.7 -                        command_timings = true, ml_statistics = true, task_statistics = true),
     9.8 +                        command_timings = true,
     9.9 +                        theory_timings = true,
    9.10 +                        ml_statistics = true,
    9.11 +                        task_statistics = true),
    9.12                    build =
    9.13                      Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
    9.14                        process_result.rc)))