more liberal parsing for old AFP logs;
authorwenzelm
Fri Oct 07 21:09:43 2016 +0200 (2016-10-07)
changeset 64091f8dfba90e73f
parent 64090 5a68280112b3
child 64092 95469c544b82
more liberal parsing for old AFP logs;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 18:41:54 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 21:09:43 2016 +0200
     1.3 @@ -100,11 +100,14 @@
     1.4  
     1.5      /* settings */
     1.6  
     1.7 -    def get_setting(a: String): Settings.Entry =
     1.8 -      Settings.Entry.unapply(
     1.9 -        lines.find(_.startsWith(a + "=")) getOrElse err("missing " + a)).get
    1.10 +    def get_setting(a: String): Option[Settings.Entry] =
    1.11 +      lines.find(_.startsWith(a + "=")) match {
    1.12 +        case Some(line) => Settings.Entry.unapply(line)
    1.13 +        case None => None
    1.14 +      }
    1.15  
    1.16 -    def get_settings(as: List[String]): Settings.T = as.map(get_setting(_))
    1.17 +    def get_settings(as: List[String]): Settings.T =
    1.18 +      for { a <- as; entry <- get_setting(a) } yield entry
    1.19  
    1.20  
    1.21      /* properties (YXML) */
    1.22 @@ -202,36 +205,53 @@
    1.23      val Date_Format =
    1.24        Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.25          // workaround for jdk-8u102
    1.26 -        s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
    1.27 +        s => Word.implode(Word.explode(s).map({
    1.28 +          case "CET" | "MET" => "GMT+1"
    1.29 +          case "CEST" | "MEST" => "GMT+2"
    1.30 +          case a => a })))
    1.31  
    1.32 -    val Test_Start = new Regex("""^Start test (?:for \S+)? at (.+), (\S+)$""")
    1.33 -    val Test_End = new Regex("""^End test on (.+), \S+, elapsed time:.*$""")
    1.34 +    object Strict_Date
    1.35 +    {
    1.36 +      def unapply(s: String): Some[Date] = Some(Date_Format.parse(s))
    1.37 +    }
    1.38 +
    1.39 +    val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
    1.40 +    val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
    1.41 +    val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
    1.42      val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
    1.43      val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
    1.44    }
    1.45  
    1.46    private def parse_header(log_file: Log_File): Header =
    1.47    {
    1.48 -    log_file.lines match {
    1.49 -      case AFP.Test_Start(start, hostname) :: _ =>
    1.50 -        (start, log_file.lines.last) match {
    1.51 -          case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
    1.52 -            val isabelle_version =
    1.53 -              log_file.find_match(AFP.Isabelle_Version).map((Field.isabelle_version, _))
    1.54 -            val afp_version =
    1.55 -              log_file.find_match(AFP.AFP_Version).map((Field.afp_version, _))
    1.56 +    def parse_afp(start: Date, hostname: String): Header =
    1.57 +    {
    1.58 +      val start_date = Field.build_start -> start.toString
    1.59 +      val end_date =
    1.60 +        log_file.lines.last match {
    1.61 +          case AFP.Test_End(AFP.Strict_Date(end_date)) =>
    1.62 +            List(Field.build_end -> end_date.toString)
    1.63 +          case _ => Nil
    1.64 +        }
    1.65 +
    1.66 +      val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
    1.67  
    1.68 -            Header(Header_Kind.AFP_TEST,
    1.69 -              List(
    1.70 -                Field.build_host -> hostname,
    1.71 -                Field.build_start -> start_date.toString,
    1.72 -                Field.build_end -> end_date.toString) :::
    1.73 -              isabelle_version.toList :::
    1.74 -              afp_version.toList,
    1.75 -              log_file.get_settings(Settings.all_settings))
    1.76 +      val isabelle_version =
    1.77 +        log_file.find_match(AFP.Isabelle_Version).map(Field.isabelle_version -> _)
    1.78 +
    1.79 +      val afp_version =
    1.80 +        log_file.find_match(AFP.AFP_Version).map(Field.afp_version -> _)
    1.81  
    1.82 -          case _ => log_file.err("cannot detect start/end date in afp-test log")
    1.83 -        }
    1.84 +      Header(Header_Kind.AFP_TEST,
    1.85 +        start_date :: end_date ::: build_host ::: isabelle_version.toList ::: afp_version.toList,
    1.86 +        log_file.get_settings(Settings.all_settings))
    1.87 +    }
    1.88 +
    1.89 +    log_file.lines match {
    1.90 +      case AFP.Test_Start(AFP.Strict_Date(start_date), hostname) :: _ =>
    1.91 +        parse_afp(start_date, hostname)
    1.92 +      case AFP.Test_Start_Old(AFP.Strict_Date(start_date)) :: _ =>
    1.93 +        parse_afp(start_date, "")
    1.94        case _ => log_file.err("cannot detect log header format")
    1.95      }
    1.96    }