src/Pure/Admin/build_status.scala
changeset 65893 20656a4709d6
parent 65868 65e132abab1e
child 65895 744878d72021
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 21 22:57:46 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 21 23:07:20 2017 +0200
     1.3 @@ -33,7 +33,10 @@
     1.4        Build_Log.Data.universal_table.select(columns, distinct = true,
     1.5          sql = "WHERE " +
     1.6            Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days(options)) + " AND " +
     1.7 -          Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
     1.8 +          SQL.member(Build_Log.Data.status.ident,
     1.9 +            List(
    1.10 +              Build_Log.Session_Status.finished.toString,
    1.11 +              Build_Log.Session_Status.failed.toString)) +
    1.12            (if (only_sessions.isEmpty) ""
    1.13             else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
    1.14            " AND " + SQL.enclose(sql) +
    1.15 @@ -66,6 +69,10 @@
    1.16    sealed case class Data(date: Date, entries: List[Data_Entry])
    1.17    sealed case class Data_Entry(
    1.18      name: String, hosts: List[String], stretch: Double, sessions: List[Session])
    1.19 +  {
    1.20 +    def failed_sessions: List[Session] =
    1.21 +      sessions.filter(_.head.failed).sortBy(_.name)
    1.22 +  }
    1.23    sealed case class Session(
    1.24      name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics)
    1.25    {
    1.26 @@ -74,10 +81,12 @@
    1.27      def head: Entry = entries.head
    1.28      def order: Long = - head.timing.elapsed.ms
    1.29  
    1.30 -    def check_timing: Boolean = entries.length >= 3
    1.31 +    def finished_entries: List[Entry] = entries.filter(_.finished)
    1.32 +
    1.33 +    def check_timing: Boolean = finished_entries.length >= 3
    1.34      def check_heap: Boolean =
    1.35 -      entries.length >= 3 &&
    1.36 -      entries.forall(entry =>
    1.37 +      finished_entries.length >= 3 &&
    1.38 +      finished_entries.forall(entry =>
    1.39          entry.maximum_heap > 0 ||
    1.40          entry.average_heap > 0 ||
    1.41          entry.stored_heap > 0)
    1.42 @@ -90,7 +99,12 @@
    1.43      ml_timing: Timing,
    1.44      maximum_heap: Long,
    1.45      average_heap: Long,
    1.46 -    stored_heap: Long)
    1.47 +    stored_heap: Long,
    1.48 +    status: Build_Log.Session_Status.Value)
    1.49 +  {
    1.50 +    def finished: Boolean = status == Build_Log.Session_Status.finished
    1.51 +    def failed: Boolean = status == Build_Log.Session_Status.failed
    1.52 +  }
    1.53  
    1.54    sealed case class Image(name: String, width: Int, height: Int)
    1.55    {
    1.56 @@ -134,7 +148,8 @@
    1.57              Build_Log.Data.ml_timing_elapsed,
    1.58              Build_Log.Data.ml_timing_cpu,
    1.59              Build_Log.Data.ml_timing_gc,
    1.60 -            Build_Log.Data.heap_size) :::
    1.61 +            Build_Log.Data.heap_size,
    1.62 +            Build_Log.Data.status) :::
    1.63            (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil)
    1.64  
    1.65          val Threads_Option = """threads\s*=\s*(\d+)""".r
    1.66 @@ -193,7 +208,8 @@
    1.67                      Build_Log.Data.ml_timing_gc),
    1.68                  maximum_heap = ml_stats.maximum_heap_size,
    1.69                  average_heap = ml_stats.average_heap_size,
    1.70 -                stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)))
    1.71 +                stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
    1.72 +                status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)))
    1.73  
    1.74              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.75              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.76 @@ -240,8 +256,17 @@
    1.77              List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
    1.78          HTML.par(
    1.79            List(HTML.itemize(data.entries.map({ case data_entry =>
    1.80 -            List(HTML.link(clean_name(data_entry.name) + "/index.html",
    1.81 -              HTML.text(data_entry.name))) }))))))
    1.82 +            List(
    1.83 +              HTML.link(clean_name(data_entry.name) + "/index.html",
    1.84 +                HTML.text(data_entry.name))) :::
    1.85 +            (data_entry.failed_sessions match {
    1.86 +              case Nil => Nil
    1.87 +              case sessions =>
    1.88 +                HTML.break ::: List(HTML.error_message_span("Failed:")) :::
    1.89 +                HTML.text(" " +
    1.90 +                  commas(sessions.map(s => s.name + " (" + s.head.isabelle_version + ")")))
    1.91 +            })
    1.92 +          }))))))
    1.93  
    1.94      for (data_entry <- data.entries) {
    1.95        val data_name = data_entry.name
    1.96 @@ -263,7 +288,7 @@
    1.97  
    1.98                File.write(data_file,
    1.99                  cat_lines(
   1.100 -                  session.entries.map(entry =>
   1.101 +                  session.finished_entries.map(entry =>
   1.102                      List(entry.pull_date.unix_epoch,
   1.103                        entry.timing.elapsed.minutes,
   1.104                        entry.timing.resources.minutes,
   1.105 @@ -274,7 +299,7 @@
   1.106                        entry.stored_heap).mkString(" "))))
   1.107  
   1.108                val max_time =
   1.109 -                ((0.0 /: session.entries){ case (m, entry) =>
   1.110 +                ((0.0 /: session.finished_entries){ case (m, entry) =>
   1.111                    m.max(entry.timing.elapsed.minutes).
   1.112                      max(entry.timing.resources.minutes).
   1.113                      max(entry.ml_timing.elapsed.minutes).