src/Pure/Admin/build_status.scala
author wenzelm
Sun May 07 16:31:39 2017 +0200 (2017-05-07)
changeset 65755 21b4bfa6d204
parent 65754 05c6a29c9132
child 65756 2c6b5dd59db3
permissions -rw-r--r--
more HTML output;
     1 /*  Title:      Pure/Admin/build_status.scala
     2     Author:     Makarius
     3 
     4 Present recent build status information from database.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Build_Status
    11 {
    12   private val default_target_dir = Path.explode("build_status")
    13   private val default_history_length = 30
    14   private val default_image_size = (800, 600)
    15 
    16 
    17   /* data profiles */
    18 
    19   sealed case class Profile(name: String, sql: String)
    20   {
    21     def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
    22     {
    23       val sql_sessions =
    24         if (only_sessions.isEmpty) ""
    25         else
    26           only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
    27             .mkString("(", " OR ", ") AND ")
    28 
    29       Build_Log.Data.universal_table.select(columns, distinct = true,
    30         sql = "WHERE " +
    31           Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
    32           Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
    33           " AND " + sql_sessions + SQL.enclose(sql) +
    34           " ORDER BY " + Build_Log.Data.pull_date + " DESC")
    35     }
    36   }
    37 
    38   val standard_profiles: List[Profile] =
    39     Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
    40 
    41   sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
    42   {
    43     def check(elapsed_threshold: Time): Boolean =
    44       !timing.is_zero && timing.elapsed >= elapsed_threshold
    45   }
    46 
    47   sealed case class Data(date: Date, entries: Map[String, Map[String, List[Entry]]])
    48   {
    49     def sorted_entries: List[(String, List[(String, List[Entry])])] =
    50       entries.toList.sortBy(_._1).map({ case (name, session_entries) =>
    51         (name, session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse) })
    52   }
    53 
    54 
    55   /* read data */
    56 
    57   def read_data(options: Options,
    58     profiles: List[Profile] = standard_profiles,
    59     progress: Progress = No_Progress,
    60     history_length: Int = default_history_length,
    61     only_sessions: Set[String] = Set.empty,
    62     elapsed_threshold: Time = Time.zero,
    63     verbose: Boolean = false): Data =
    64   {
    65     val date = Date.now()
    66     var data_entries = Map.empty[String, Map[String, List[Entry]]]
    67 
    68     val store = Build_Log.store(options)
    69     using(store.open_database())(db =>
    70     {
    71       for (profile <- profiles.sortBy(_.name)) {
    72         progress.echo("input " + quote(profile.name))
    73         val columns =
    74           List(
    75             Build_Log.Data.pull_date,
    76             Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
    77             Build_Log.Settings.ML_PLATFORM,
    78             Build_Log.Data.session_name,
    79             Build_Log.Data.threads,
    80             Build_Log.Data.timing_elapsed,
    81             Build_Log.Data.timing_cpu,
    82             Build_Log.Data.timing_gc,
    83             Build_Log.Data.ml_timing_elapsed,
    84             Build_Log.Data.ml_timing_cpu,
    85             Build_Log.Data.ml_timing_gc)
    86 
    87         val Threads_Option = """threads\s*=\s*(\d+)""".r
    88 
    89         val sql = profile.select(columns, history_length, only_sessions)
    90         if (verbose) progress.echo(sql)
    91 
    92         db.using_statement(sql)(stmt =>
    93         {
    94           val res = stmt.execute_query()
    95           while (res.next()) {
    96             val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
    97 
    98             val threads_option =
    99               res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
   100                 case Threads_Option(Value.Int(i)) => i
   101                 case _ => 1
   102               }
   103             val threads = res.get_int(Build_Log.Data.threads).getOrElse(1)
   104 
   105             val name =
   106               profile.name +
   107                 "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
   108                 "_M" + (threads_option max threads)
   109 
   110             val session = res.string(Build_Log.Data.session_name)
   111             val entry =
   112               Entry(res.date(Build_Log.Data.pull_date),
   113                 res.timing(
   114                   Build_Log.Data.timing_elapsed,
   115                   Build_Log.Data.timing_cpu,
   116                   Build_Log.Data.timing_gc),
   117                 res.timing(
   118                   Build_Log.Data.ml_timing_elapsed,
   119                   Build_Log.Data.ml_timing_cpu,
   120                   Build_Log.Data.ml_timing_gc))
   121 
   122             val session_entries = data_entries.getOrElse(name, Map.empty)
   123             val entries = session_entries.getOrElse(session, Nil)
   124             data_entries += (name -> (session_entries + (session -> (entry :: entries))))
   125           }
   126         })
   127       }
   128     })
   129 
   130     Data(date,
   131       for {
   132         (name, session_entries) <- data_entries
   133         session_entries1 <-
   134           {
   135             val session_entries1 =
   136               for {
   137                 (session, entries) <- session_entries
   138                 if entries.filter(_.check(elapsed_threshold)).length >= 3
   139               } yield (session, entries)
   140             if (session_entries1.isEmpty) None
   141             else Some(session_entries1)
   142           }
   143       } yield (name, session_entries1))
   144   }
   145 
   146 
   147   /* present data */
   148 
   149   def present_data(data: Data,
   150     progress: Progress = No_Progress,
   151     target_dir: Path = default_target_dir,
   152     image_size: (Int, Int) = default_image_size,
   153     ml_timing: Option[Boolean] = None)
   154   {
   155     val data_entries = data.sorted_entries
   156 
   157     for ((data_name, session_entries) <- data_entries) {
   158       val dir = target_dir + Path.explode(data_name)
   159       progress.echo("output " + dir)
   160       Isabelle_System.mkdirs(dir)
   161 
   162       for ((session, entries) <- session_entries) {
   163         Isabelle_System.with_tmp_file(session, "data") { data_file =>
   164           Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
   165 
   166             File.write(data_file,
   167               cat_lines(
   168                 entries.map(entry =>
   169                   List(entry.date.unix_epoch.toString,
   170                     entry.timing.elapsed.minutes,
   171                     entry.timing.cpu.minutes,
   172                     entry.ml_timing.elapsed.minutes,
   173                     entry.ml_timing.cpu.minutes,
   174                     entry.ml_timing.gc.minutes).mkString(" "))))
   175 
   176             val plots1 =
   177               List(
   178                 """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   179                 """ using 1:3 smooth csplines title "cpu time" """,
   180                 """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   181                 """ using 1:2 smooth csplines title "elapsed time" """)
   182             val plots2 =
   183               List(
   184                 """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   185                 """ using 1:5 smooth csplines title "ML cpu time" """,
   186                 """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   187                 """ using 1:4 smooth csplines title "ML elapsed time" """,
   188                 """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
   189                 """ using 1:6 smooth csplines title "ML gc time" """)
   190             val plots =
   191               ml_timing match {
   192                 case None => plots1
   193                 case Some(false) => plots1 ::: plots2
   194                 case Some(true) => plots2
   195               }
   196 
   197             File.write(gnuplot_file, """
   198 set terminal png size """ + image_size._1 + "," + image_size._2 + """
   199 set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
   200 set xdata time
   201 set timefmt "%s"
   202 set format x "%d-%b"
   203 set xlabel """ + quote(session) + """ noenhanced
   204 set key left top
   205 plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   206 
   207             val result =
   208               Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   209             if (result.rc != 0)
   210               result.error("Gnuplot failed for " + data_name + "/" + session).check
   211           }
   212         }
   213       }
   214 
   215       val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
   216       val heading = "Build status for " + data_name + " (" + data.date + ")"
   217 
   218       File.write(dir + Path.basic("index.html"),
   219         HTML.output_document(
   220           List(HTML.title(heading)),
   221           HTML.chapter(heading) ::
   222           HTML.itemize(
   223             sessions.map({ case (name, entries) =>
   224               HTML.link("#session_" + name, HTML.text(name)) ::
   225               HTML.text(" (" + entries.head.timing.message_resources + ")") })) ::
   226           sessions.flatMap({ case (name, entries) =>
   227             List(
   228               HTML.section(name) + HTML.id("session_" + name),
   229               HTML.par(
   230                 List(
   231                   HTML.itemize(List(
   232                     HTML.bold(HTML.text("last timing: ")) ::
   233                       HTML.text(entries.head.timing.message_resources),
   234                     HTML.bold(HTML.text("last ML timing: ")) ::
   235                       HTML.text(entries.head.ml_timing.message_resources))),
   236                   HTML.image(name + ".png")))) })))
   237     }
   238 
   239     val heading = "Build status (" + data.date + ")"
   240 
   241     File.write(target_dir + Path.basic("index.html"),
   242       HTML.output_document(
   243         List(HTML.title(heading)),
   244         List(HTML.chapter(heading),
   245           HTML.itemize(data_entries.map({ case (name, _) =>
   246             List(HTML.link(name + "/index.html", HTML.text(name))) })))))
   247   }
   248 
   249 
   250   /* Isabelle tool wrapper */
   251 
   252   val isabelle_tool =
   253     Isabelle_Tool("build_status", "present recent build status information from database", args =>
   254     {
   255       var target_dir = default_target_dir
   256       var ml_timing: Option[Boolean] = None
   257       var only_sessions = Set.empty[String]
   258       var elapsed_threshold = Time.zero
   259       var history_length = default_history_length
   260       var options = Options.init()
   261       var image_size = default_image_size
   262       var verbose = false
   263 
   264       val getopts = Getopts("""
   265 Usage: isabelle build_status [OPTIONS]
   266 
   267   Options are:
   268     -D DIR       target directory (default """ + default_target_dir + """)
   269     -M           only ML timing
   270     -S SESSIONS  only given SESSIONS (comma separated)
   271     -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
   272     -l LENGTH    length of history (default """ + default_history_length + """)
   273     -m           include ML timing
   274     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   275     -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
   276     -v           verbose
   277 
   278   Present performance statistics from build log database, which is specified
   279   via system options build_log_database_host, build_log_database_user etc.
   280 """,
   281         "D:" -> (arg => target_dir = Path.explode(arg)),
   282         "M" -> (_ => ml_timing = Some(true)),
   283         "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   284         "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
   285         "l:" -> (arg => history_length = Value.Int.parse(arg)),
   286         "m" -> (_ => ml_timing = Some(false)),
   287         "o:" -> (arg => options = options + arg),
   288         "s:" -> (arg =>
   289           space_explode('x', arg).map(Value.Int.parse(_)) match {
   290             case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
   291             case _ => error("Error bad PNG image size: " + quote(arg))
   292           }),
   293         "v" -> (_ => verbose = true))
   294 
   295       val more_args = getopts(args)
   296       if (more_args.nonEmpty) getopts.usage()
   297 
   298       val progress = new Console_Progress
   299 
   300       val data =
   301         read_data(options, progress = progress, history_length = history_length,
   302           only_sessions = only_sessions, elapsed_threshold = elapsed_threshold, verbose = verbose)
   303 
   304       present_data(data, progress = progress, target_dir = target_dir,
   305         image_size = image_size, ml_timing = ml_timing)
   306 
   307   }, admin = true)
   308 }