more plots from ml_statistics;
authorwenzelm
Thu May 18 14:14:20 2017 +0200 (2017-05-18)
changeset 65865177b90f33f40
parent 65864 1945fa8f0c39
child 65866 00e8b836d4db
more plots from ml_statistics;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Thu May 18 13:51:25 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Thu May 18 14:14:20 2017 +0200
     1.3 @@ -66,7 +66,8 @@
     1.4    sealed case class Data(date: Date, entries: List[Data_Entry])
     1.5    sealed case class Data_Entry(
     1.6      name: String, hosts: List[String], stretch: Double, sessions: List[Session])
     1.7 -  sealed case class Session(name: String, threads: Int, entries: List[Entry])
     1.8 +  sealed case class Session(
     1.9 +    name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics)
    1.10    {
    1.11      require(entries.nonEmpty)
    1.12  
    1.13 @@ -91,6 +92,11 @@
    1.14      average_heap: Long,
    1.15      final_heap: Long)
    1.16  
    1.17 +  sealed case class Image(name: String, width: Int, height: Int)
    1.18 +  {
    1.19 +    def path: Path = Path.basic(name)
    1.20 +  }
    1.21 +
    1.22    def read_data(options: Options,
    1.23      progress: Progress = No_Progress,
    1.24      profiles: List[Profile] = default_profiles,
    1.25 @@ -191,7 +197,7 @@
    1.26  
    1.27              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.28              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.29 -            val session = Session(session_name, threads, entry :: entries)
    1.30 +            val session = Session(session_name, threads, entry :: entries, ml_stats)
    1.31              data_entries += (data_name -> (sessions + (session_name -> session)))
    1.32            }
    1.33          })
    1.34 @@ -245,8 +251,8 @@
    1.35      for (data_entry <- data.entries) {
    1.36        val data_name = data_entry.name
    1.37  
    1.38 -      val image_width = (image_size._1 * data_entry.stretch).toInt
    1.39 -      val image_height = image_size._2
    1.40 +      val (image_width, image_height) = image_size
    1.41 +      val image_width_stretch = (image_width * data_entry.stretch).toInt
    1.42  
    1.43        progress.echo("output " + quote(data_name))
    1.44  
    1.45 @@ -258,6 +264,8 @@
    1.46            Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
    1.47              Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
    1.48  
    1.49 +              def plot_name(kind: String): String = session.name + "_" + kind + ".png"
    1.50 +
    1.51                File.write(data_file,
    1.52                  cat_lines(
    1.53                    session.entries.map(entry =>
    1.54 @@ -278,13 +286,13 @@
    1.55                      max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
    1.56                val timing_range = "[0:" + max_time + "]"
    1.57  
    1.58 -              def gnuplot(plots: List[String], kind: String, range: String): String =
    1.59 +              def gnuplot(plot_name: String, plots: List[String], range: String): Image =
    1.60                {
    1.61 -                val plot_name = session.name + "_" + kind + ".png"
    1.62 +                val image = Image(plot_name, image_width_stretch, image_height)
    1.63  
    1.64                  File.write(gnuplot_file, """
    1.65 -set terminal png size """ + image_width + "," + image_height + """
    1.66 -set output """ + quote(File.standard_path(dir + Path.basic(plot_name))) + """
    1.67 +set terminal png size """ + image.width + "," + image.height + """
    1.68 +set output """ + quote(File.standard_path(dir + image.path)) + """
    1.69  set xdata time
    1.70  set timefmt "%s"
    1.71  set format x "%d-%b"
    1.72 @@ -298,7 +306,7 @@
    1.73                  if (!result.ok)
    1.74                    result.error("Gnuplot failed for " + data_name + "/" + plot_name).check
    1.75  
    1.76 -                plot_name
    1.77 +                image
    1.78                }
    1.79  
    1.80                val timing_plots =
    1.81 @@ -330,15 +338,34 @@
    1.82                    """ using 1:8 smooth sbezier title "final heap (smooth)" """,
    1.83                    """ using 1:8 smooth csplines title "final heap" """)
    1.84  
    1.85 -              val plot_names =
    1.86 +              def jfreechart(plot_name: String, fields: ML_Statistics.Fields): Image =
    1.87 +              {
    1.88 +                val image = Image(plot_name, image_width, image_height)
    1.89 +                val chart =
    1.90 +                  session.ml_statistics.chart(
    1.91 +                    fields._1 + ": " + session.ml_statistics.heading, fields._2)
    1.92 +                Graphics_File.write_chart_png(
    1.93 +                  (dir + image.path).file, chart, image.width, image.height)
    1.94 +                image
    1.95 +              }
    1.96 +
    1.97 +              val images =
    1.98                  (if (session.check_timing)
    1.99                    List(
   1.100 -                    gnuplot(timing_plots, "timing", timing_range),
   1.101 -                    gnuplot(ml_timing_plots, "ml_timing", timing_range))
   1.102 +                    gnuplot(plot_name("timing"), timing_plots, timing_range),
   1.103 +                    gnuplot(plot_name("ml_timing"), ml_timing_plots, timing_range))
   1.104 +                 else Nil) :::
   1.105 +                (if (session.check_heap)
   1.106 +                  List(gnuplot(plot_name("heap"), heap_plots, "[0:]"))
   1.107                   else Nil) :::
   1.108 -                (if (session.check_heap) List(gnuplot(heap_plots, "heap", "[0:]")) else Nil)
   1.109 +                (if (session.ml_statistics.content.nonEmpty)
   1.110 +                  List(jfreechart(plot_name("heap_chart"), ML_Statistics.heap_fields)) :::
   1.111 +                  (if (session.threads > 1)
   1.112 +                    List(jfreechart(plot_name("tasks_chart"), ML_Statistics.tasks_fields))
   1.113 +                   else Nil)
   1.114 +                 else Nil)
   1.115  
   1.116 -              session.name -> plot_names
   1.117 +              session.name -> images
   1.118              }
   1.119            }, data_entry.sessions).toMap
   1.120  
   1.121 @@ -373,10 +400,10 @@
   1.122                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
   1.123                  proper_string(session.head.afp_version).map(s =>
   1.124                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
   1.125 -              session_plots.getOrElse(session.name, Nil).map(plot_name =>
   1.126 -                HTML.image(plot_name) +
   1.127 -                  HTML.width(image_width / 2) +
   1.128 -                  HTML.height(image_height / 2))))))
   1.129 +              session_plots.getOrElse(session.name, Nil).map(image =>
   1.130 +                HTML.image(image.name) +
   1.131 +                  HTML.width(image.width / 2) +
   1.132 +                  HTML.height(image.height / 2))))))
   1.133      }
   1.134    }
   1.135