src/Pure/Admin/build_status.scala
changeset 67739 e512938b853c
parent 67738 1bbe618c4b24
child 67749 08dc76bf6400
equal deleted inserted replaced
67738:1bbe618c4b24 67739:e512938b853c
    77   sealed case class Session(
    77   sealed case class Session(
    78     name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics)
    78     name: String, threads: Int, entries: List[Entry], ml_statistics: ML_Statistics)
    79   {
    79   {
    80     require(entries.nonEmpty)
    80     require(entries.nonEmpty)
    81 
    81 
    82     lazy val sorted_entries: List[Entry] =
    82     lazy val sorted_entries: List[Entry] = entries.sortBy(entry => - entry.date)
    83       entries.sortBy(entry => - entry.pull_date.unix_epoch)
       
    84 
    83 
    85     def head: Entry = sorted_entries.head
    84     def head: Entry = sorted_entries.head
    86     def order: Long = - head.timing.elapsed.ms
    85     def order: Long = - head.timing.elapsed.ms
    87 
    86 
    88     def finished_entries: List[Entry] = sorted_entries.filter(_.finished)
    87     def finished_entries: List[Entry] = sorted_entries.filter(_.finished)
    89     def finished_entries_size: Int =
    88     def finished_entries_size: Int = finished_entries.map(_.date).toSet.size
    90       finished_entries.map(entry => entry.pull_date.unix_epoch).toSet.size
       
    91 
    89 
    92     def check_timing: Boolean = finished_entries_size >= 3
    90     def check_timing: Boolean = finished_entries_size >= 3
    93     def check_heap: Boolean =
    91     def check_heap: Boolean =
    94       finished_entries_size >= 3 &&
    92       finished_entries_size >= 3 &&
    95       finished_entries.forall(entry =>
    93       finished_entries.forall(entry =>
   101     {
    99     {
   102       val header =
   100       val header =
   103         List("session_name",
   101         List("session_name",
   104           "chapter",
   102           "chapter",
   105           "pull_date",
   103           "pull_date",
       
   104           "afp_pull_date",
   106           "isabelle_version",
   105           "isabelle_version",
   107           "afp_version",
   106           "afp_version",
   108           "timing_elapsed",
   107           "timing_elapsed",
   109           "timing_cpu",
   108           "timing_cpu",
   110           "timing_gc",
   109           "timing_gc",
   119       val records =
   118       val records =
   120         for (entry <- entries) yield {
   119         for (entry <- entries) yield {
   121           CSV.Record(name,
   120           CSV.Record(name,
   122             entry.chapter,
   121             entry.chapter,
   123             date_format(entry.pull_date),
   122             date_format(entry.pull_date),
       
   123             entry.afp_pull_date match { case Some(date) => date_format(date) case None => "" },
   124             entry.isabelle_version,
   124             entry.isabelle_version,
   125             entry.afp_version,
   125             entry.afp_version,
   126             entry.timing.elapsed.ms,
   126             entry.timing.elapsed.ms,
   127             entry.timing.cpu.ms,
   127             entry.timing.cpu.ms,
   128             entry.timing.gc.ms,
   128             entry.timing.gc.ms,
   138     }
   138     }
   139   }
   139   }
   140   sealed case class Entry(
   140   sealed case class Entry(
   141     chapter: String,
   141     chapter: String,
   142     pull_date: Date,
   142     pull_date: Date,
       
   143     afp_pull_date: Option[Date],
   143     isabelle_version: String,
   144     isabelle_version: String,
   144     afp_version: String,
   145     afp_version: String,
   145     timing: Timing,
   146     timing: Timing,
   146     ml_timing: Timing,
   147     ml_timing: Timing,
   147     maximum_heap: Long,
   148     maximum_heap: Long,
   148     average_heap: Long,
   149     average_heap: Long,
   149     stored_heap: Long,
   150     stored_heap: Long,
   150     status: Build_Log.Session_Status.Value,
   151     status: Build_Log.Session_Status.Value,
   151     errors: List[String])
   152     errors: List[String])
   152   {
   153   {
       
   154     val date: Long = (afp_pull_date getOrElse pull_date).unix_epoch
       
   155 
   153     def finished: Boolean = status == Build_Log.Session_Status.finished
   156     def finished: Boolean = status == Build_Log.Session_Status.finished
   154     def failed: Boolean = status == Build_Log.Session_Status.failed
   157     def failed: Boolean = status == Build_Log.Session_Status.failed
   155 
   158 
   156     def present_errors(name: String): XML.Body =
   159     def present_errors(name: String): XML.Body =
   157     {
   160     {
   200         progress.echo("input " + quote(profile.description))
   203         progress.echo("input " + quote(profile.description))
   201 
   204 
   202         val afp = profile.afp
   205         val afp = profile.afp
   203         val columns =
   206         val columns =
   204           List(
   207           List(
   205             Build_Log.Data.pull_date(afp),
   208             Build_Log.Data.pull_date(afp = false),
       
   209             Build_Log.Data.pull_date(afp = true),
   206             Build_Log.Prop.build_host,
   210             Build_Log.Prop.build_host,
   207             Build_Log.Prop.isabelle_version,
   211             Build_Log.Prop.isabelle_version,
   208             Build_Log.Prop.afp_version,
   212             Build_Log.Prop.afp_version,
   209             Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
   213             Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
   210             Build_Log.Settings.ML_PLATFORM,
   214             Build_Log.Settings.ML_PLATFORM,
   267                 heading = session_name + print_version(isabelle_version, afp_version, chapter))
   271                 heading = session_name + print_version(isabelle_version, afp_version, chapter))
   268 
   272 
   269             val entry =
   273             val entry =
   270               Entry(
   274               Entry(
   271                 chapter = chapter,
   275                 chapter = chapter,
   272                 pull_date = res.date(Build_Log.Data.pull_date(afp)),
   276                 pull_date = res.date(Build_Log.Data.pull_date(afp = false)),
       
   277                 afp_pull_date =
       
   278                   if (afp) res.get_date(Build_Log.Data.pull_date(afp = true)) else None,
   273                 isabelle_version = isabelle_version,
   279                 isabelle_version = isabelle_version,
   274                 afp_version = afp_version,
   280                 afp_version = afp_version,
   275                 timing =
   281                 timing =
   276                   res.timing(
   282                   res.timing(
   277                     Build_Log.Data.timing_elapsed,
   283                     Build_Log.Data.timing_elapsed,
   374               def plot_name(kind: String): String = session.name + "_" + kind + ".png"
   380               def plot_name(kind: String): String = session.name + "_" + kind + ".png"
   375 
   381 
   376               File.write(data_file,
   382               File.write(data_file,
   377                 cat_lines(
   383                 cat_lines(
   378                   session.finished_entries.map(entry =>
   384                   session.finished_entries.map(entry =>
   379                     List(entry.pull_date.unix_epoch,
   385                     List(entry.date,
   380                       entry.timing.elapsed.minutes,
   386                       entry.timing.elapsed.minutes,
   381                       entry.timing.resources.minutes,
   387                       entry.timing.resources.minutes,
   382                       entry.ml_timing.elapsed.minutes,
   388                       entry.ml_timing.elapsed.minutes,
   383                       entry.ml_timing.resources.minutes,
   389                       entry.ml_timing.resources.minutes,
   384                       entry.maximum_heap,
   390                       entry.maximum_heap,