more accurate total timing
authorLars Hupel <lars.hupel@mytum.de>
Tue, 05 Jul 2016 10:26:23 +0200
changeset 63387 3395fe5e3893
parent 63386 0d6adf2d5035
child 63388 a095acd4cfbf
more accurate total timing
src/Pure/Tools/ci_profile.scala
--- a/src/Pure/Tools/ci_profile.scala	Tue Jul 05 09:50:20 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Tue Jul 05 10:26:23 2016 +0200
@@ -19,10 +19,11 @@
     println(name + "=" + Outer_Syntax.quote_string(value))
   }
 
-  private def build(options: Options): Build.Results =
+  private def build(options: Options): (Build.Results, Time) =
   {
     val progress = new Console_Progress(true)
-    progress.interrupt_handler {
+    val start_time = Time.now()
+    val results = progress.interrupt_handler {
       Build.build_selection(
         options = options,
         progress = progress,
@@ -34,6 +35,8 @@
         system_mode = true,
         selection = select_sessions _)
     }
+    val end_time = Time.now()
+    (results, end_time - start_time)
   }
 
   private def load_properties(): JProperties =
@@ -85,14 +88,16 @@
     println(s"Build for Isabelle id $isabelle_id")
     pre_hook(args)
 
-    val results = build(options)
+    val (results, elapsed_time) = build(options)
 
     print_section("TIMING")
 
     val groups = results.sessions.map(results.info).flatMap(_.groups)
     for (group <- groups)
       println(s"Group $group: " + compute_timing(results, Some(group)).message_resources)
-    println("Overall: " + compute_timing(results, None).message_resources)
+
+    val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time)
+    println("Overall: " + total_timing.message_resources)
 
     if (!results.ok) {
       print_section("FAILED SESSIONS")