clarified parse_build_info: isabelle build output;
authorwenzelm
Fri Oct 07 17:12:47 2016 +0200 (2016-10-07)
changeset 640851c451e5c145f
parent 64084 bca58a11efde
child 64086 ac7ae5067783
clarified parse_build_info: isabelle build output;
clarified Session_Status;
tuned signature;
src/Pure/Tools/build_log.scala
src/Pure/Tools/build_stats.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 16:50:47 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 17:12:47 2016 +0200
     1.3 @@ -119,16 +119,16 @@
     1.4      /* parse various formats */
     1.5  
     1.6      def parse_session_info(
     1.7 -        session_name: String,
     1.8 +        default_name: String = "",
     1.9          command_timings: Boolean = false,
    1.10          ml_statistics: Boolean = false,
    1.11          task_statistics: Boolean = false): Session_Info =
    1.12        Build_Log.parse_session_info(
    1.13 -        log_file, session_name, command_timings, ml_statistics, task_statistics)
    1.14 +        log_file, default_name, command_timings, ml_statistics, task_statistics)
    1.15  
    1.16 -    def parse_header: Header = Build_Log.parse_header(log_file)
    1.17 +    def parse_header(): Header = Build_Log.parse_header(log_file)
    1.18  
    1.19 -    def parse_info: Info = Build_Log.parse_info(log_file)
    1.20 +    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
    1.21    }
    1.22  
    1.23  
    1.24 @@ -230,68 +230,128 @@
    1.25      }
    1.26    }
    1.27  
    1.28 +
    1.29 +  /* build info: produced by isabelle build */
    1.30 +
    1.31    object Session_Status extends Enumeration
    1.32    {
    1.33 -    val UNKNOWN = Value("unknown")
    1.34 +    val EXISTING = Value("existing")
    1.35      val FINISHED = Value("finished")
    1.36      val FAILED = Value("failed")
    1.37      val CANCELLED = Value("cancelled")
    1.38    }
    1.39  
    1.40 -
    1.41 -  /* main log: produced by isatest, afp-test, jenkins etc. */
    1.42 +  sealed case class Session_Entry(
    1.43 +    chapter: String,
    1.44 +    groups: List[String],
    1.45 +    threads: Option[Int],
    1.46 +    timing: Option[Timing],
    1.47 +    ml_timing: Option[Timing],
    1.48 +    status: Session_Status.Value)
    1.49 +  {
    1.50 +    def ok: Boolean = status == Session_Status.EXISTING || status == Session_Status.FINISHED
    1.51 +    def finished: Boolean = status == Session_Status.FINISHED
    1.52 +  }
    1.53  
    1.54 -  sealed case class Info(
    1.55 -    settings: List[(String, String)],
    1.56 -    finished: Map[String, Timing],
    1.57 -    timing: Map[String, Timing],
    1.58 -    threads: Map[String, Int])
    1.59 +  sealed case class Build_Info(sessions: Map[String, Session_Entry])
    1.60    {
    1.61 -    val sessions: Set[String] = finished.keySet ++ timing.keySet
    1.62 +    def session(name: String): Session_Entry = sessions(name)
    1.63 +    def get_session(name: String): Option[Session_Entry] = sessions.get(name)
    1.64  
    1.65 -    override def toString: String =
    1.66 -      sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")")
    1.67 +    def finished(name: String): Boolean =
    1.68 +      get_session(name) match {
    1.69 +        case Some(entry) => entry.finished
    1.70 +        case None => false
    1.71 +      }
    1.72 +
    1.73 +    def timing(name: String): Timing =
    1.74 +      (for (entry <- get_session(name); t <- entry.timing) yield t) getOrElse Timing.zero
    1.75 +
    1.76 +    def ml_timing(name: String): Timing =
    1.77 +      (for (entry <- get_session(name); t <- entry.ml_timing) yield t) getOrElse Timing.zero
    1.78    }
    1.79  
    1.80 -  private val Session_Finished1 =
    1.81 -    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
    1.82 -  private val Session_Finished2 =
    1.83 -    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
    1.84 -  private val Session_Timing =
    1.85 -    new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
    1.86 +  private def parse_build_info(log_file: Log_File): Build_Info =
    1.87 +  {
    1.88 +    object Chapter_Name
    1.89 +    {
    1.90 +      def unapply(s: String): Some[(String, String)] =
    1.91 +        space_explode('/', s) match {
    1.92 +          case List(chapter, name) => Some((chapter, name))
    1.93 +          case _ => Some(("", s))
    1.94 +        }
    1.95 +    }
    1.96  
    1.97 -  private def parse_info(log_file: Log_File): Info =
    1.98 -  {
    1.99 -    val settings = new mutable.ListBuffer[(String, String)]
   1.100 -    var finished = Map.empty[String, Timing]
   1.101 +    val Session_No_Groups = new Regex("""^Session (\S+)$""")
   1.102 +    val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   1.103 +    val Session_Finished1 =
   1.104 +      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   1.105 +    val Session_Finished2 =
   1.106 +      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   1.107 +    val Session_Timing =
   1.108 +      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   1.109 +    val Session_Failed = new Regex("""^(\S+) FAILED""")
   1.110 +    val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   1.111 +
   1.112 +    var chapter = Map.empty[String, String]
   1.113 +    var groups = Map.empty[String, List[String]]
   1.114 +    var threads = Map.empty[String, Int]
   1.115      var timing = Map.empty[String, Timing]
   1.116 -    var threads = Map.empty[String, Int]
   1.117 +    var ml_timing = Map.empty[String, Timing]
   1.118 +    var failed = Set.empty[String]
   1.119 +    var cancelled = Set.empty[String]
   1.120 +    def all_sessions: Set[String] =
   1.121 +      chapter.keySet ++ groups.keySet ++ threads.keySet ++
   1.122 +      timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled
   1.123 +
   1.124  
   1.125      for (line <- log_file.lines) {
   1.126        line match {
   1.127 +        case Session_No_Groups(Chapter_Name(chapt, name)) =>
   1.128 +          chapter += (name -> chapt)
   1.129 +          groups += (name -> Nil)
   1.130 +        case Session_Groups(Chapter_Name(chapt, name), grps) =>
   1.131 +          chapter += (name -> chapt)
   1.132 +          groups += (name -> Word.explode(grps))
   1.133          case Session_Finished1(name,
   1.134              Value.Int(e1), Value.Int(e2), Value.Int(e3),
   1.135              Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   1.136            val elapsed = Time.hms(e1, e2, e3)
   1.137            val cpu = Time.hms(c1, c2, c3)
   1.138 -          finished += (name -> Timing(elapsed, cpu, Time.zero))
   1.139 +          timing += (name -> Timing(elapsed, cpu, Time.zero))
   1.140          case Session_Finished2(name,
   1.141              Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   1.142            val elapsed = Time.hms(e1, e2, e3)
   1.143 -          finished += (name -> Timing(elapsed, Time.zero, Time.zero))
   1.144 +          timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   1.145          case Session_Timing(name,
   1.146              Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   1.147            val elapsed = Time.seconds(e)
   1.148            val cpu = Time.seconds(c)
   1.149            val gc = Time.seconds(g)
   1.150 -          timing += (name -> Timing(elapsed, cpu, gc))
   1.151 +          ml_timing += (name -> Timing(elapsed, cpu, gc))
   1.152            threads += (name -> t)
   1.153 -        case Settings.Entry(a, b) if Settings.all_settings.contains(a) =>
   1.154 -          settings += (a -> b)
   1.155          case _ =>
   1.156        }
   1.157      }
   1.158  
   1.159 -    Info(settings.toList, finished, timing, threads)
   1.160 +    val sessions =
   1.161 +      Map(
   1.162 +        (for (name <- all_sessions.toList) yield {
   1.163 +          val status =
   1.164 +            if (failed(name)) Session_Status.FAILED
   1.165 +            else if (cancelled(name)) Session_Status.CANCELLED
   1.166 +            else if (timing.isDefinedAt(name)) Session_Status.FINISHED
   1.167 +            else Session_Status.EXISTING
   1.168 +          val entry =
   1.169 +            Session_Entry(
   1.170 +              chapter.getOrElse(name, ""),
   1.171 +              groups.getOrElse(name, Nil),
   1.172 +              threads.get(name),
   1.173 +              timing.get(name),
   1.174 +              ml_timing.get(name),
   1.175 +              status)
   1.176 +          (name -> entry)
   1.177 +        }):_*)
   1.178 +    Build_Info(sessions)
   1.179    }
   1.180  }
     2.1 --- a/src/Pure/Tools/build_stats.scala	Fri Oct 07 16:50:47 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_stats.scala	Fri Oct 07 17:12:47 2016 +0200
     2.3 @@ -29,16 +29,14 @@
     2.4  
     2.5      val all_infos =
     2.6        Par_List.map((job_info: CI_API.Job_Info) =>
     2.7 -        (job_info.timestamp / 1000, job_info.read_output.parse_info), job_infos)
     2.8 +        (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos)
     2.9      val all_sessions =
    2.10        (Set.empty[String] /: all_infos)(
    2.11 -        { case (s, (_, info)) => s ++ info.sessions })
    2.12 +        { case (s, (_, info)) => s ++ info.sessions.keySet })
    2.13  
    2.14 -    def check_threshold(info: Build_Log.Info, session: String): Boolean =
    2.15 -      info.finished.get(session) match {
    2.16 -        case Some(t) => t.elapsed >= elapsed_threshold
    2.17 -        case None => false
    2.18 -      }
    2.19 +    def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
    2.20 +      (for (entry <- info.get_session(session); t <- entry.timing)
    2.21 +        yield t.elapsed >= elapsed_threshold) getOrElse false
    2.22  
    2.23      val sessions =
    2.24        for {
    2.25 @@ -51,12 +49,16 @@
    2.26        Isabelle_System.with_tmp_file(session, "png") { data_file =>
    2.27          Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
    2.28            val data =
    2.29 -            for { (t, info) <- all_infos if info.finished.isDefinedAt(session) }
    2.30 +            for { (t, info) <- all_infos if info.finished(session) }
    2.31              yield {
    2.32 -              val finished = info.finished.getOrElse(session, Timing.zero)
    2.33 -              val timing = info.timing.getOrElse(session, Timing.zero)
    2.34 -              List(t.toString, finished.elapsed.minutes, finished.cpu.minutes,
    2.35 -                timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ")
    2.36 +              val timing1 = info.timing(session)
    2.37 +              val timing2 = info.ml_timing(session)
    2.38 +              List(t.toString,
    2.39 +                timing1.elapsed.minutes,
    2.40 +                timing1.cpu.minutes,
    2.41 +                timing2.elapsed.minutes,
    2.42 +                timing2.cpu.minutes,
    2.43 +                timing2.gc.minutes).mkString(" ")
    2.44              }
    2.45            File.write(data_file, cat_lines(data))
    2.46