more uniform charts;
authorwenzelm
Sun May 07 17:40:41 2017 +0200 (2017-05-07)
changeset 65760a51290fd62d9
parent 65759 a2b041a36523
child 65761 ce909161d030
more uniform charts;
tuned headings;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 17:29:38 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 17:40:41 2017 +0200
     1.3 @@ -161,10 +161,9 @@
     1.4                    entries.map(entry =>
     1.5                      List(entry.date.unix_epoch.toString,
     1.6                        entry.timing.elapsed.minutes,
     1.7 -                      entry.timing.cpu.minutes,
     1.8 +                      entry.timing.resources.minutes,
     1.9                        entry.ml_timing.elapsed.minutes,
    1.10 -                      entry.ml_timing.cpu.minutes,
    1.11 -                      entry.ml_timing.gc.minutes).mkString(" "))))
    1.12 +                      entry.ml_timing.resources.minutes).mkString(" "))))
    1.13  
    1.14                def gnuplot(plots: List[String], kind: String): Process_Result =
    1.15                {
    1.16 @@ -196,9 +195,7 @@
    1.17                    """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
    1.18                    """ using 1:5 smooth csplines title "ML cpu time" """,
    1.19                    """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
    1.20 -                  """ using 1:4 smooth csplines title "ML elapsed time" """,
    1.21 -                  """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
    1.22 -                  """ using 1:6 smooth csplines title "ML gc time" """)
    1.23 +                  """ using 1:4 smooth csplines title "ML elapsed time" """)
    1.24  
    1.25                List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
    1.26              }
    1.27 @@ -206,12 +203,11 @@
    1.28          }, session_entries).flatten.foreach(_.check)
    1.29  
    1.30        val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
    1.31 -      val heading = "Build status for " + data_name + " (" + data.date + ")"
    1.32  
    1.33        File.write(dir + Path.basic("index.html"),
    1.34          HTML.output_document(
    1.35 -          List(HTML.title(heading)),
    1.36 -          HTML.chapter(heading) ::
    1.37 +          List(HTML.title("Isabelle build status for " + data_name)),
    1.38 +          HTML.chapter("Isabelle build status for " + data_name + " (" + data.date + ")") ::
    1.39            HTML.itemize(
    1.40              sessions.map({ case (name, entries) =>
    1.41                HTML.link("#session_" + name, HTML.text(name)) ::
    1.42 @@ -230,12 +226,10 @@
    1.43                    HTML.image(name + "_ml_timing.png")))) })))
    1.44      }
    1.45  
    1.46 -    val heading = "Build status (" + data.date + ")"
    1.47 -
    1.48      File.write(target_dir + Path.basic("index.html"),
    1.49        HTML.output_document(
    1.50 -        List(HTML.title(heading)),
    1.51 -        List(HTML.chapter(heading),
    1.52 +        List(HTML.title("Isabelle build status")),
    1.53 +        List(HTML.chapter("Isabelle build status (" + data.date + ")"),
    1.54            HTML.itemize(data_entries.map({ case (name, _) =>
    1.55              List(HTML.link(name + "/index.html", HTML.text(name))) })))))
    1.56    }