# HG changeset patch # User wenzelm # Date 1508157129 -7200 # Node ID 9953ae603a234b2923bb30871ffa6c29c2514d12 # Parent 69afe45a6062978755ff78ea468b05e93c519d85 provide theory timing information, similar to command timing but always considered relevant; diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Mon Oct 16 14:32:09 2017 +0200 @@ -283,9 +283,11 @@ def parse_session_info( command_timings: Boolean = false, + theory_timings: Boolean = false, ml_statistics: Boolean = false, task_statistics: Boolean = false): Session_Info = - Build_Log.parse_session_info(log_file, command_timings, ml_statistics, task_statistics) + Build_Log.parse_session_info( + log_file, command_timings, theory_timings, ml_statistics, task_statistics) } @@ -446,6 +448,7 @@ /** build info: toplevel output of isabelle build or Admin/build_history **/ + val THEORY_TIMING_MARKER = "\ftheory_timing = " val ML_STATISTICS_MARKER = "\fML_statistics = " val ERROR_MESSAGE_MARKER = "\ferror_message = " val SESSION_NAME = "session_name" @@ -612,6 +615,7 @@ sealed case class Session_Info( session_timing: Properties.T, command_timings: List[Properties.T], + theory_timings: List[Properties.T], ml_statistics: List[Properties.T], task_statistics: List[Properties.T], errors: List[String]) @@ -619,12 +623,14 @@ private def parse_session_info( log_file: Log_File, command_timings: Boolean, + theory_timings: Boolean, ml_statistics: Boolean, task_statistics: Boolean): Session_Info = { Session_Info( session_timing = log_file.find_props("\fTiming = ") getOrElse Nil, command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil, + theory_timings = if (theory_timings) log_file.filter_props(THEORY_TIMING_MARKER) else Nil, ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil, task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil, errors = log_file.filter_lines(ERROR_MESSAGE_MARKER).map(Library.decode_lines(_))) diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/PIDE/markup.ML Mon Oct 16 14:32:09 2017 +0200 @@ -194,6 +194,7 @@ val ML_statistics: Properties.entry val task_statistics: Properties.entry val command_timing: Properties.entry + val theory_timing: Properties.entry val loading_theory: string -> Properties.T val dest_loading_theory: Properties.T -> string option val build_session_finished: Properties.T @@ -619,6 +620,8 @@ val command_timing = (functionN, "command_timing"); +val theory_timing = (functionN, "theory_timing"); + fun loading_theory name = [("function", "loading_theory"), ("name", name)]; fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/PIDE/markup.scala Mon Oct 16 14:32:09 2017 +0200 @@ -392,9 +392,11 @@ } - /* command timing */ + /* protocol functions */ - val COMMAND_TIMING = "command_timing" + val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing") + + val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing") /* command indentation */ diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/PIDE/protocol.scala Mon Oct 16 14:32:09 2017 +0200 @@ -113,7 +113,7 @@ { def unapply(props: Properties.T): Option[(Document_ID.Generic, isabelle.Timing)] = props match { - case (Markup.FUNCTION, Markup.COMMAND_TIMING) :: args => + case Markup.COMMAND_TIMING :: args => (args, args) match { case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((id, timing)) case _ => None @@ -123,6 +123,22 @@ } + /* theory timing */ + + object Theory_Timing + { + def unapply(props: Properties.T): Option[(String, isabelle.Timing)] = + props match { + case Markup.THEORY_TIMING :: args => + (args, args) match { + case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing)) + case _ => None + } + case _ => None + } + } + + /* node status */ sealed case class Node_Status( diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/PIDE/session.scala Mon Oct 16 14:32:09 2017 +0200 @@ -432,6 +432,9 @@ val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) accumulate(state_id, xml_cache.elem(message)) + case Protocol.Theory_Timing(_, _) => + // FIXME + case Markup.Assign_Update => msg.text match { case Protocol.Assign_Update(id, update) => diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Mon Oct 16 14:32:09 2017 +0200 @@ -829,11 +829,13 @@ // Build_Log.Session_Info val session_timing = SQL.Column.bytes("session_timing") val command_timings = SQL.Column.bytes("command_timings") + val theory_timings = SQL.Column.bytes("theory_timings") val ml_statistics = SQL.Column.bytes("ml_statistics") val task_statistics = SQL.Column.bytes("task_statistics") val errors = SQL.Column.bytes("errors") val build_log_columns = - List(session_name, session_timing, command_timings, ml_statistics, task_statistics, errors) + List(session_name, session_timing, command_timings, theory_timings, + ml_statistics, task_statistics, errors) // Build.Session_Info val sources = SQL.Column.string("sources") @@ -926,13 +928,14 @@ stmt.string(1) = name stmt.bytes(2) = Properties.encode(build_log.session_timing) stmt.bytes(3) = Properties.compress(build_log.command_timings) - stmt.bytes(4) = Properties.compress(build_log.ml_statistics) - stmt.bytes(5) = Properties.compress(build_log.task_statistics) - stmt.bytes(6) = Build_Log.compress_errors(build_log.errors) - stmt.string(7) = build.sources - stmt.string(8) = cat_lines(build.input_heaps) - stmt.string(9) = build.output_heap getOrElse "" - stmt.int(10) = build.return_code + stmt.bytes(4) = Properties.compress(build_log.theory_timings) + stmt.bytes(5) = Properties.compress(build_log.ml_statistics) + stmt.bytes(6) = Properties.compress(build_log.task_statistics) + stmt.bytes(7) = Build_Log.compress_errors(build_log.errors) + stmt.string(8) = build.sources + stmt.string(9) = cat_lines(build.input_heaps) + stmt.string(10) = build.output_heap getOrElse "" + stmt.int(11) = build.return_code stmt.execute() }) } @@ -944,6 +947,9 @@ def read_command_timings(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.command_timings) + def read_theory_timings(db: SQL.Database, name: String): List[Properties.T] = + read_properties(db, name, Session_Info.theory_timings) + def read_ml_statistics(db: SQL.Database, name: String): List[Properties.T] = read_properties(db, name, Session_Info.ml_statistics) diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/Thy/thy_info.ML Mon Oct 16 14:32:09 2017 +0200 @@ -301,10 +301,17 @@ Execution.running Document_ID.none exec_id [] orelse raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); + val timing_start = Timing.start (); + val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); val (theory, present, weight) = eval_thy document symbols last_timing update_time dir header text_pos text (if name = Context.PureN then [Context.the_global_context ()] else parents); + + val timing_result = Timing.result timing_start; + val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; + val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] + fun commit () = update_thy deps theory; in Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/Tools/build.ML Mon Oct 16 14:32:09 2017 +0200 @@ -92,6 +92,8 @@ | NONE => ()) else () end + else if function = Markup.theory_timing then + inline_message (#2 function) args else (case Markup.dest_loading_theory props of SOME name => writeln ("\floading_theory = " ^ name) diff -r 69afe45a6062 -r 9953ae603a23 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/Tools/build.scala Mon Oct 16 14:32:09 2017 +0200 @@ -537,7 +537,10 @@ build_log = Build_Log.Log_File(name, process_result.out_lines). parse_session_info( - command_timings = true, ml_statistics = true, task_statistics = true), + command_timings = true, + theory_timings = true, + ml_statistics = true, + task_statistics = true), build = Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp, process_result.rc)))