src/Pure/Admin/build_status.scala
author wenzelm
Sun May 07 17:06:05 2017 +0200 (2017-05-07)
changeset 65757 a6522bb9acfa
parent 65756 2c6b5dd59db3
child 65758 d79126bb5d07
permissions -rw-r--r--
tuned 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 = (640, 480)
    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       Par_List.map[(String, List[isabelle.Build_Status.Entry]), Process_Result](
   163         { case (session, entries) =>
   164           Isabelle_System.with_tmp_file(session, "data") { data_file =>
   165             Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
   166 
   167               File.write(data_file,
   168                 cat_lines(
   169                   entries.map(entry =>
   170                     List(entry.date.unix_epoch.toString,
   171                       entry.timing.elapsed.minutes,
   172                       entry.timing.cpu.minutes,
   173                       entry.ml_timing.elapsed.minutes,
   174                       entry.ml_timing.cpu.minutes,
   175                       entry.ml_timing.gc.minutes).mkString(" "))))
   176 
   177               val plots1 =
   178                 List(
   179                   """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   180                   """ using 1:3 smooth csplines title "cpu time" """,
   181                   """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   182                   """ using 1:2 smooth csplines title "elapsed time" """)
   183               val plots2 =
   184                 List(
   185                   """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   186                   """ using 1:5 smooth csplines title "ML cpu time" """,
   187                   """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   188                   """ using 1:4 smooth csplines title "ML elapsed time" """,
   189                   """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
   190                   """ using 1:6 smooth csplines title "ML gc time" """)
   191               val plots =
   192                 ml_timing match {
   193                   case None => plots1
   194                   case Some(false) => plots1 ::: plots2
   195                   case Some(true) => plots2
   196                 }
   197 
   198               File.write(gnuplot_file, """
   199 set terminal png size """ + image_size._1 + "," + image_size._2 + """
   200 set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
   201 set xdata time
   202 set timefmt "%s"
   203 set format x "%d-%b"
   204 set xlabel """ + quote(session) + """ noenhanced
   205 set key left top
   206 plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   207 
   208               val result =
   209                 Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   210               if (result.ok) result
   211               else result.error("Gnuplot failed for " + data_name + "/" + session)
   212             }
   213           }
   214         }, session_entries).foreach(_.check)
   215 
   216       val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
   217       val heading = "Build status for " + data_name + " (" + data.date + ")"
   218 
   219       File.write(dir + Path.basic("index.html"),
   220         HTML.output_document(
   221           List(HTML.title(heading)),
   222           HTML.chapter(heading) ::
   223           HTML.itemize(
   224             sessions.map({ case (name, entries) =>
   225               HTML.link("#session_" + name, HTML.text(name)) ::
   226               HTML.text(" (" + entries.head.timing.message_resources + ")") })) ::
   227           sessions.flatMap({ case (name, entries) =>
   228             List(
   229               HTML.section(name) + HTML.id("session_" + name),
   230               HTML.par(
   231                 List(
   232                   HTML.itemize(List(
   233                     HTML.bold(HTML.text("timing: ")) ::
   234                       HTML.text(entries.head.timing.message_resources),
   235                     HTML.bold(HTML.text("ML timing: ")) ::
   236                       HTML.text(entries.head.ml_timing.message_resources))),
   237                   HTML.image(name + ".png")))) })))
   238     }
   239 
   240     val heading = "Build status (" + data.date + ")"
   241 
   242     File.write(target_dir + Path.basic("index.html"),
   243       HTML.output_document(
   244         List(HTML.title(heading)),
   245         List(HTML.chapter(heading),
   246           HTML.itemize(data_entries.map({ case (name, _) =>
   247             List(HTML.link(name + "/index.html", HTML.text(name))) })))))
   248   }
   249 
   250 
   251   /* Isabelle tool wrapper */
   252 
   253   val isabelle_tool =
   254     Isabelle_Tool("build_status", "present recent build status information from database", args =>
   255     {
   256       var target_dir = default_target_dir
   257       var ml_timing: Option[Boolean] = None
   258       var only_sessions = Set.empty[String]
   259       var elapsed_threshold = Time.zero
   260       var history_length = default_history_length
   261       var options = Options.init()
   262       var image_size = default_image_size
   263       var verbose = false
   264 
   265       val getopts = Getopts("""
   266 Usage: isabelle build_status [OPTIONS]
   267 
   268   Options are:
   269     -D DIR       target directory (default """ + default_target_dir + """)
   270     -M           only ML timing
   271     -S SESSIONS  only given SESSIONS (comma separated)
   272     -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
   273     -l LENGTH    length of history (default """ + default_history_length + """)
   274     -m           include ML timing
   275     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   276     -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
   277     -v           verbose
   278 
   279   Present performance statistics from build log database, which is specified
   280   via system options build_log_database_host, build_log_database_user etc.
   281 """,
   282         "D:" -> (arg => target_dir = Path.explode(arg)),
   283         "M" -> (_ => ml_timing = Some(true)),
   284         "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   285         "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
   286         "l:" -> (arg => history_length = Value.Int.parse(arg)),
   287         "m" -> (_ => ml_timing = Some(false)),
   288         "o:" -> (arg => options = options + arg),
   289         "s:" -> (arg =>
   290           space_explode('x', arg).map(Value.Int.parse(_)) match {
   291             case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
   292             case _ => error("Error bad PNG image size: " + quote(arg))
   293           }),
   294         "v" -> (_ => verbose = true))
   295 
   296       val more_args = getopts(args)
   297       if (more_args.nonEmpty) getopts.usage()
   298 
   299       val progress = new Console_Progress
   300 
   301       val data =
   302         read_data(options, progress = progress, history_length = history_length,
   303           only_sessions = only_sessions, elapsed_threshold = elapsed_threshold, verbose = verbose)
   304 
   305       present_data(data, progress = progress, target_dir = target_dir,
   306         image_size = image_size, ml_timing = ml_timing)
   307 
   308   }, admin = true)
   309 }