src/Pure/Admin/build_status.scala
changeset 65859 95ddb6dea0d5
parent 65857 5d29d93766ef
child 65860 ce6be2e40d47
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed May 17 22:27:33 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Wed May 17 22:32:48 2017 +0200
     1.3 @@ -81,7 +81,10 @@
     1.4      def check_timing: Boolean = entries.length >= 3
     1.5      def check_heap: Boolean =
     1.6        entries.length >= 3 &&
     1.7 -      entries.forall(entry => entry.heap_size > 0 || entry.heap_size_max > 0)
     1.8 +      entries.forall(entry =>
     1.9 +        entry.maximum_heap > 0 ||
    1.10 +        entry.average_heap > 0 ||
    1.11 +        entry.final_heap > 0)
    1.12    }
    1.13    sealed case class Entry(
    1.14      pull_date: Date,
    1.15 @@ -89,8 +92,9 @@
    1.16      afp_version: String,
    1.17      timing: Timing,
    1.18      ml_timing: Timing,
    1.19 -    heap_size: Long,
    1.20 -    heap_size_max: Long,
    1.21 +    maximum_heap: Long,
    1.22 +    average_heap: Long,
    1.23 +    final_heap: Long,
    1.24      ml_statistics: ML_Statistics)
    1.25  
    1.26    def read_data(options: Options,
    1.27 @@ -187,8 +191,9 @@
    1.28                      Build_Log.Data.ml_timing_elapsed,
    1.29                      Build_Log.Data.ml_timing_cpu,
    1.30                      Build_Log.Data.ml_timing_gc),
    1.31 -                heap_size = res.long(Build_Log.Data.heap_size),
    1.32 -                heap_size_max = ml_stats.heap_size_max,
    1.33 +                maximum_heap = ml_stats.maximum_heap_size,
    1.34 +                average_heap = ml_stats.average_heap_size,
    1.35 +                final_heap = res.long(Build_Log.Data.heap_size),
    1.36                  ml_statistics = ml_stats)
    1.37  
    1.38              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.39 @@ -262,8 +267,9 @@
    1.40                        entry.timing.resources.minutes,
    1.41                        entry.ml_timing.elapsed.minutes,
    1.42                        entry.ml_timing.resources.minutes,
    1.43 -                      heap_scale(entry.heap_size),
    1.44 -                      heap_scale(entry.heap_size_max)).mkString(" "))))
    1.45 +                      heap_scale(entry.maximum_heap),
    1.46 +                      heap_scale(entry.average_heap),
    1.47 +                      heap_scale(entry.final_heap)).mkString(" "))))
    1.48  
    1.49                val max_time =
    1.50                  ((0.0 /: session.entries){ case (m, entry) =>
    1.51 @@ -318,10 +324,12 @@
    1.52  
    1.53                val heap_plots =
    1.54                  List(
    1.55 -                  """ using 1:6 smooth sbezier title "final heap (smooth)" """,
    1.56 -                  """ using 1:6 smooth csplines title "final heap" """,
    1.57 -                  """ using 1:7 smooth sbezier title "max heap (smooth)" """,
    1.58 -                  """ using 1:7 smooth csplines title "max heap" """)
    1.59 +                  """ using 1:6 smooth sbezier title "maximum heap (smooth)" """,
    1.60 +                  """ using 1:6 smooth csplines title "maximum heap" """,
    1.61 +                  """ using 1:7 smooth sbezier title "average heap (smooth)" """,
    1.62 +                  """ using 1:7 smooth csplines title "average heap" """,
    1.63 +                  """ using 1:8 smooth sbezier title "final heap (smooth)" """,
    1.64 +                  """ using 1:8 smooth csplines title "final heap" """)
    1.65  
    1.66                val plot_names =
    1.67                  (if (session.check_timing)