src/Pure/Tools/build_log.scala
changeset 64054 1fc9ab31720d
parent 64053 7ece2e14fd6c
child 64061 1bbea2b55d22
     1.1 --- a/src/Pure/Tools/build_log.scala	Wed Oct 05 13:56:19 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Wed Oct 05 14:15:54 2016 +0200
     1.3 @@ -7,6 +7,10 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import scala.collection.mutable
     1.8 +import scala.util.matching.Regex
     1.9 +
    1.10 +
    1.11  object Build_Log
    1.12  {
    1.13    /* inlined properties (YXML) */
    1.14 @@ -55,4 +59,74 @@
    1.15  
    1.16      Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
    1.17    }
    1.18 +
    1.19 +
    1.20 +  /* main log: produced by isatest, afp-test, jenkins etc. */
    1.21 +
    1.22 +  sealed case class Info(
    1.23 +    ml_options: List[(String, String)],
    1.24 +    finished: Map[String, Timing],
    1.25 +    timing: Map[String, Timing],
    1.26 +    threads: Map[String, Int])
    1.27 +  {
    1.28 +    val sessions: Set[String] = finished.keySet ++ timing.keySet
    1.29 +
    1.30 +    override def toString: String =
    1.31 +      sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")")
    1.32 +  }
    1.33 +
    1.34 +  private val Session_Finished1 =
    1.35 +    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
    1.36 +  private val Session_Finished2 =
    1.37 +    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
    1.38 +  private val Session_Timing =
    1.39 +    new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
    1.40 +
    1.41 +  private object ML_Option
    1.42 +  {
    1.43 +    def unapply(s: String): Option[(String, String)] =
    1.44 +      s.indexOf('=') match {
    1.45 +        case -1 => None
    1.46 +        case i =>
    1.47 +          val a = s.substring(0, i)
    1.48 +          Library.try_unquote(s.substring(i + 1)) match {
    1.49 +            case Some(b) if Build.ml_options.contains(a) => Some((a, b))
    1.50 +            case _ => None
    1.51 +          }
    1.52 +      }
    1.53 +  }
    1.54 +
    1.55 +  def parse_info(text: String): Info =
    1.56 +  {
    1.57 +    val ml_options = new mutable.ListBuffer[(String, String)]
    1.58 +    var finished = Map.empty[String, Timing]
    1.59 +    var timing = Map.empty[String, Timing]
    1.60 +    var threads = Map.empty[String, Int]
    1.61 +
    1.62 +    for (line <- split_lines(text)) {
    1.63 +      line match {
    1.64 +        case Session_Finished1(name,
    1.65 +            Value.Int(e1), Value.Int(e2), Value.Int(e3),
    1.66 +            Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
    1.67 +          val elapsed = Time.hms(e1, e2, e3)
    1.68 +          val cpu = Time.hms(c1, c2, c3)
    1.69 +          finished += (name -> Timing(elapsed, cpu, Time.zero))
    1.70 +        case Session_Finished2(name,
    1.71 +            Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
    1.72 +          val elapsed = Time.hms(e1, e2, e3)
    1.73 +          finished += (name -> Timing(elapsed, Time.zero, Time.zero))
    1.74 +        case Session_Timing(name,
    1.75 +            Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
    1.76 +          val elapsed = Time.seconds(e)
    1.77 +          val cpu = Time.seconds(c)
    1.78 +          val gc = Time.seconds(g)
    1.79 +          timing += (name -> Timing(elapsed, cpu, gc))
    1.80 +          threads += (name -> t)
    1.81 +        case ML_Option(a, b) => ml_options += (a -> b)
    1.82 +        case _ =>
    1.83 +      }
    1.84 +    }
    1.85 +
    1.86 +    Info(ml_options.toList, finished, timing, threads)
    1.87 +  }
    1.88  }