src/Pure/Tools/build_log.scala
author wenzelm
Fri Oct 07 18:41:54 2016 +0200 (2016-10-07)
changeset 64090 5a68280112b3
parent 64089 10d719dbb3ee
child 64091 f8dfba90e73f
permissions -rw-r--r--
more operations;
     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): Settings.Entry =
   104       Settings.Entry.unapply(
   105         lines.find(_.startsWith(a + "=")) getOrElse err("missing " + a)).get
   106 
   107     def get_settings(as: List[String]): Settings.T = as.map(get_setting(_))
   108 
   109 
   110     /* properties (YXML) */
   111 
   112     val xml_cache = new XML.Cache()
   113 
   114     def parse_props(text: String): Properties.T =
   115       xml_cache.props(XML.Decode.properties(YXML.parse_body(text)))
   116 
   117     def filter_props(prefix: String): List[Properties.T] =
   118       for (line <- lines; s <- Library.try_unprefix(prefix, line)) yield parse_props(s)
   119 
   120     def find_line(prefix: String): Option[String] =
   121       find(Library.try_unprefix(prefix, _))
   122 
   123     def find_props(prefix: String): Option[Properties.T] =
   124       find_line(prefix).map(parse_props(_))
   125 
   126 
   127     /* parse various formats */
   128 
   129     def parse_session_info(
   130         default_name: String = "",
   131         command_timings: Boolean = false,
   132         ml_statistics: Boolean = false,
   133         task_statistics: Boolean = false): Session_Info =
   134       Build_Log.parse_session_info(
   135         log_file, default_name, command_timings, ml_statistics, task_statistics)
   136 
   137     def parse_header(): Header = Build_Log.parse_header(log_file)
   138 
   139     def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
   140   }
   141 
   142 
   143   /* session log: produced by "isabelle build" */
   144 
   145   sealed case class Session_Info(
   146     session_name: String,
   147     session_timing: Properties.T,
   148     command_timings: List[Properties.T],
   149     ml_statistics: List[Properties.T],
   150     task_statistics: List[Properties.T])
   151 
   152   private def parse_session_info(
   153     log_file: Log_File,
   154     default_name: String,
   155     command_timings: Boolean,
   156     ml_statistics: Boolean,
   157     task_statistics: Boolean): Session_Info =
   158   {
   159     val xml_cache = new XML.Cache()
   160 
   161     val session_name =
   162       log_file.find_line("\fSession.name = ") match {
   163         case None => default_name
   164         case Some(name) if default_name == "" || default_name == name => name
   165         case Some(name) => log_file.err("log from different session " + quote(name))
   166       }
   167     val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   168     val command_timings_ =
   169       if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   170     val ml_statistics_ =
   171       if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   172     val task_statistics_ =
   173       if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   174 
   175     Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   176   }
   177 
   178 
   179   /* header and meta data */
   180 
   181   object Header_Kind extends Enumeration
   182   {
   183     val ISATEST = Value("isatest")
   184     val AFP_TEST = Value("afp-test")
   185     val JENKINS = Value("jenkins")
   186   }
   187 
   188   sealed case class Header(
   189     kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
   190 
   191   object Field
   192   {
   193     val build_host = "build_host"
   194     val build_start = "build_start"
   195     val build_end = "build_end"
   196     val isabelle_version = "isabelle_version"
   197     val afp_version = "afp_version"
   198   }
   199 
   200   object AFP
   201   {
   202     val Date_Format =
   203       Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
   204         // workaround for jdk-8u102
   205         s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
   206 
   207     val Test_Start = new Regex("""^Start test (?:for \S+)? at (.+), (\S+)$""")
   208     val Test_End = new Regex("""^End test on (.+), \S+, elapsed time:.*$""")
   209     val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   210     val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   211   }
   212 
   213   private def parse_header(log_file: Log_File): Header =
   214   {
   215     log_file.lines match {
   216       case AFP.Test_Start(start, hostname) :: _ =>
   217         (start, log_file.lines.last) match {
   218           case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
   219             val isabelle_version =
   220               log_file.find_match(AFP.Isabelle_Version).map((Field.isabelle_version, _))
   221             val afp_version =
   222               log_file.find_match(AFP.AFP_Version).map((Field.afp_version, _))
   223 
   224             Header(Header_Kind.AFP_TEST,
   225               List(
   226                 Field.build_host -> hostname,
   227                 Field.build_start -> start_date.toString,
   228                 Field.build_end -> end_date.toString) :::
   229               isabelle_version.toList :::
   230               afp_version.toList,
   231               log_file.get_settings(Settings.all_settings))
   232 
   233           case _ => log_file.err("cannot detect start/end date in afp-test log")
   234         }
   235       case _ => log_file.err("cannot detect log header format")
   236     }
   237   }
   238 
   239 
   240   /* build info: produced by isabelle build */
   241 
   242   object Session_Status extends Enumeration
   243   {
   244     val EXISTING = Value("existing")
   245     val FINISHED = Value("finished")
   246     val FAILED = Value("failed")
   247     val CANCELLED = Value("cancelled")
   248   }
   249 
   250   sealed case class Session_Entry(
   251     chapter: String,
   252     groups: List[String],
   253     threads: Option[Int],
   254     timing: Timing,
   255     ml_timing: Timing,
   256     status: Session_Status.Value)
   257   {
   258     def finished: Boolean = status == Session_Status.FINISHED
   259   }
   260 
   261   sealed case class Build_Info(sessions: Map[String, Session_Entry])
   262   {
   263     def session(name: String): Session_Entry = sessions(name)
   264     def get_session(name: String): Option[Session_Entry] = sessions.get(name)
   265 
   266     def get_default[A](name: String, f: Session_Entry => A, x: A): A =
   267       get_session(name) match {
   268         case Some(entry) => f(entry)
   269         case None => x
   270       }
   271 
   272     def finished(name: String): Boolean = get_default(name, _.finished, false)
   273     def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
   274     def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   275   }
   276 
   277   private def parse_build_info(log_file: Log_File): Build_Info =
   278   {
   279     object Chapter_Name
   280     {
   281       def unapply(s: String): Some[(String, String)] =
   282         space_explode('/', s) match {
   283           case List(chapter, name) => Some((chapter, name))
   284           case _ => Some(("", s))
   285         }
   286     }
   287 
   288     val Session_No_Groups = new Regex("""^Session (\S+)$""")
   289     val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   290     val Session_Finished1 =
   291       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   292     val Session_Finished2 =
   293       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   294     val Session_Timing =
   295       new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   296     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
   297     val Session_Failed = new Regex("""^(\S+) FAILED""")
   298     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   299 
   300     var chapter = Map.empty[String, String]
   301     var groups = Map.empty[String, List[String]]
   302     var threads = Map.empty[String, Int]
   303     var timing = Map.empty[String, Timing]
   304     var ml_timing = Map.empty[String, Timing]
   305     var started = Set.empty[String]
   306     var failed = Set.empty[String]
   307     var cancelled = Set.empty[String]
   308     def all_sessions: Set[String] =
   309       chapter.keySet ++ groups.keySet ++ threads.keySet ++
   310       timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
   311 
   312 
   313     for (line <- log_file.lines) {
   314       line match {
   315         case Session_No_Groups(Chapter_Name(chapt, name)) =>
   316           chapter += (name -> chapt)
   317           groups += (name -> Nil)
   318         case Session_Groups(Chapter_Name(chapt, name), grps) =>
   319           chapter += (name -> chapt)
   320           groups += (name -> Word.explode(grps))
   321         case Session_Started(name) =>
   322           started += name
   323         case Session_Finished1(name,
   324             Value.Int(e1), Value.Int(e2), Value.Int(e3),
   325             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   326           val elapsed = Time.hms(e1, e2, e3)
   327           val cpu = Time.hms(c1, c2, c3)
   328           timing += (name -> Timing(elapsed, cpu, Time.zero))
   329         case Session_Finished2(name,
   330             Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   331           val elapsed = Time.hms(e1, e2, e3)
   332           timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   333         case Session_Timing(name,
   334             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   335           val elapsed = Time.seconds(e)
   336           val cpu = Time.seconds(c)
   337           val gc = Time.seconds(g)
   338           ml_timing += (name -> Timing(elapsed, cpu, gc))
   339           threads += (name -> t)
   340         case _ =>
   341       }
   342     }
   343 
   344     val sessions =
   345       Map(
   346         (for (name <- all_sessions.toList) yield {
   347           val status =
   348             if (failed(name)) Session_Status.FAILED
   349             else if (cancelled(name)) Session_Status.CANCELLED
   350             else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
   351               Session_Status.FINISHED
   352             else if (started(name)) Session_Status.FAILED
   353             else Session_Status.EXISTING
   354           val entry =
   355             Session_Entry(
   356               chapter.getOrElse(name, ""),
   357               groups.getOrElse(name, Nil),
   358               threads.get(name),
   359               timing.getOrElse(name, Timing.zero),
   360               ml_timing.getOrElse(name, Timing.zero),
   361               status)
   362           (name -> entry)
   363         }):_*)
   364     Build_Info(sessions)
   365   }
   366 }