obsolete
authorLars Hupel <lars.hupel@mytum.de>
Mon Jun 25 17:18:59 2018 +0200 (14 months ago)
changeset 6849571483c0e0023
parent 68494 ebdd5508f386
child 68497 f483fe1813f0
obsolete
Admin/jenkins/build/ci_build_stats.scala
     1.1 --- a/Admin/jenkins/build/ci_build_stats.scala	Mon Jun 25 14:06:50 2018 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,64 +0,0 @@
     1.4 -// FIXME obsolete
     1.5 -
     1.6 -object stats extends isabelle.Isabelle_Tool.Body {
     1.7 -
     1.8 -  import isabelle._
     1.9 -  import java.time._
    1.10 -  import java.time.format.DateTimeFormatter
    1.11 -
    1.12 -
    1.13 -  val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME)
    1.14 -
    1.15 -  val target_dir = Path.explode("stats")
    1.16 -  val jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
    1.17 -
    1.18 -  val html_header = s"""<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    1.19 -<html>
    1.20 -<head><title>Performance statistics from session build output</title></head>
    1.21 -<body>
    1.22 -  <p>Generated at $start_time</p>
    1.23 -"""
    1.24 -
    1.25 -  val html_footer = """
    1.26 -</body>
    1.27 -</html>
    1.28 -"""
    1.29 -
    1.30 -  def generate(job: String): Unit = {
    1.31 -    println(s"=== $job ===")
    1.32 -
    1.33 -    val dir = target_dir + Path.basic(job)
    1.34 -    val sessions: List[String] = Nil
    1.35 -
    1.36 -    val sections =
    1.37 -      cat_lines(
    1.38 -        sessions.map(session =>
    1.39 -          "<p id=" + quote("session_" + HTML.output(session)) + ">" +
    1.40 -          "<h2>" + HTML.output(session) + "</h2>" +
    1.41 -          "<img src=" + quote(HTML.output(session + ".png")) + "></p>\n"))
    1.42 -
    1.43 -    val toc =
    1.44 -      cat_lines(
    1.45 -        sessions.map(session =>
    1.46 -          "<li><a href=" + quote("#session_" + HTML.output(session)) + ">" +
    1.47 -          HTML.output(session) + "</a></li>\n"))
    1.48 -
    1.49 -    val html =
    1.50 -      html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" + "<div><ul>" + toc + "</ul></div>\n" +
    1.51 -      sections + html_footer
    1.52 -
    1.53 -    File.write(dir + Path.basic("index.html"), html)
    1.54 -  }
    1.55 -
    1.56 -  override final def apply(args: List[String]): Unit = {
    1.57 -    jobs.foreach(generate)
    1.58 -
    1.59 -    File.write(target_dir + Path.basic("index.html"),
    1.60 -      html_header + "\n<ul>\n" +
    1.61 -      cat_lines(
    1.62 -        jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" +
    1.63 -          HTML.output(job) + """</a> </li>""")) +
    1.64 -      "\n</ul>\n" + html_footer)
    1.65 -  }
    1.66 -
    1.67 -}