src/Pure/Tools/build_log.scala
author wenzelm
Fri Oct 07 21:09:43 2016 +0200 (2016-10-07)
changeset 64091 f8dfba90e73f
parent 64090 5a68280112b3
child 64092 95469c544b82
permissions -rw-r--r--
more liberal parsing for old AFP logs;
     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 a => a })))
   212 
   213     object Strict_Date
   214     {
   215       def unapply(s: String): Some[Date] = Some(Date_Format.parse(s))
   216     }
   217 
   218     val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   219     val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   220     val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   221     val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   222     val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   223   }
   224 
   225   private def parse_header(log_file: Log_File): Header =
   226   {
   227     def parse_afp(start: Date, hostname: String): Header =
   228     {
   229       val start_date = Field.build_start -> start.toString
   230       val end_date =
   231         log_file.lines.last match {
   232           case AFP.Test_End(AFP.Strict_Date(end_date)) =>
   233             List(Field.build_end -> end_date.toString)
   234           case _ => Nil
   235         }
   236 
   237       val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
   238 
   239       val isabelle_version =
   240         log_file.find_match(AFP.Isabelle_Version).map(Field.isabelle_version -> _)
   241 
   242       val afp_version =
   243         log_file.find_match(AFP.AFP_Version).map(Field.afp_version -> _)
   244 
   245       Header(Header_Kind.AFP_TEST,
   246         start_date :: end_date ::: build_host ::: isabelle_version.toList ::: afp_version.toList,
   247         log_file.get_settings(Settings.all_settings))
   248     }
   249 
   250     log_file.lines match {
   251       case AFP.Test_Start(AFP.Strict_Date(start_date), hostname) :: _ =>
   252         parse_afp(start_date, hostname)
   253       case AFP.Test_Start_Old(AFP.Strict_Date(start_date)) :: _ =>
   254         parse_afp(start_date, "")
   255       case _ => log_file.err("cannot detect log header format")
   256     }
   257   }
   258 
   259 
   260   /* build info: produced by isabelle build */
   261 
   262   object Session_Status extends Enumeration
   263   {
   264     val EXISTING = Value("existing")
   265     val FINISHED = Value("finished")
   266     val FAILED = Value("failed")
   267     val CANCELLED = Value("cancelled")
   268   }
   269 
   270   sealed case class Session_Entry(
   271     chapter: String,
   272     groups: List[String],
   273     threads: Option[Int],
   274     timing: Timing,
   275     ml_timing: Timing,
   276     status: Session_Status.Value)
   277   {
   278     def finished: Boolean = status == Session_Status.FINISHED
   279   }
   280 
   281   sealed case class Build_Info(sessions: Map[String, Session_Entry])
   282   {
   283     def session(name: String): Session_Entry = sessions(name)
   284     def get_session(name: String): Option[Session_Entry] = sessions.get(name)
   285 
   286     def get_default[A](name: String, f: Session_Entry => A, x: A): A =
   287       get_session(name) match {
   288         case Some(entry) => f(entry)
   289         case None => x
   290       }
   291 
   292     def finished(name: String): Boolean = get_default(name, _.finished, false)
   293     def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
   294     def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   295   }
   296 
   297   private def parse_build_info(log_file: Log_File): Build_Info =
   298   {
   299     object Chapter_Name
   300     {
   301       def unapply(s: String): Some[(String, String)] =
   302         space_explode('/', s) match {
   303           case List(chapter, name) => Some((chapter, name))
   304           case _ => Some(("", s))
   305         }
   306     }
   307 
   308     val Session_No_Groups = new Regex("""^Session (\S+)$""")
   309     val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   310     val Session_Finished1 =
   311       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   312     val Session_Finished2 =
   313       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   314     val Session_Timing =
   315       new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   316     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
   317     val Session_Failed = new Regex("""^(\S+) FAILED""")
   318     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   319 
   320     var chapter = Map.empty[String, String]
   321     var groups = Map.empty[String, List[String]]
   322     var threads = Map.empty[String, Int]
   323     var timing = Map.empty[String, Timing]
   324     var ml_timing = Map.empty[String, Timing]
   325     var started = Set.empty[String]
   326     var failed = Set.empty[String]
   327     var cancelled = Set.empty[String]
   328     def all_sessions: Set[String] =
   329       chapter.keySet ++ groups.keySet ++ threads.keySet ++
   330       timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
   331 
   332 
   333     for (line <- log_file.lines) {
   334       line match {
   335         case Session_No_Groups(Chapter_Name(chapt, name)) =>
   336           chapter += (name -> chapt)
   337           groups += (name -> Nil)
   338         case Session_Groups(Chapter_Name(chapt, name), grps) =>
   339           chapter += (name -> chapt)
   340           groups += (name -> Word.explode(grps))
   341         case Session_Started(name) =>
   342           started += name
   343         case Session_Finished1(name,
   344             Value.Int(e1), Value.Int(e2), Value.Int(e3),
   345             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   346           val elapsed = Time.hms(e1, e2, e3)
   347           val cpu = Time.hms(c1, c2, c3)
   348           timing += (name -> Timing(elapsed, cpu, Time.zero))
   349         case Session_Finished2(name,
   350             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   351           val elapsed = Time.hms(e1, e2, e3)
   352           timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   353         case Session_Timing(name,
   354             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   355           val elapsed = Time.seconds(e)
   356           val cpu = Time.seconds(c)
   357           val gc = Time.seconds(g)
   358           ml_timing += (name -> Timing(elapsed, cpu, gc))
   359           threads += (name -> t)
   360         case _ =>
   361       }
   362     }
   363 
   364     val sessions =
   365       Map(
   366         (for (name <- all_sessions.toList) yield {
   367           val status =
   368             if (failed(name)) Session_Status.FAILED
   369             else if (cancelled(name)) Session_Status.CANCELLED
   370             else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
   371               Session_Status.FINISHED
   372             else if (started(name)) Session_Status.FAILED
   373             else Session_Status.EXISTING
   374           val entry =
   375             Session_Entry(
   376               chapter.getOrElse(name, ""),
   377               groups.getOrElse(name, Nil),
   378               threads.get(name),
   379               timing.getOrElse(name, Timing.zero),
   380               ml_timing.getOrElse(name, Timing.zero),
   381               status)
   382           (name -> entry)
   383         }):_*)
   384     Build_Info(sessions)
   385   }
   386 }