src/Pure/Admin/build_status.scala
changeset 65769 490b7c517000
parent 65766 2edb89630a80
child 65773 120ef768c84c
     1.1 --- a/src/Pure/Admin/build_status.scala	Mon May 08 11:00:20 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Mon May 08 11:33:04 2017 +0200
     1.3 @@ -48,9 +48,11 @@
     1.4      def timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.timing
     1.5      def ml_timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.ml_timing
     1.6      def order: Long = - timing.elapsed.ms
     1.7 -    def check: Boolean = entries.length >= 3
     1.8 +
     1.9 +    def check_timing: Boolean = entries.length >= 3
    1.10 +    def check_heap: Boolean = entries.forall(_.heap_size > 0)
    1.11    }
    1.12 -  sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
    1.13 +  sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing, heap_size: Long)
    1.14  
    1.15  
    1.16    /* read data */
    1.17 @@ -82,7 +84,8 @@
    1.18              Build_Log.Data.timing_gc,
    1.19              Build_Log.Data.ml_timing_elapsed,
    1.20              Build_Log.Data.ml_timing_cpu,
    1.21 -            Build_Log.Data.ml_timing_gc)
    1.22 +            Build_Log.Data.ml_timing_gc,
    1.23 +            Build_Log.Data.heap_size)
    1.24  
    1.25          val Threads_Option = """threads\s*=\s*(\d+)""".r
    1.26  
    1.27 @@ -119,7 +122,8 @@
    1.28                  res.timing(
    1.29                    Build_Log.Data.ml_timing_elapsed,
    1.30                    Build_Log.Data.ml_timing_cpu,
    1.31 -                  Build_Log.Data.ml_timing_gc))
    1.32 +                  Build_Log.Data.ml_timing_gc),
    1.33 +                heap_size = res.long(Build_Log.Data.heap_size))
    1.34  
    1.35              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.36              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.37 @@ -133,7 +137,8 @@
    1.38      Data(date,
    1.39        (for {
    1.40          (data_name, sessions) <- data_entries.toList
    1.41 -        sorted_sessions <- proper_list(sessions.toList.map(_._2).filter(_.check).sortBy(_.order))
    1.42 +        sorted_sessions <-
    1.43 +          proper_list(sessions.toList.map(_._2).filter(_.check_timing).sortBy(_.order))
    1.44        } yield (data_name, sorted_sessions)).sortBy(_._1))
    1.45    }
    1.46  
    1.47 @@ -163,7 +168,8 @@
    1.48                        entry.timing.elapsed.minutes,
    1.49                        entry.timing.resources.minutes,
    1.50                        entry.ml_timing.elapsed.minutes,
    1.51 -                      entry.ml_timing.resources.minutes).mkString(" "))))
    1.52 +                      entry.ml_timing.resources.minutes,
    1.53 +                      (entry.heap_size.toDouble / (1024 * 1024)).toString).mkString(" "))))
    1.54  
    1.55                val max_time =
    1.56                  ((0.0 /: session.entries){ case (m, entry) =>
    1.57 @@ -171,8 +177,9 @@
    1.58                      max(entry.timing.resources.minutes).
    1.59                      max(entry.ml_timing.elapsed.minutes).
    1.60                      max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
    1.61 +              val timing_range = "[0:" + max_time + "]"
    1.62  
    1.63 -              def gnuplot(plots: List[String], kind: String): String =
    1.64 +              def gnuplot(plots: List[String], kind: String, range: String): String =
    1.65                {
    1.66                  val plot_name = session.name + "_" + kind + ".png"
    1.67  
    1.68 @@ -184,8 +191,8 @@
    1.69  set format x "%d-%b"
    1.70  set xlabel """ + quote(session.name) + """ noenhanced
    1.71  set key left bottom
    1.72 -plot [] [0:""" + max_time + "] " +
    1.73 -                  plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
    1.74 +plot [] """ + range + " " +
    1.75 +                plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
    1.76  
    1.77                  val result =
    1.78                    Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
    1.79 @@ -195,17 +202,18 @@
    1.80                  plot_name
    1.81                }
    1.82  
    1.83 -              val timing_plots1 =
    1.84 -                List(
    1.85 -                  """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    1.86 -                  """ using 1:2 smooth csplines title "elapsed time" """)
    1.87 -              val timing_plots2 =
    1.88 -                List(
    1.89 -                  """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
    1.90 -                  """ using 1:3 smooth csplines title "cpu time" """)
    1.91                val timing_plots =
    1.92 -                if (session.threads == 1) timing_plots1
    1.93 -                else timing_plots1 ::: timing_plots2
    1.94 +              {
    1.95 +                val plots1 =
    1.96 +                  List(
    1.97 +                    """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    1.98 +                    """ using 1:2 smooth csplines title "elapsed time" """)
    1.99 +                val plots2 =
   1.100 +                  List(
   1.101 +                    """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   1.102 +                    """ using 1:3 smooth csplines title "cpu time" """)
   1.103 +                if (session.threads == 1) plots1 else plots1 ::: plots2
   1.104 +              }
   1.105  
   1.106                val ml_timing_plots =
   1.107                  List(
   1.108 @@ -214,8 +222,18 @@
   1.109                    """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   1.110                    """ using 1:5 smooth csplines title "ML cpu time" """)
   1.111  
   1.112 -              session.name ->
   1.113 -                List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
   1.114 +              val heap_plots =
   1.115 +                List(
   1.116 +                  """ using 1:6 smooth sbezier title "heap (smooth)" """,
   1.117 +                  """ using 1:6 smooth csplines title "heap" """)
   1.118 +
   1.119 +              val plot_names =
   1.120 +                List(
   1.121 +                  gnuplot(timing_plots, "timing", timing_range),
   1.122 +                  gnuplot(ml_timing_plots, "ml_timing", timing_range)) :::
   1.123 +                (if (session.check_heap) List(gnuplot(heap_plots, "heap", "[0:]")) else Nil)
   1.124 +
   1.125 +              session.name -> plot_names
   1.126              }
   1.127            }, sessions).toMap
   1.128