src/Pure/Admin/build_status.scala
changeset 65854 db070951dfee
parent 65849 d70d2d68f7f0
child 65857 5d29d93766ef
     1.1 --- a/src/Pure/Admin/build_status.scala	Wed May 17 13:52:46 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Wed May 17 14:58:48 2017 +0200
     1.3 @@ -50,11 +50,12 @@
     1.4      only_sessions: Set[String] = Set.empty,
     1.5      verbose: Boolean = false,
     1.6      target_dir: Path = default_target_dir,
     1.7 +    ml_statistics: Boolean = false,
     1.8      image_size: (Int, Int) = default_image_size)
     1.9    {
    1.10      val data =
    1.11        read_data(options, progress = progress, profiles = profiles,
    1.12 -        only_sessions = only_sessions, verbose = verbose)
    1.13 +        only_sessions = only_sessions, ml_statistics = ml_statistics, verbose = verbose)
    1.14  
    1.15      present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
    1.16    }
    1.17 @@ -78,15 +79,25 @@
    1.18      def order: Long = - timing.elapsed.ms
    1.19  
    1.20      def check_timing: Boolean = entries.length >= 3
    1.21 -    def check_heap: Boolean = entries.length >= 3 && entries.forall(_.heap_size > 0)
    1.22 +    def check_heap: Boolean =
    1.23 +      entries.length >= 3 &&
    1.24 +      entries.forall(entry => entry.heap_size > 0 || entry.heap_size_max > 0)
    1.25    }
    1.26 -  sealed case class Entry(pull_date: Date, isabelle_version: String, afp_version: String,
    1.27 -    timing: Timing, ml_timing: Timing, heap_size: Long)
    1.28 +  sealed case class Entry(
    1.29 +    pull_date: Date,
    1.30 +    isabelle_version: String,
    1.31 +    afp_version: String,
    1.32 +    timing: Timing,
    1.33 +    ml_timing: Timing,
    1.34 +    heap_size: Long,
    1.35 +    heap_size_max: Long,
    1.36 +    ml_statistics: ML_Statistics)
    1.37  
    1.38    def read_data(options: Options,
    1.39      progress: Progress = No_Progress,
    1.40      profiles: List[Profile] = default_profiles,
    1.41      only_sessions: Set[String] = Set.empty,
    1.42 +    ml_statistics: Boolean = false,
    1.43      verbose: Boolean = false): Data =
    1.44    {
    1.45      val date = Date.now()
    1.46 @@ -102,6 +113,7 @@
    1.47      {
    1.48        for (profile <- profiles.sortBy(_.description)) {
    1.49          progress.echo("input " + quote(profile.description))
    1.50 +
    1.51          val columns =
    1.52            List(
    1.53              Build_Log.Data.pull_date,
    1.54 @@ -118,7 +130,8 @@
    1.55              Build_Log.Data.ml_timing_elapsed,
    1.56              Build_Log.Data.ml_timing_cpu,
    1.57              Build_Log.Data.ml_timing_gc,
    1.58 -            Build_Log.Data.heap_size)
    1.59 +            Build_Log.Data.heap_size) :::
    1.60 +          (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil)
    1.61  
    1.62          val Threads_Option = """threads\s*=\s*(\d+)""".r
    1.63  
    1.64 @@ -151,10 +164,18 @@
    1.65  
    1.66              data_stretch += (data_name -> profile.stretch(options))
    1.67  
    1.68 +            val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
    1.69 +
    1.70 +            val ml_stats =
    1.71 +              ML_Statistics(
    1.72 +                if (ml_statistics)
    1.73 +                    store.uncompress_properties(res.bytes(Build_Log.Data.ml_statistics))
    1.74 +                else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")")
    1.75 +
    1.76              val entry =
    1.77                Entry(
    1.78                  pull_date = res.date(Build_Log.Data.pull_date),
    1.79 -                isabelle_version = res.string(Build_Log.Prop.isabelle_version),
    1.80 +                isabelle_version = isabelle_version,
    1.81                  afp_version = res.string(Build_Log.Prop.afp_version),
    1.82                  timing =
    1.83                    res.timing(
    1.84 @@ -166,7 +187,9 @@
    1.85                      Build_Log.Data.ml_timing_elapsed,
    1.86                      Build_Log.Data.ml_timing_cpu,
    1.87                      Build_Log.Data.ml_timing_gc),
    1.88 -                heap_size = res.long(Build_Log.Data.heap_size))
    1.89 +                heap_size = res.long(Build_Log.Data.heap_size),
    1.90 +                heap_size_max = ml_stats.heap_size_max,
    1.91 +                ml_statistics = ml_stats)
    1.92  
    1.93              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.94              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.95 @@ -202,6 +225,8 @@
    1.96      def clean_name(name: String): String =
    1.97        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.98  
    1.99 +    def heap_scale(x: Long): Double = x.toDouble / (1024 * 1024)
   1.100 +
   1.101      HTML.write_document(target_dir, "index.html",
   1.102        List(HTML.title("Isabelle build status")),
   1.103        List(HTML.chapter("Isabelle build status"),
   1.104 @@ -232,12 +257,13 @@
   1.105                File.write(data_file,
   1.106                  cat_lines(
   1.107                    session.entries.map(entry =>
   1.108 -                    List(entry.pull_date.unix_epoch.toString,
   1.109 +                    List(entry.pull_date.unix_epoch,
   1.110                        entry.timing.elapsed.minutes,
   1.111                        entry.timing.resources.minutes,
   1.112                        entry.ml_timing.elapsed.minutes,
   1.113                        entry.ml_timing.resources.minutes,
   1.114 -                      (entry.heap_size.toDouble / (1024 * 1024)).toString).mkString(" "))))
   1.115 +                      heap_scale(entry.heap_size),
   1.116 +                      heap_scale(entry.heap_size_max)).mkString(" "))))
   1.117  
   1.118                val max_time =
   1.119                  ((0.0 /: session.entries){ case (m, entry) =>
   1.120 @@ -292,8 +318,10 @@
   1.121  
   1.122                val heap_plots =
   1.123                  List(
   1.124 -                  """ using 1:6 smooth sbezier title "heap (smooth)" """,
   1.125 -                  """ using 1:6 smooth csplines title "heap" """)
   1.126 +                  """ using 1:6 smooth sbezier title "final heap (smooth)" """,
   1.127 +                  """ using 1:6 smooth csplines title "final heap" """,
   1.128 +                  """ using 1:7 smooth sbezier title "max heap (smooth)" """,
   1.129 +                  """ using 1:7 smooth csplines title "max heap" """)
   1.130  
   1.131                val plot_names =
   1.132                  (if (session.check_timing)
   1.133 @@ -346,6 +374,7 @@
   1.134      Isabelle_Tool("build_status", "present recent build status information from database", args =>
   1.135      {
   1.136        var target_dir = default_target_dir
   1.137 +      var ml_statistics = false
   1.138        var only_sessions = Set.empty[String]
   1.139        var options = Options.init()
   1.140        var image_size = default_image_size
   1.141 @@ -356,6 +385,7 @@
   1.142  
   1.143    Options are:
   1.144      -D DIR       target directory (default """ + default_target_dir + """)
   1.145 +    -M           include full ML statistics
   1.146      -S SESSIONS  only given SESSIONS (comma separated)
   1.147      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   1.148      -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
   1.149 @@ -366,6 +396,7 @@
   1.150    build_log_history etc.
   1.151  """,
   1.152          "D:" -> (arg => target_dir = Path.explode(arg)),
   1.153 +        "M" -> (_ => ml_statistics = true),
   1.154          "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   1.155          "o:" -> (arg => options = options + arg),
   1.156          "s:" -> (arg =>
   1.157 @@ -381,7 +412,7 @@
   1.158        val progress = new Console_Progress
   1.159  
   1.160        build_status(options, progress = progress, only_sessions = only_sessions, verbose = verbose,
   1.161 -        target_dir = target_dir, image_size = image_size)
   1.162 +        target_dir = target_dir, ml_statistics = ml_statistics, image_size = image_size)
   1.163  
   1.164    }, admin = true)
   1.165  }