some support for header and data fields, notably from afp-test;
authorwenzelm
Wed Oct 05 22:09:53 2016 +0200 (2016-10-05)
changeset 640611bbea2b55d22
parent 64060 f3fa0bb3f666
child 64062 a7352cbde7d7
some support for header and data fields, notably from afp-test;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Wed Oct 05 22:07:36 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Wed Oct 05 22:09:53 2016 +0200
     1.3 @@ -7,6 +7,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import java.time.ZonedDateTime
     1.8 +import java.time.format.{DateTimeFormatter, DateTimeParseException}
     1.9 +
    1.10  import scala.collection.mutable
    1.11  import scala.util.matching.Regex
    1.12  
    1.13 @@ -61,6 +64,76 @@
    1.14    }
    1.15  
    1.16  
    1.17 +  /* header and data fields */
    1.18 +
    1.19 +  object Header_Kind extends Enumeration
    1.20 +  {
    1.21 +    val ISATEST = Value("isatest")
    1.22 +    val AFP_TEST = Value("afp-test")
    1.23 +    val JENKINS = Value("jenkins")
    1.24 +  }
    1.25 +
    1.26 +  sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String])
    1.27 +
    1.28 +  object Field
    1.29 +  {
    1.30 +    val build_host = "build_host"
    1.31 +    val build_start = "build_start"
    1.32 +    val build_end = "build_end"
    1.33 +    val isabelle_version = "isabelle_version"
    1.34 +    val afp_version = "afp_version"
    1.35 +  }
    1.36 +
    1.37 +  object AFP
    1.38 +  {
    1.39 +    val Date_Format =
    1.40 +      Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.41 +        // workaround for jdk-8u102
    1.42 +        s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
    1.43 +    val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""")
    1.44 +    val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
    1.45 +    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
    1.46 +    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
    1.47 +    val settings =
    1.48 +      List("ISABELLE_BUILD_OPTIONS=", "ML_PLATFORM=", "ML_HOME=", "ML_SYSTEM=", "ML_OPTIONS=")
    1.49 +  }
    1.50 +
    1.51 +  def parse_header(lines: List[String]): Header =
    1.52 +  {
    1.53 +    val proper_lines = lines.filterNot(line => line.forall(Character.isWhitespace(_)))
    1.54 +
    1.55 +    def err(msg: String): Nothing = error(cat_lines((msg + ":") :: lines.take(10)))
    1.56 +
    1.57 +    proper_lines match {
    1.58 +      case AFP.Test_Start(start, hostname) :: _ =>
    1.59 +        (start, proper_lines.last) match {
    1.60 +          case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
    1.61 +            val props =
    1.62 +              List(
    1.63 +                Field.build_host -> hostname,
    1.64 +                Field.build_start -> start_date.toString,
    1.65 +                Field.build_end -> end_date.toString) :::
    1.66 +              lines.collectFirst(
    1.67 +                { case AFP.Isabelle_Version(id) => Field.isabelle_version -> id }).toList :::
    1.68 +              lines.collectFirst(
    1.69 +                { case AFP.AFP_Version(id) => Field.afp_version -> id }).toList
    1.70 +            val settings = lines.filter(line => AFP.settings.exists(line.startsWith(_)))
    1.71 +            Header(Header_Kind.AFP_TEST, props, settings)
    1.72 +          case _ => err("Malformed start/end date in afp-test log")
    1.73 +        }
    1.74 +      case _ => err("Failed to detect build log header")
    1.75 +    }
    1.76 +  }
    1.77 +
    1.78 +  object Session_Status extends Enumeration
    1.79 +  {
    1.80 +    val UNKNOWN = Value("unknown")
    1.81 +    val FINISHED = Value("finished")
    1.82 +    val FAILED = Value("failed")
    1.83 +    val CANCELLED = Value("cancelled")
    1.84 +  }
    1.85 +
    1.86 +
    1.87    /* main log: produced by isatest, afp-test, jenkins etc. */
    1.88  
    1.89    sealed case class Info(