Admin/jenkins/build/ci_build_stats.scala
author wenzelm
Wed, 17 May 2017 13:47:19 +0200
changeset 65851 c103358a5559
parent 65790 91940684a267
permissions -rw-r--r--
tuned signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65790
91940684a267 obsolete;
wenzelm
parents: 65734
diff changeset
     1
// FIXME obsolete
91940684a267 obsolete;
wenzelm
parents: 65734
diff changeset
     2
63942
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     3
object stats extends isabelle.Isabelle_Tool.Body {
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     4
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
     5
  import isabelle._
63943
fbc2b562331b include generation time in statistics
Lars Hupel <lars.hupel@mytum.de>
parents: 63942
diff changeset
     6
  import java.time._
fbc2b562331b include generation time in statistics
Lars Hupel <lars.hupel@mytum.de>
parents: 63942
diff changeset
     7
  import java.time.format.DateTimeFormatter
fbc2b562331b include generation time in statistics
Lars Hupel <lars.hupel@mytum.de>
parents: 63942
diff changeset
     8
fbc2b562331b include generation time in statistics
Lars Hupel <lars.hupel@mytum.de>
parents: 63942
diff changeset
     9
fbc2b562331b include generation time in statistics
Lars Hupel <lars.hupel@mytum.de>
parents: 63942
diff changeset
    10
  val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
63942
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    11
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    12
  val target_dir = Path.explode("stats")
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    13
  val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    14
63943
fbc2b562331b include generation time in statistics
Lars Hupel <lars.hupel@mytum.de>
parents: 63942
diff changeset
    15
  val html_header = s"""<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
63942
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    16
<html>
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    17
<head><title>Performance statistics from session build output</title></head>
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    18
<body>
63943
fbc2b562331b include generation time in statistics
Lars Hupel <lars.hupel@mytum.de>
parents: 63942
diff changeset
    19
  <p>Generated at $start_time</p>
63942
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    20
"""
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    21
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    22
  val html_footer = """
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    23
</body>
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    24
</html>
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    25
"""
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    26
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    27
  def generate(job: String): Unit = {
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    28
    println(s"=== $job ===")
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    29
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    30
    val dir = target_dir + Path.basic(job)
65790
91940684a267 obsolete;
wenzelm
parents: 65734
diff changeset
    31
    val sessions: List[String] = Nil
63942
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    32
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    33
    val sections =
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    34
      cat_lines(
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    35
        sessions.map(session =>
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    36
          "<p id=" + quote("session_" + HTML.output(session)) + ">" +
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    37
          "<h2>" + HTML.output(session) + "</h2>" +
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    38
          "<img src=" + quote(HTML.output(session + ".png")) + "></p>\n"))
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    39
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    40
    val toc =
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    41
      cat_lines(
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    42
        sessions.map(session =>
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    43
          "<li><a href=" + quote("#session_" + HTML.output(session)) + ">" +
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    44
          HTML.output(session) + "</a></li>\n"))
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    45
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    46
    val html =
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    47
      html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" + "<div><ul>" + toc + "</ul></div>\n" +
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    48
      sections + html_footer
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    49
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    50
    File.write(dir + Path.basic("index.html"), html)
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    51
  }
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    52
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    53
  override final def apply(args: List[String]): Unit = {
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    54
    jobs.foreach(generate)
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    55
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    56
    File.write(target_dir + Path.basic("index.html"),
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    57
      html_header + "\n<ul>\n" +
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    58
      cat_lines(
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    59
        jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" +
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    60
          HTML.output(job) + """</a> </li>""")) +
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    61
      "\n</ul>\n" + html_footer)
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    62
  }
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    63
9195600fcc7c CI script to generate timing statistics
Lars Hupel <lars.hupel@mytum.de>
parents:
diff changeset
    64
}