src/Pure/Admin/build_stats.scala
author wenzelm
Wed Oct 12 10:22:34 2016 +0200 (2016-10-12)
changeset 64161 2b1128e95dfb
parent 64106 src/Pure/Tools/build_stats.scala@b7ff61d50b19
child 64220 e7cbf81ec4b7
permissions -rw-r--r--
explicit indication of Admin tools;
     1 /*  Title:      Pure/Admin/build_stats.scala
     2     Author:     Makarius
     3 
     4 Statistics from session build output.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Build_Stats
    11 {
    12   /* presentation */
    13 
    14   private val default_history_length = 100
    15   private val default_size = (800, 600)
    16   private val default_only_sessions = Set.empty[String]
    17   private val default_elapsed_threshold = Time.zero
    18   private val default_ml_timing: Option[Boolean] = None
    19 
    20   def present_job(job: String, dir: Path,
    21     history_length: Int = default_history_length,
    22     size: (Int, Int) = default_size,
    23     only_sessions: Set[String] = default_only_sessions,
    24     elapsed_threshold: Time = default_elapsed_threshold,
    25     ml_timing: Option[Boolean] = default_ml_timing): List[String] =
    26   {
    27     val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
    28     if (job_infos.isEmpty) error("No build infos for job " + quote(job))
    29 
    30     val all_infos =
    31       Par_List.map((job_info: CI_API.Job_Info) =>
    32         (job_info.timestamp / 1000, job_info.read_main_log.parse_build_info), job_infos)
    33     val all_sessions =
    34       (Set.empty[String] /: all_infos)(
    35         { case (s, (_, info)) => s ++ info.sessions.keySet })
    36 
    37     def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
    38     {
    39       val t = info.timing(session)
    40       !t.is_zero && t.elapsed >= elapsed_threshold
    41     }
    42 
    43     val sessions =
    44       for {
    45         session <- (if (only_sessions.isEmpty) all_sessions else all_sessions & only_sessions)
    46         if all_infos.filter({ case (_, info) => check_threshold(info, session) }).length >= 3
    47       } yield session
    48 
    49     Isabelle_System.mkdirs(dir)
    50     for (session <- sessions) {
    51       Isabelle_System.with_tmp_file(session, "png") { data_file =>
    52         Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
    53           val data =
    54             for { (t, info) <- all_infos if info.finished(session) }
    55             yield {
    56               val timing1 = info.timing(session)
    57               val timing2 = info.ml_timing(session)
    58               List(t.toString,
    59                 timing1.elapsed.minutes,
    60                 timing1.cpu.minutes,
    61                 timing2.elapsed.minutes,
    62                 timing2.cpu.minutes,
    63                 timing2.gc.minutes).mkString(" ")
    64             }
    65           File.write(data_file, cat_lines(data))
    66 
    67           val plots1 =
    68             List(
    69               """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
    70               """ using 1:3 smooth csplines title "cpu time" """,
    71               """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    72               """ using 1:2 smooth csplines title "elapsed time" """)
    73           val plots2 =
    74             List(
    75               """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
    76               """ using 1:5 smooth csplines title "ML cpu time" """,
    77               """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
    78               """ using 1:4 smooth csplines title "ML elapsed time" """,
    79               """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
    80               """ using 1:6 smooth csplines title "ML gc time" """)
    81           val plots =
    82             ml_timing match {
    83               case None => plots1
    84               case Some(false) => plots1 ::: plots2
    85               case Some(true) => plots2
    86             }
    87 
    88           val data_file_name = File.standard_path(data_file.getAbsolutePath)
    89           File.write(plot_file, """
    90 set terminal png size """ + size._1 + "," + size._2 + """
    91 set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
    92 set xdata time
    93 set timefmt "%s"
    94 set format x "%d-%b"
    95 set xlabel """ + quote(session) + """ noenhanced
    96 set key left top
    97 plot [] [0:] """ + plots.map(s => quote(data_file_name) + " " + s).mkString(", ") + "\n")
    98           val result = Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(plot_file))
    99           if (result.rc != 0) {
   100             Output.error_message("Session " + session + ": gnuplot error")
   101             result.print
   102           }
   103         }
   104       }
   105     }
   106 
   107     sessions.toList.sorted
   108   }
   109 
   110 
   111   /* Isabelle tool wrapper */
   112 
   113   private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
   114 <html>
   115 <head><title>Performance statistics from session build output</title></head>
   116 <body>
   117 """
   118   private val html_footer = """
   119 </body>
   120 </html>
   121 """
   122 
   123   val isabelle_tool =
   124     Isabelle_Tool("build_stats", "present statistics from session build output", args =>
   125     {
   126       var target_dir = Path.explode("stats")
   127       var ml_timing = default_ml_timing
   128       var only_sessions = default_only_sessions
   129       var elapsed_threshold = default_elapsed_threshold
   130       var history_length = default_history_length
   131       var size = default_size
   132 
   133       val getopts = Getopts("""
   134 Usage: isabelle build_stats [OPTIONS] [JOBS ...]
   135 
   136   Options are:
   137     -D DIR       target directory (default "stats")
   138     -M           only ML timing
   139     -S SESSIONS  only given SESSIONS (comma separated)
   140     -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
   141     -l LENGTH    length of history (default 100)
   142     -m           include ML timing
   143     -s WxH       size of PNG image (default 800x600)
   144 
   145   Present statistics from session build output of the given JOBS, from Jenkins
   146   continuous build service specified as URL via ISABELLE_JENKINS_ROOT.
   147 """,
   148         "D:" -> (arg => target_dir = Path.explode(arg)),
   149         "M" -> (_ => ml_timing = Some(true)),
   150         "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   151         "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
   152         "l:" -> (arg => history_length = Value.Int.parse(arg)),
   153         "m" -> (_ => ml_timing = Some(false)),
   154         "s:" -> (arg =>
   155           space_explode('x', arg).map(Value.Int.parse(_)) match {
   156             case List(w, h) if w > 0 && h > 0 => size = (w, h)
   157             case _ => error("Error bad PNG image size: " + quote(arg))
   158           }))
   159 
   160       val jobs = getopts(args)
   161       val all_jobs = CI_API.build_jobs()
   162       val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
   163 
   164       if (jobs.isEmpty)
   165         error("No build jobs given. Available jobs: " + all_jobs.sorted.mkString(" "))
   166 
   167       if (bad_jobs.nonEmpty)
   168         error("Unknown build jobs: " + bad_jobs.mkString(" ") +
   169           "\nAvailable jobs: " + all_jobs.sorted.mkString(" "))
   170 
   171       for (job <- jobs) {
   172         val dir = target_dir + Path.basic(job)
   173         Output.writeln(dir.implode)
   174         val sessions =
   175           present_job(job, dir, history_length, size, only_sessions, elapsed_threshold, ml_timing)
   176         File.write(dir + Path.basic("index.html"),
   177           html_header + "\n<h1>" + HTML.output(job) + "</h1>\n" +
   178           cat_lines(
   179             sessions.map(session =>
   180               """<br/><img src=""" + quote(HTML.output(session + ".png")) + """><br/>""")) +
   181           "\n" + html_footer)
   182       }
   183 
   184       File.write(target_dir + Path.basic("index.html"),
   185         html_header + "\n<ul>\n" +
   186         cat_lines(
   187           jobs.map(job => """<li> <a href=""" + quote(HTML.output(job + "/index.html")) + """>""" +
   188             HTML.output(job) + """</a> </li>""")) +
   189         "\n</ul>\n" + html_footer)
   190   }, admin = true)
   191 }