uniform heap_scale;
authorwenzelm
Thu May 18 14:38:09 2017 +0200 (2017-05-18)
changeset 6586600e8b836d4db
parent 65865 177b90f33f40
child 65867 53613acb76e7
uniform heap_scale;
tuned;
src/Pure/Admin/build_status.scala
src/Pure/ML/ml_statistics.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Thu May 18 14:14:20 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Thu May 18 14:38:09 2017 +0200
     1.3 @@ -80,7 +80,7 @@
     1.4        entries.forall(entry =>
     1.5          entry.maximum_heap > 0 ||
     1.6          entry.average_heap > 0 ||
     1.7 -        entry.final_heap > 0)
     1.8 +        entry.stored_heap > 0)
     1.9    }
    1.10    sealed case class Entry(
    1.11      pull_date: Date,
    1.12 @@ -90,7 +90,7 @@
    1.13      ml_timing: Timing,
    1.14      maximum_heap: Long,
    1.15      average_heap: Long,
    1.16 -    final_heap: Long)
    1.17 +    stored_heap: Long)
    1.18  
    1.19    sealed case class Image(name: String, width: Int, height: Int)
    1.20    {
    1.21 @@ -174,7 +174,7 @@
    1.22                ML_Statistics(
    1.23                  if (ml_statistics)
    1.24                    Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics))
    1.25 -                else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")")
    1.26 +                else Nil, heading = session_name + " (Isabelle/" + isabelle_version + ")")
    1.27  
    1.28              val entry =
    1.29                Entry(
    1.30 @@ -193,7 +193,7 @@
    1.31                      Build_Log.Data.ml_timing_gc),
    1.32                  maximum_heap = ml_stats.maximum_heap_size,
    1.33                  average_heap = ml_stats.average_heap_size,
    1.34 -                final_heap = res.long(Build_Log.Data.heap_size))
    1.35 +                stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)))
    1.36  
    1.37              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.38              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.39 @@ -229,13 +229,8 @@
    1.40      def clean_name(name: String): String =
    1.41        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.42  
    1.43 -    def heap_scale(x: Long): Long = x / 1024 / 1024
    1.44 -
    1.45      def print_heap(x: Long): Option[String] =
    1.46 -    {
    1.47 -      val y = heap_scale(x)
    1.48 -      if (y == 0L) None else Some(y.toString + " M")
    1.49 -    }
    1.50 +      if (x == 0L) None else Some(x.toString + " M")
    1.51  
    1.52      HTML.write_document(target_dir, "index.html",
    1.53        List(HTML.title("Isabelle build status")),
    1.54 @@ -274,9 +269,9 @@
    1.55                        entry.timing.resources.minutes,
    1.56                        entry.ml_timing.elapsed.minutes,
    1.57                        entry.ml_timing.resources.minutes,
    1.58 -                      heap_scale(entry.maximum_heap),
    1.59 -                      heap_scale(entry.average_heap),
    1.60 -                      heap_scale(entry.final_heap)).mkString(" "))))
    1.61 +                      entry.maximum_heap,
    1.62 +                      entry.average_heap,
    1.63 +                      entry.stored_heap).mkString(" "))))
    1.64  
    1.65                val max_time =
    1.66                  ((0.0 /: session.entries){ case (m, entry) =>
    1.67 @@ -394,8 +389,8 @@
    1.68                    HTML.text("maximum heap:") -> HTML.text(s)).toList :::
    1.69                  print_heap(session.head.average_heap).map(s =>
    1.70                    HTML.text("average heap:") -> HTML.text(s)).toList :::
    1.71 -                print_heap(session.head.final_heap).map(s =>
    1.72 -                  HTML.text("final heap:") -> HTML.text(s)).toList :::
    1.73 +                print_heap(session.head.stored_heap).map(s =>
    1.74 +                  HTML.text("stored heap:") -> HTML.text(s)).toList :::
    1.75                  proper_string(session.head.isabelle_version).map(s =>
    1.76                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.77                  proper_string(session.head.afp_version).map(s =>
     2.1 --- a/src/Pure/ML/ml_statistics.scala	Thu May 18 14:14:20 2017 +0200
     2.2 +++ b/src/Pure/ML/ml_statistics.scala	Thu May 18 14:38:09 2017 +0200
     2.3 @@ -25,10 +25,16 @@
     2.4    def now(props: Properties.T): Double = Now.unapply(props).get
     2.5  
     2.6  
     2.7 -  /* standard fields */
     2.8 +  /* heap */
     2.9  
    2.10    val HEAP_SIZE = "size_heap"
    2.11  
    2.12 +  def heap_scale(x: Long): Long = x / 1024 / 1024
    2.13 +  def heap_scale(x: Double): Double = heap_scale(x.toLong).toLong
    2.14 +
    2.15 +
    2.16 +  /* standard fields */
    2.17 +
    2.18    type Fields = (String, List[String])
    2.19  
    2.20    val tasks_fields: Fields =
    2.21 @@ -109,7 +115,11 @@
    2.22          val data =
    2.23            SortedMap.empty[String, Double] ++ speeds ++
    2.24              (for ((x, y) <- props.iterator if x != Now.name)
    2.25 -              yield (x.intern, java.lang.Double.parseDouble(y)))
    2.26 +             yield {
    2.27 +               val z = java.lang.Double.parseDouble(y)
    2.28 +              (x.intern, if (heap_fields._2.contains(x)) heap_scale(z) else z)
    2.29 +            })
    2.30 +
    2.31          result += ML_Statistics.Entry(time, data)
    2.32        }
    2.33        result.toList