support for Isabelle/Jenkins log file format;
authorwenzelm
Sat Oct 08 17:22:52 2016 +0200 (2016-10-08)
changeset 64110c0b96b34c7b9
parent 64109 d54aa68e33dc
child 64111 b2290b9d0175
support for Isabelle/Jenkins log file format;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 16:07:41 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 17:22:52 2016 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/Tools/build_log.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Build log parsing for current and historic versions.
     1.8 +Build log parsing for current and historic formats.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -9,7 +9,7 @@
    1.13  
    1.14  import java.io.{File => JFile}
    1.15  import java.time.ZoneId
    1.16 -import java.time.format.DateTimeParseException
    1.17 +import java.time.format.{DateTimeFormatter, DateTimeParseException}
    1.18  import java.util.Locale
    1.19  
    1.20  import scala.collection.mutable
    1.21 @@ -90,13 +90,18 @@
    1.22  
    1.23      def apply(path: Path): Log_File = apply(path.file)
    1.24  
    1.25 +
    1.26 +    /* date format */
    1.27 +
    1.28      val Date_Format =
    1.29      {
    1.30        val fmts =
    1.31          Date.Formatter.variants(
    1.32            List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
    1.33            List(Locale.ENGLISH, Locale.GERMAN)) :::
    1.34 -        List(Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
    1.35 +        List(
    1.36 +          DateTimeFormatter.RFC_1123_DATE_TIME,
    1.37 +          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(ZoneId.of("Europe/Berlin")))
    1.38  
    1.39        def tune_timezone(s: String): String =
    1.40          s match {
    1.41 @@ -249,6 +254,19 @@
    1.42      val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
    1.43    }
    1.44  
    1.45 +  object Jenkins
    1.46 +  {
    1.47 +    val engine = "jenkins"
    1.48 +    val Start = new Regex("""^Started .*$""")
    1.49 +    val Start_Date = new Regex("""^Build started at (.+)$""")
    1.50 +    val No_End = new Regex("""$.""")
    1.51 +    val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""")
    1.52 +    val AFP_Version = new Regex("""^AFP id (\S+)$""")
    1.53 +    val CONFIGURATION = "=== CONFIGURATION ==="
    1.54 +    val BUILD = "=== BUILD ==="
    1.55 +    val FINISHED = "Finished: "
    1.56 +  }
    1.57 +
    1.58    private def parse_meta_info(log_file: Log_File): Meta_Info =
    1.59    {
    1.60      def parse(engine: String, host: String, start: Date,
    1.61 @@ -288,12 +306,22 @@
    1.62          parse(AFP_Test.engine, "", start, AFP_Test.End,
    1.63            AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
    1.64  
    1.65 +      case Jenkins.Start() :: _
    1.66 +      if log_file.lines.contains(Jenkins.CONFIGURATION) ||
    1.67 +         log_file.lines.last.startsWith(Jenkins.FINISHED) =>
    1.68 +        log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
    1.69 +          case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
    1.70 +            parse(Jenkins.engine, "", start, Jenkins.No_End,
    1.71 +              Jenkins.Isabelle_Version, Jenkins.AFP_Version)
    1.72 +          case _ => Meta_Info.empty
    1.73 +        }
    1.74 +
    1.75        case line :: _ if line.startsWith("\0") => Meta_Info.empty
    1.76        case List(Isatest.End(_)) => Meta_Info.empty
    1.77        case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
    1.78        case Nil => Meta_Info.empty
    1.79  
    1.80 -      case _ => log_file.err("cannot detect log header format")
    1.81 +      case _ => log_file.err("cannot detect log file format")
    1.82      }
    1.83    }
    1.84