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