more permissive: accept all historic isatest and afp-test logs;
authorwenzelm
Sat Oct 08 14:55:34 2016 +0200 (2016-10-08)
changeset 64104b70fa05d6746
parent 64103 60d163f38056
child 64105 d93bd6d253c6
more permissive: accept all historic isatest and afp-test logs;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 13:05:05 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 14:55:34 2016 +0200
     1.3 @@ -93,18 +93,37 @@
     1.4      val Date_Format =
     1.5      {
     1.6        val fmts =
     1.7 -        Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")) ::
     1.8          Date.Formatter.variants(
     1.9            List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.10 -          List(Locale.ENGLISH, Locale.GERMAN))
    1.11 +          List(Locale.ENGLISH, Locale.GERMAN)) :::
    1.12 +        List(Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
    1.13  
    1.14 -      // workaround undetected timezones
    1.15 -      def tune(s: String): String =
    1.16 -        Word.implode(Word.explode(s).map({
    1.17 +      def tune_timezone(s: String): String =
    1.18 +        s match {
    1.19            case "CET" | "MET" => "GMT+1"
    1.20            case "CEST" | "MEST" => "GMT+2"
    1.21 -          case "EST" => "GMT+1"  // FIXME ??
    1.22 -          case a => a }))
    1.23 +          case "EST" => "Europe/Berlin"
    1.24 +          case _ => s
    1.25 +        }
    1.26 +      def tune_weekday(s: String): String =
    1.27 +        s match {
    1.28 +          case "Die" => "Di"
    1.29 +          case "Mit" => "Mi"
    1.30 +          case "Don" => "Do"
    1.31 +          case "Fre" => "Fr"
    1.32 +          case "Sam" => "Sa"
    1.33 +          case "Son" => "So"
    1.34 +          case _ => s
    1.35 +        }
    1.36 +
    1.37 +      def tune(s: String): String =
    1.38 +        Word.implode(
    1.39 +          Word.explode(s) match {
    1.40 +            case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_))
    1.41 +            case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_))
    1.42 +            case Nil => Nil
    1.43 +          }
    1.44 +        )
    1.45  
    1.46        Date.Format.make(fmts, tune)
    1.47      }
    1.48 @@ -201,11 +220,17 @@
    1.49  
    1.50    object Kind extends Enumeration
    1.51    {
    1.52 +    val EMPTY = Value("empty")
    1.53      val ISATEST = Value("isatest")
    1.54      val AFP_TEST = Value("afp-test")
    1.55      val JENKINS = Value("jenkins")
    1.56    }
    1.57  
    1.58 +  object Header
    1.59 +  {
    1.60 +    val empty: Header = Header(Kind.EMPTY, Nil, Nil)
    1.61 +  }
    1.62 +
    1.63    sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
    1.64    {
    1.65      def is_empty: Boolean = props.isEmpty && settings.isEmpty
    1.66 @@ -226,6 +251,7 @@
    1.67      val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
    1.68      val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
    1.69      val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
    1.70 +    val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
    1.71    }
    1.72  
    1.73    private def parse_header(log_file: Log_File): Header =
    1.74 @@ -260,8 +286,6 @@
    1.75          parse(Kind.ISATEST, start, hostname,
    1.76            Isatest.Test_End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)
    1.77  
    1.78 -      case List(Isatest.Test_End(_)) => Header(Kind.ISATEST, Nil, Nil)
    1.79 -
    1.80        case AFP.Test_Start(log_file.Strict_Date(start), hostname) :: _ =>
    1.81          parse(Kind.AFP_TEST, start, hostname,
    1.82            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    1.83 @@ -270,6 +294,11 @@
    1.84          parse(Kind.AFP_TEST, start, "",
    1.85            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    1.86  
    1.87 +      case line :: _ if line.startsWith("\0") => Header.empty
    1.88 +      case List(Isatest.Test_End(_)) => Header.empty
    1.89 +      case _ :: AFP.Bad_Init() :: _ => Header.empty
    1.90 +      case Nil => Header.empty
    1.91 +
    1.92        case _ => log_file.err("cannot detect log header format")
    1.93      }
    1.94    }