src/Pure/Tools/build_log.scala
author wenzelm
Fri Oct 07 22:58:24 2016 +0200 (2016-10-07)
changeset 64095 1a6d37c31df9
parent 64094 629558a1ecf5
child 64096 5edeb60a7ec5
permissions -rw-r--r--
support for isatest format;
     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   val Date_Format =
   185     Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
   186       // workaround for jdk-8u102
   187       s => Word.implode(Word.explode(s).map({
   188         case "CET" | "MET" => "GMT+1"
   189         case "CEST" | "MEST" => "GMT+2"
   190         case "EST" => "GMT+1"  // FIXME ??
   191         case a => a })))
   192 
   193   object Header_Kind extends Enumeration
   194   {
   195     val ISATEST = Value("isatest")
   196     val AFP_TEST = Value("afp-test")
   197     val JENKINS = Value("jenkins")
   198   }
   199 
   200   sealed case class Header(
   201     kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
   202 
   203   object Field
   204   {
   205     val build_host = "build_host"
   206     val build_start = "build_start"
   207     val build_end = "build_end"
   208     val isabelle_version = "isabelle_version"
   209     val afp_version = "afp_version"
   210   }
   211 
   212   object Isatest
   213   {
   214     val Test_Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
   215     val Test_End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
   216     val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""")
   217     val No_AFP_Version = new Regex("""$.""")
   218   }
   219 
   220   object AFP
   221   {
   222     val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   223     val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   224     val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   225     val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   226     val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   227   }
   228 
   229   private def parse_header(log_file: Log_File): Header =
   230   {
   231     def parse(kind: Header_Kind.Value, start: Date, hostname: String,
   232       Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
   233     {
   234       val start_date = Field.build_start -> start.toString
   235       val end_date =
   236         log_file.lines.last match {
   237           case Test_End(Date_Format.Strict(end_date)) =>
   238             List(Field.build_end -> end_date.toString)
   239           case _ => Nil
   240         }
   241 
   242       val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
   243 
   244       val isabelle_version =
   245         log_file.find_match(Isabelle_Version).map(Field.isabelle_version -> _)
   246 
   247       val afp_version =
   248         log_file.find_match(AFP_Version).map(Field.afp_version -> _)
   249 
   250       Header(kind,
   251         start_date :: end_date ::: build_host :::
   252           isabelle_version.toList ::: afp_version.toList,
   253         log_file.get_settings(Settings.all_settings))
   254     }
   255 
   256     log_file.lines match {
   257       case Isatest.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
   258         parse(Header_Kind.ISATEST, start, hostname,
   259           Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
   260       case AFP.Test_Start(Date_Format.Strict(start), hostname) :: _ =>
   261         parse(Header_Kind.AFP_TEST, start, hostname,
   262           AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   263       case AFP.Test_Start_Old(Date_Format.Strict(start)) :: _ =>
   264         parse(Header_Kind.AFP_TEST, start, "",
   265           AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
   266       case _ => log_file.err("cannot detect log header format")
   267     }
   268   }
   269 
   270 
   271   /* build info: produced by isabelle build */
   272 
   273   object Session_Status extends Enumeration
   274   {
   275     val EXISTING = Value("existing")
   276     val FINISHED = Value("finished")
   277     val FAILED = Value("failed")
   278     val CANCELLED = Value("cancelled")
   279   }
   280 
   281   sealed case class Session_Entry(
   282     chapter: String,
   283     groups: List[String],
   284     threads: Option[Int],
   285     timing: Timing,
   286     ml_timing: Timing,
   287     status: Session_Status.Value)
   288   {
   289     def finished: Boolean = status == Session_Status.FINISHED
   290   }
   291 
   292   sealed case class Build_Info(sessions: Map[String, Session_Entry])
   293   {
   294     def session(name: String): Session_Entry = sessions(name)
   295     def get_session(name: String): Option[Session_Entry] = sessions.get(name)
   296 
   297     def get_default[A](name: String, f: Session_Entry => A, x: A): A =
   298       get_session(name) match {
   299         case Some(entry) => f(entry)
   300         case None => x
   301       }
   302 
   303     def finished(name: String): Boolean = get_default(name, _.finished, false)
   304     def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
   305     def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   306   }
   307 
   308   private def parse_build_info(log_file: Log_File): Build_Info =
   309   {
   310     object Chapter_Name
   311     {
   312       def unapply(s: String): Some[(String, String)] =
   313         space_explode('/', s) match {
   314           case List(chapter, name) => Some((chapter, name))
   315           case _ => Some(("", s))
   316         }
   317     }
   318 
   319     val Session_No_Groups = new Regex("""^Session (\S+)$""")
   320     val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   321     val Session_Finished1 =
   322       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   323     val Session_Finished2 =
   324       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   325     val Session_Timing =
   326       new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   327     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
   328     val Session_Failed = new Regex("""^(\S+) FAILED""")
   329     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   330 
   331     var chapter = Map.empty[String, String]
   332     var groups = Map.empty[String, List[String]]
   333     var threads = Map.empty[String, Int]
   334     var timing = Map.empty[String, Timing]
   335     var ml_timing = Map.empty[String, Timing]
   336     var started = Set.empty[String]
   337     var failed = Set.empty[String]
   338     var cancelled = Set.empty[String]
   339     def all_sessions: Set[String] =
   340       chapter.keySet ++ groups.keySet ++ threads.keySet ++
   341       timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
   342 
   343 
   344     for (line <- log_file.lines) {
   345       line match {
   346         case Session_No_Groups(Chapter_Name(chapt, name)) =>
   347           chapter += (name -> chapt)
   348           groups += (name -> Nil)
   349         case Session_Groups(Chapter_Name(chapt, name), grps) =>
   350           chapter += (name -> chapt)
   351           groups += (name -> Word.explode(grps))
   352         case Session_Started(name) =>
   353           started += name
   354         case Session_Finished1(name,
   355             Value.Int(e1), Value.Int(e2), Value.Int(e3),
   356             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   357           val elapsed = Time.hms(e1, e2, e3)
   358           val cpu = Time.hms(c1, c2, c3)
   359           timing += (name -> Timing(elapsed, cpu, Time.zero))
   360         case Session_Finished2(name,
   361             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   362           val elapsed = Time.hms(e1, e2, e3)
   363           timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   364         case Session_Timing(name,
   365             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   366           val elapsed = Time.seconds(e)
   367           val cpu = Time.seconds(c)
   368           val gc = Time.seconds(g)
   369           ml_timing += (name -> Timing(elapsed, cpu, gc))
   370           threads += (name -> t)
   371         case _ =>
   372       }
   373     }
   374 
   375     val sessions =
   376       Map(
   377         (for (name <- all_sessions.toList) yield {
   378           val status =
   379             if (failed(name)) Session_Status.FAILED
   380             else if (cancelled(name)) Session_Status.CANCELLED
   381             else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
   382               Session_Status.FINISHED
   383             else if (started(name)) Session_Status.FAILED
   384             else Session_Status.EXISTING
   385           val entry =
   386             Session_Entry(
   387               chapter.getOrElse(name, ""),
   388               groups.getOrElse(name, Nil),
   389               threads.get(name),
   390               timing.getOrElse(name, Timing.zero),
   391               ml_timing.getOrElse(name, Timing.zero),
   392               status)
   393           (name -> entry)
   394         }):_*)
   395     Build_Info(sessions)
   396   }
   397 }