src/Pure/Tools/build_log.scala
author wenzelm
Fri Oct 07 21:46:42 2016 +0200 (2016-10-07)
changeset 64094 629558a1ecf5
parent 64092 95469c544b82
child 64095 1a6d37c31df9
permissions -rw-r--r--
tuned;
     1 /*  Title:      Pure/Tools/build_log.scala
     2     Author:     Makarius
     3 
     4 Build log parsing for historic versions, back to "build_history_base".
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{File => JFile}
    11 import java.time.ZonedDateTime
    12 import java.time.format.{DateTimeFormatter, DateTimeParseException}
    13 
    14 import scala.collection.mutable
    15 import scala.util.matching.Regex
    16 
    17 
    18 object Build_Log
    19 {
    20   /** settings **/
    21 
    22   object Settings
    23   {
    24     val build_settings = List("ISABELLE_BUILD_OPTIONS")
    25     val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    26     val all_settings = build_settings ::: ml_settings
    27 
    28     type Entry = (String, String)
    29     type T = List[Entry]
    30 
    31     object Entry
    32     {
    33       def unapply(s: String): Option[Entry] =
    34         s.indexOf('=') match {
    35           case -1 => None
    36           case i =>
    37             val a = s.substring(0, i)
    38             val b = Library.perhaps_unquote(s.substring(i + 1))
    39             Some((a, b))
    40         }
    41       def apply(a: String, b: String): String = a + "=" + quote(b)
    42       def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    43     }
    44 
    45     def show(): String =
    46       cat_lines(
    47         build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
    48   }
    49 
    50 
    51   /** log file **/
    52 
    53   object Log_File
    54   {
    55     def apply(name: String, lines: List[String]): Log_File =
    56       new Log_File(name, lines)
    57 
    58     def apply(name: String, text: String): Log_File =
    59       Log_File(name, Library.trim_split_lines(text))
    60 
    61     def apply(file: JFile): Log_File =
    62     {
    63       val name = file.getName
    64       val (base_name, text) =
    65         Library.try_unsuffix(".gz", name) match {
    66           case Some(base_name) => (base_name, File.read_gzip(file))
    67           case None =>
    68             Library.try_unsuffix(".xz", name) match {
    69               case Some(base_name) => (base_name, File.read_xz(file))
    70               case None => (name, File.read(file))
    71             }
    72           }
    73       apply(base_name, text)
    74     }
    75 
    76     def apply(path: Path): Log_File = apply(path.file)
    77   }
    78 
    79   class Log_File private(val name: String, val lines: List[String])
    80   {
    81     log_file =>
    82 
    83     override def toString: String = name
    84 
    85     def text: String = cat_lines(lines)
    86 
    87     def err(msg: String): Nothing =
    88       error("Error in log file " + quote(name) + ": " + msg)
    89 
    90 
    91     /* inlined content */
    92 
    93     def find[A](f: String => Option[A]): Option[A] =
    94       lines.iterator.map(f).find(_.isDefined).map(_.get)
    95 
    96     def find_match(regex: Regex): Option[String] =
    97       lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
    98         map(res => res.get.head)
    99 
   100 
   101     /* settings */
   102 
   103     def get_setting(a: String): Option[Settings.Entry] =
   104       lines.find(_.startsWith(a + "=")) match {
   105         case Some(line) => Settings.Entry.unapply(line)
   106         case None => None
   107       }
   108 
   109     def get_settings(as: List[String]): Settings.T =
   110       for { a <- as; entry <- get_setting(a) } yield entry
   111 
   112 
   113     /* properties (YXML) */
   114 
   115     val xml_cache = new XML.Cache()
   116 
   117     def parse_props(text: String): Properties.T =
   118       xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
   119 
   120     def filter_props(prefix: String): List[Properties.T] =
   121       for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s)
   122 
   123     def find_line(prefix: String): Option[String] =
   124       find(Library.try_unprefix(prefix, _))
   125 
   126     def find_props(prefix: String): Option[Properties.T] =
   127       find_line(prefix).map(parse_props(_))
   128 
   129 
   130     /* parse various formats */
   131 
   132     def parse_session_info(
   133         default_name: String = "",
   134         command_timings: Boolean = false,
   135         ml_statistics: Boolean = false,
   136         task_statistics: Boolean = false): Session_Info =
   137       Build_Log.parse_session_info(
   138         log_file, default_name, command_timings, ml_statistics, task_statistics)
   139 
   140     def parse_header(): Header = Build_Log.parse_header(log_file)
   141 
   142     def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
   143   }
   144 
   145 
   146   /* session log: produced by "isabelle build" */
   147 
   148   sealed case class Session_Info(
   149     session_name: String,
   150     session_timing: Properties.T,
   151     command_timings: List[Properties.T],
   152     ml_statistics: List[Properties.T],
   153     task_statistics: List[Properties.T])
   154 
   155   private def parse_session_info(
   156     log_file: Log_File,
   157     default_name: String,
   158     command_timings: Boolean,
   159     ml_statistics: Boolean,
   160     task_statistics: Boolean): Session_Info =
   161   {
   162     val xml_cache = new XML.Cache()
   163 
   164     val session_name =
   165       log_file.find_line("\fSession.name = ") match {
   166         case None => default_name
   167         case Some(name) if default_name == "" || default_name == name => name
   168         case Some(name) => log_file.err("log from different session " + quote(name))
   169       }
   170     val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   171     val command_timings_ =
   172       if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   173     val ml_statistics_ =
   174       if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   175     val task_statistics_ =
   176       if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   177 
   178     Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   179   }
   180 
   181 
   182   /* header and meta data */
   183 
   184   object Header_Kind extends Enumeration
   185   {
   186     val ISATEST = Value("isatest")
   187     val AFP_TEST = Value("afp-test")
   188     val JENKINS = Value("jenkins")
   189   }
   190 
   191   sealed case class Header(
   192     kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
   193 
   194   object Field
   195   {
   196     val build_host = "build_host"
   197     val build_start = "build_start"
   198     val build_end = "build_end"
   199     val isabelle_version = "isabelle_version"
   200     val afp_version = "afp_version"
   201   }
   202 
   203   object AFP
   204   {
   205     val Date_Format =
   206       Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
   207         // workaround for jdk-8u102
   208         s => Word.implode(Word.explode(s).map({
   209           case "CET" | "MET" => "GMT+1"
   210           case "CEST" | "MEST" => "GMT+2"
   211           case "EST" => "GMT+1"  // FIXME ??
   212           case a => a })))
   213 
   214     val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   215     val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   216     val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   217     val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   218     val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   219   }
   220 
   221   private def parse_header(log_file: Log_File): Header =
   222   {
   223     def parse_afp(start: Date, hostname: String): Header =
   224     {
   225       val start_date = Field.build_start -> start.toString
   226       val end_date =
   227         log_file.lines.last match {
   228           case AFP.Test_End(AFP.Date_Format.Strict(end_date)) =>
   229             List(Field.build_end -> end_date.toString)
   230           case _ => Nil
   231         }
   232 
   233       val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
   234 
   235       val isabelle_version =
   236         log_file.find_match(AFP.Isabelle_Version).map(Field.isabelle_version -> _)
   237 
   238       val afp_version =
   239         log_file.find_match(AFP.AFP_Version).map(Field.afp_version -> _)
   240 
   241       Header(Header_Kind.AFP_TEST,
   242         start_date :: end_date ::: build_host ::: isabelle_version.toList ::: afp_version.toList,
   243         log_file.get_settings(Settings.all_settings))
   244     }
   245 
   246     log_file.lines match {
   247       case AFP.Test_Start(AFP.Date_Format.Strict(start_date), hostname) :: _ =>
   248         parse_afp(start_date, hostname)
   249       case AFP.Test_Start_Old(AFP.Date_Format.Strict(start_date)) :: _ =>
   250         parse_afp(start_date, "")
   251       case _ => log_file.err("cannot detect log header format")
   252     }
   253   }
   254 
   255 
   256   /* build info: produced by isabelle build */
   257 
   258   object Session_Status extends Enumeration
   259   {
   260     val EXISTING = Value("existing")
   261     val FINISHED = Value("finished")
   262     val FAILED = Value("failed")
   263     val CANCELLED = Value("cancelled")
   264   }
   265 
   266   sealed case class Session_Entry(
   267     chapter: String,
   268     groups: List[String],
   269     threads: Option[Int],
   270     timing: Timing,
   271     ml_timing: Timing,
   272     status: Session_Status.Value)
   273   {
   274     def finished: Boolean = status == Session_Status.FINISHED
   275   }
   276 
   277   sealed case class Build_Info(sessions: Map[String, Session_Entry])
   278   {
   279     def session(name: String): Session_Entry = sessions(name)
   280     def get_session(name: String): Option[Session_Entry] = sessions.get(name)
   281 
   282     def get_default[A](name: String, f: Session_Entry => A, x: A): A =
   283       get_session(name) match {
   284         case Some(entry) => f(entry)
   285         case None => x
   286       }
   287 
   288     def finished(name: String): Boolean = get_default(name, _.finished, false)
   289     def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
   290     def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   291   }
   292 
   293   private def parse_build_info(log_file: Log_File): Build_Info =
   294   {
   295     object Chapter_Name
   296     {
   297       def unapply(s: String): Some[(String, String)] =
   298         space_explode('/', s) match {
   299           case List(chapter, name) => Some((chapter, name))
   300           case _ => Some(("", s))
   301         }
   302     }
   303 
   304     val Session_No_Groups = new Regex("""^Session (\S+)$""")
   305     val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   306     val Session_Finished1 =
   307       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   308     val Session_Finished2 =
   309       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   310     val Session_Timing =
   311       new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   312     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
   313     val Session_Failed = new Regex("""^(\S+) FAILED""")
   314     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   315 
   316     var chapter = Map.empty[String, String]
   317     var groups = Map.empty[String, List[String]]
   318     var threads = Map.empty[String, Int]
   319     var timing = Map.empty[String, Timing]
   320     var ml_timing = Map.empty[String, Timing]
   321     var started = Set.empty[String]
   322     var failed = Set.empty[String]
   323     var cancelled = Set.empty[String]
   324     def all_sessions: Set[String] =
   325       chapter.keySet ++ groups.keySet ++ threads.keySet ++
   326       timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
   327 
   328 
   329     for (line <- log_file.lines) {
   330       line match {
   331         case Session_No_Groups(Chapter_Name(chapt, name)) =>
   332           chapter += (name -> chapt)
   333           groups += (name -> Nil)
   334         case Session_Groups(Chapter_Name(chapt, name), grps) =>
   335           chapter += (name -> chapt)
   336           groups += (name -> Word.explode(grps))
   337         case Session_Started(name) =>
   338           started += name
   339         case Session_Finished1(name,
   340             Value.Int(e1), Value.Int(e2), Value.Int(e3),
   341             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   342           val elapsed = Time.hms(e1, e2, e3)
   343           val cpu = Time.hms(c1, c2, c3)
   344           timing += (name -> Timing(elapsed, cpu, Time.zero))
   345         case Session_Finished2(name,
   346             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   347           val elapsed = Time.hms(e1, e2, e3)
   348           timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   349         case Session_Timing(name,
   350             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   351           val elapsed = Time.seconds(e)
   352           val cpu = Time.seconds(c)
   353           val gc = Time.seconds(g)
   354           ml_timing += (name -> Timing(elapsed, cpu, gc))
   355           threads += (name -> t)
   356         case _ =>
   357       }
   358     }
   359 
   360     val sessions =
   361       Map(
   362         (for (name <- all_sessions.toList) yield {
   363           val status =
   364             if (failed(name)) Session_Status.FAILED
   365             else if (cancelled(name)) Session_Status.CANCELLED
   366             else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
   367               Session_Status.FINISHED
   368             else if (started(name)) Session_Status.FAILED
   369             else Session_Status.EXISTING
   370           val entry =
   371             Session_Entry(
   372               chapter.getOrElse(name, ""),
   373               groups.getOrElse(name, Nil),
   374               threads.get(name),
   375               timing.getOrElse(name, Timing.zero),
   376               ml_timing.getOrElse(name, Timing.zero),
   377               status)
   378           (name -> entry)
   379         }):_*)
   380     Build_Info(sessions)
   381   }
   382 }