merged
authorwenzelm
Fri Oct 07 21:19:15 2016 +0200 (2016-10-07)
changeset 64093f09f377da49d
parent 64077 6d770c2dc60d
parent 64092 95469c544b82
child 64094 629558a1ecf5
merged
     1.1 --- a/src/HOL/Library/Old_SMT.thy	Fri Oct 07 17:59:19 2016 +0200
     1.2 +++ b/src/HOL/Library/Old_SMT.thy	Fri Oct 07 21:19:15 2016 +0200
     1.3 @@ -142,7 +142,8 @@
     1.4  method_setup old_smt = \<open>
     1.5    Scan.optional Attrib.thms [] >>
     1.6      (fn thms => fn ctxt =>
     1.7 -      METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))
     1.8 +      (legacy_feature "Proof method \"old_smt\" will be discontinued soon -- use \"smt\" instead";
     1.9 +       METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))))
    1.10  \<close> "apply an SMT solver to the current goal"
    1.11  
    1.12  
     2.1 --- a/src/Pure/General/timing.scala	Fri Oct 07 17:59:19 2016 +0200
     2.2 +++ b/src/Pure/General/timing.scala	Fri Oct 07 21:19:15 2016 +0200
     2.3 @@ -1,5 +1,4 @@
     2.4  /*  Title:      Pure/General/timing.scala
     2.5 -    Module:     PIDE
     2.6      Author:     Makarius
     2.7  
     2.8  Basic support for time measurement.
     2.9 @@ -34,27 +33,34 @@
    2.10  
    2.11  sealed case class Timing(elapsed: Time, cpu: Time, gc: Time)
    2.12  {
    2.13 +  def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
    2.14    def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
    2.15  
    2.16 +  def resources: Time = cpu + gc
    2.17 +
    2.18 +  def factor: Option[Double] =
    2.19 +  {
    2.20 +    val t1 = elapsed.seconds
    2.21 +    val t2 = resources.seconds
    2.22 +    if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None
    2.23 +  }
    2.24 +
    2.25    def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc)
    2.26  
    2.27    def message: String =
    2.28      elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
    2.29  
    2.30 -  def resources: Time = cpu + gc
    2.31    def message_resources: String =
    2.32    {
    2.33 -    val resources = cpu + gc
    2.34 -    val t1 = elapsed.seconds
    2.35 -    val t2 = resources.seconds
    2.36 -    val factor =
    2.37 -      if (t1 >= 3.0 && t2 >= 3.0)
    2.38 -        String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1))
    2.39 -      else ""
    2.40 -    if (t2 >= 3.0)
    2.41 -      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor
    2.42 +    val factor_text =
    2.43 +      factor match {
    2.44 +        case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f))
    2.45 +        case None => ""
    2.46 +      }
    2.47 +    if (resources.seconds >= 3.0)
    2.48 +      elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text
    2.49      else
    2.50 -      elapsed.message_hms + " elapsed time" + factor
    2.51 +      elapsed.message_hms + " elapsed time" + factor_text
    2.52    }
    2.53  
    2.54    override def toString: String = message
     3.1 --- a/src/Pure/Tools/build.scala	Fri Oct 07 17:59:19 2016 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Fri Oct 07 21:19:15 2016 +0200
     3.3 @@ -477,7 +477,7 @@
     3.4        }
     3.5  
     3.6        try {
     3.7 -        val info = Build_Log.Log_File(name, text).parse_session_info(name, false)
     3.8 +        val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true)
     3.9          val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0
    3.10          (info.command_timings, session_timing)
    3.11        }
    3.12 @@ -686,17 +686,8 @@
    3.13  
    3.14    /* Isabelle tool wrapper */
    3.15  
    3.16 -  val ml_options = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    3.17 -
    3.18    val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
    3.19    {
    3.20 -    def show_settings(): String =
    3.21 -      cat_lines(List(
    3.22 -        "ISABELLE_BUILD_OPTIONS=" +
    3.23 -          quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
    3.24 -        "") :::
    3.25 -        ml_options.map(opt => opt + "=" + quote(Isabelle_System.getenv(opt))))
    3.26 -
    3.27      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
    3.28  
    3.29      var select_dirs: List[Path] = Nil
    3.30 @@ -739,7 +730,7 @@
    3.31  
    3.32    Build and manage Isabelle sessions, depending on implicit settings:
    3.33  
    3.34 -""" + Library.prefix_lines("  ", show_settings()),
    3.35 +""" + Library.prefix_lines("  ", Build_Log.Settings.show()),
    3.36        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    3.37        "R" -> (_ => requirements = true),
    3.38        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    3.39 @@ -766,7 +757,7 @@
    3.40          Library.trim_line(
    3.41            Isabelle_System.bash(
    3.42              """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
    3.43 -      progress.echo(show_settings() + "\n")
    3.44 +      progress.echo(Build_Log.Settings.show() + "\n")
    3.45      }
    3.46  
    3.47      val start_time = Time.now()
     4.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 17:59:19 2016 +0200
     4.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 21:19:15 2016 +0200
     4.3 @@ -7,6 +7,7 @@
     4.4  package isabelle
     4.5  
     4.6  
     4.7 +import java.io.{File => JFile}
     4.8  import java.time.ZonedDateTime
     4.9  import java.time.format.{DateTimeFormatter, DateTimeParseException}
    4.10  
    4.11 @@ -16,6 +17,37 @@
    4.12  
    4.13  object Build_Log
    4.14  {
    4.15 +  /** settings **/
    4.16 +
    4.17 +  object Settings
    4.18 +  {
    4.19 +    val build_settings = List("ISABELLE_BUILD_OPTIONS")
    4.20 +    val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    4.21 +    val all_settings = build_settings ::: ml_settings
    4.22 +
    4.23 +    type Entry = (String, String)
    4.24 +    type T = List[Entry]
    4.25 +
    4.26 +    object Entry
    4.27 +    {
    4.28 +      def unapply(s: String): Option[Entry] =
    4.29 +        s.indexOf('=') match {
    4.30 +          case -1 => None
    4.31 +          case i =>
    4.32 +            val a = s.substring(0, i)
    4.33 +            val b = Library.perhaps_unquote(s.substring(i + 1))
    4.34 +            Some((a, b))
    4.35 +        }
    4.36 +      def apply(a: String, b: String): String = a + "=" + quote(b)
    4.37 +      def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    4.38 +    }
    4.39 +
    4.40 +    def show(): String =
    4.41 +      cat_lines(
    4.42 +        build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
    4.43 +  }
    4.44 +
    4.45 +
    4.46    /** log file **/
    4.47  
    4.48    object Log_File
    4.49 @@ -25,6 +57,23 @@
    4.50  
    4.51      def apply(name: String, text: String): Log_File =
    4.52        Log_File(name, Library.trim_split_lines(text))
    4.53 +
    4.54 +    def apply(file: JFile): Log_File =
    4.55 +    {
    4.56 +      val name = file.getName
    4.57 +      val (base_name, text) =
    4.58 +        Library.try_unsuffix(".gz", name) match {
    4.59 +          case Some(base_name) => (base_name, File.read_gzip(file))
    4.60 +          case None =>
    4.61 +            Library.try_unsuffix(".xz", name) match {
    4.62 +              case Some(base_name) => (base_name, File.read_xz(file))
    4.63 +              case None => (name, File.read(file))
    4.64 +            }
    4.65 +          }
    4.66 +      apply(base_name, text)
    4.67 +    }
    4.68 +
    4.69 +    def apply(path: Path): Log_File = apply(path.file)
    4.70    }
    4.71  
    4.72    class Log_File private(val name: String, val lines: List[String])
    4.73 @@ -51,11 +100,14 @@
    4.74  
    4.75      /* settings */
    4.76  
    4.77 -    def get_setting(setting: String): String =
    4.78 -      lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting)
    4.79 +    def get_setting(a: String): Option[Settings.Entry] =
    4.80 +      lines.find(_.startsWith(a + "=")) match {
    4.81 +        case Some(line) => Settings.Entry.unapply(line)
    4.82 +        case None => None
    4.83 +      }
    4.84  
    4.85 -    def get_settings(settings: List[String]): List[String] =
    4.86 -      settings.map(get_setting(_))
    4.87 +    def get_settings(as: List[String]): Settings.T =
    4.88 +      for { a <- as; entry <- get_setting(a) } yield entry
    4.89  
    4.90  
    4.91      /* properties (YXML) */
    4.92 @@ -77,12 +129,17 @@
    4.93  
    4.94      /* parse various formats */
    4.95  
    4.96 -    def parse_session_info(session_name: String, full: Boolean): Session_Info =
    4.97 -      Build_Log.parse_session_info(log_file, session_name, full)
    4.98 +    def parse_session_info(
    4.99 +        default_name: String = "",
   4.100 +        command_timings: Boolean = false,
   4.101 +        ml_statistics: Boolean = false,
   4.102 +        task_statistics: Boolean = false): Session_Info =
   4.103 +      Build_Log.parse_session_info(
   4.104 +        log_file, default_name, command_timings, ml_statistics, task_statistics)
   4.105  
   4.106 -    def parse_header: Header = Build_Log.parse_header(log_file)
   4.107 +    def parse_header(): Header = Build_Log.parse_header(log_file)
   4.108  
   4.109 -    def parse_info: Info = Build_Log.parse_info(log_file)
   4.110 +    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
   4.111    }
   4.112  
   4.113  
   4.114 @@ -95,22 +152,30 @@
   4.115      ml_statistics: List[Properties.T],
   4.116      task_statistics: List[Properties.T])
   4.117  
   4.118 -  private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info =
   4.119 +  private def parse_session_info(
   4.120 +    log_file: Log_File,
   4.121 +    default_name: String,
   4.122 +    command_timings: Boolean,
   4.123 +    ml_statistics: Boolean,
   4.124 +    task_statistics: Boolean): Session_Info =
   4.125    {
   4.126      val xml_cache = new XML.Cache()
   4.127  
   4.128      val session_name =
   4.129        log_file.find_line("\fSession.name = ") match {
   4.130 -        case None => name0
   4.131 -        case Some(name) if name0 == "" || name0 == name => name
   4.132 +        case None => default_name
   4.133 +        case Some(name) if default_name == "" || default_name == name => name
   4.134          case Some(name) => log_file.err("log from different session " + quote(name))
   4.135        }
   4.136      val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil
   4.137 -    val command_timings = log_file.filter_props("\fcommand_timing = ")
   4.138 -    val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil
   4.139 -    val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil
   4.140 +    val command_timings_ =
   4.141 +      if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil
   4.142 +    val ml_statistics_ =
   4.143 +      if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil
   4.144 +    val task_statistics_ =
   4.145 +      if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil
   4.146  
   4.147 -    Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics)
   4.148 +    Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_)
   4.149    }
   4.150  
   4.151  
   4.152 @@ -123,7 +188,8 @@
   4.153      val JENKINS = Value("jenkins")
   4.154    }
   4.155  
   4.156 -  sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String])
   4.157 +  sealed case class Header(
   4.158 +    kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
   4.159  
   4.160    object Field
   4.161    {
   4.162 @@ -134,125 +200,188 @@
   4.163      val afp_version = "afp_version"
   4.164    }
   4.165  
   4.166 -  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
   4.167 -
   4.168    object AFP
   4.169    {
   4.170      val Date_Format =
   4.171        Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"),
   4.172          // workaround for jdk-8u102
   4.173 -        s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a })))
   4.174 +        s => Word.implode(Word.explode(s).map({
   4.175 +          case "CET" | "MET" => "GMT+1"
   4.176 +          case "CEST" | "MEST" => "GMT+2"
   4.177 +          case "EST" => "GMT+1"  // FIXME ??
   4.178 +          case a => a })))
   4.179  
   4.180 -    val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""")
   4.181 -    val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
   4.182 -    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
   4.183 -    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
   4.184 -    val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings
   4.185 +    object Strict_Date
   4.186 +    {
   4.187 +      def unapply(s: String): Some[Date] = Some(Date_Format.parse(s))
   4.188 +    }
   4.189 +
   4.190 +    val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
   4.191 +    val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
   4.192 +    val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
   4.193 +    val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""")
   4.194 +    val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""")
   4.195    }
   4.196  
   4.197    private def parse_header(log_file: Log_File): Header =
   4.198    {
   4.199 -    log_file.lines match {
   4.200 -      case AFP.Test_Start(start, hostname) :: _ =>
   4.201 -        (start, log_file.lines.last) match {
   4.202 -          case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) =>
   4.203 -            val isabelle_version =
   4.204 -              log_file.find_match(AFP.Isabelle_Version) getOrElse
   4.205 -                log_file.err("missing Isabelle version")
   4.206 -            val afp_version =
   4.207 -              log_file.find_match(AFP.AFP_Version) getOrElse
   4.208 -                log_file.err("missing AFP version")
   4.209 +    def parse_afp(start: Date, hostname: String): Header =
   4.210 +    {
   4.211 +      val start_date = Field.build_start -> start.toString
   4.212 +      val end_date =
   4.213 +        log_file.lines.last match {
   4.214 +          case AFP.Test_End(AFP.Strict_Date(end_date)) =>
   4.215 +            List(Field.build_end -> end_date.toString)
   4.216 +          case _ => Nil
   4.217 +        }
   4.218 +
   4.219 +      val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname)
   4.220  
   4.221 -            Header(Header_Kind.AFP_TEST,
   4.222 -              List(
   4.223 -                Field.build_host -> hostname,
   4.224 -                Field.build_start -> start_date.toString,
   4.225 -                Field.build_end -> end_date.toString,
   4.226 -                Field.isabelle_version -> isabelle_version,
   4.227 -                Field.afp_version -> afp_version),
   4.228 -              log_file.get_settings(AFP.settings))
   4.229 +      val isabelle_version =
   4.230 +        log_file.find_match(AFP.Isabelle_Version).map(Field.isabelle_version -> _)
   4.231 +
   4.232 +      val afp_version =
   4.233 +        log_file.find_match(AFP.AFP_Version).map(Field.afp_version -> _)
   4.234  
   4.235 -          case _ => log_file.err("cannot detect start/end date in afp-test log")
   4.236 -        }
   4.237 +      Header(Header_Kind.AFP_TEST,
   4.238 +        start_date :: end_date ::: build_host ::: isabelle_version.toList ::: afp_version.toList,
   4.239 +        log_file.get_settings(Settings.all_settings))
   4.240 +    }
   4.241 +
   4.242 +    log_file.lines match {
   4.243 +      case AFP.Test_Start(AFP.Strict_Date(start_date), hostname) :: _ =>
   4.244 +        parse_afp(start_date, hostname)
   4.245 +      case AFP.Test_Start_Old(AFP.Strict_Date(start_date)) :: _ =>
   4.246 +        parse_afp(start_date, "")
   4.247        case _ => log_file.err("cannot detect log header format")
   4.248      }
   4.249    }
   4.250  
   4.251 +
   4.252 +  /* build info: produced by isabelle build */
   4.253 +
   4.254    object Session_Status extends Enumeration
   4.255    {
   4.256 -    val UNKNOWN = Value("unknown")
   4.257 +    val EXISTING = Value("existing")
   4.258      val FINISHED = Value("finished")
   4.259      val FAILED = Value("failed")
   4.260      val CANCELLED = Value("cancelled")
   4.261    }
   4.262  
   4.263 -
   4.264 -  /* main log: produced by isatest, afp-test, jenkins etc. */
   4.265 +  sealed case class Session_Entry(
   4.266 +    chapter: String,
   4.267 +    groups: List[String],
   4.268 +    threads: Option[Int],
   4.269 +    timing: Timing,
   4.270 +    ml_timing: Timing,
   4.271 +    status: Session_Status.Value)
   4.272 +  {
   4.273 +    def finished: Boolean = status == Session_Status.FINISHED
   4.274 +  }
   4.275  
   4.276 -  sealed case class Info(
   4.277 -    ml_options: List[(String, String)],
   4.278 -    finished: Map[String, Timing],
   4.279 -    timing: Map[String, Timing],
   4.280 -    threads: Map[String, Int])
   4.281 +  sealed case class Build_Info(sessions: Map[String, Session_Entry])
   4.282    {
   4.283 -    val sessions: Set[String] = finished.keySet ++ timing.keySet
   4.284 +    def session(name: String): Session_Entry = sessions(name)
   4.285 +    def get_session(name: String): Option[Session_Entry] = sessions.get(name)
   4.286  
   4.287 -    override def toString: String =
   4.288 -      sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")")
   4.289 +    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
   4.290 +      get_session(name) match {
   4.291 +        case Some(entry) => f(entry)
   4.292 +        case None => x
   4.293 +      }
   4.294 +
   4.295 +    def finished(name: String): Boolean = get_default(name, _.finished, false)
   4.296 +    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
   4.297 +    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
   4.298    }
   4.299  
   4.300 -  private val Session_Finished1 =
   4.301 -    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   4.302 -  private val Session_Finished2 =
   4.303 -    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   4.304 -  private val Session_Timing =
   4.305 -    new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   4.306 -
   4.307 -  private object ML_Option
   4.308 +  private def parse_build_info(log_file: Log_File): Build_Info =
   4.309    {
   4.310 -    def unapply(s: String): Option[(String, String)] =
   4.311 -      s.indexOf('=') match {
   4.312 -        case -1 => None
   4.313 -        case i =>
   4.314 -          val a = s.substring(0, i)
   4.315 -          Library.try_unquote(s.substring(i + 1)) match {
   4.316 -            case Some(b) if Build.ml_options.contains(a) => Some((a, b))
   4.317 -            case _ => None
   4.318 -          }
   4.319 -      }
   4.320 -  }
   4.321 +    object Chapter_Name
   4.322 +    {
   4.323 +      def unapply(s: String): Some[(String, String)] =
   4.324 +        space_explode('/', s) match {
   4.325 +          case List(chapter, name) => Some((chapter, name))
   4.326 +          case _ => Some(("", s))
   4.327 +        }
   4.328 +    }
   4.329  
   4.330 -  private def parse_info(log_file: Log_File): Info =
   4.331 -  {
   4.332 -    val ml_options = new mutable.ListBuffer[(String, String)]
   4.333 -    var finished = Map.empty[String, Timing]
   4.334 +    val Session_No_Groups = new Regex("""^Session (\S+)$""")
   4.335 +    val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
   4.336 +    val Session_Finished1 =
   4.337 +      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
   4.338 +    val Session_Finished2 =
   4.339 +      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   4.340 +    val Session_Timing =
   4.341 +      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
   4.342 +    val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
   4.343 +    val Session_Failed = new Regex("""^(\S+) FAILED""")
   4.344 +    val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
   4.345 +
   4.346 +    var chapter = Map.empty[String, String]
   4.347 +    var groups = Map.empty[String, List[String]]
   4.348 +    var threads = Map.empty[String, Int]
   4.349      var timing = Map.empty[String, Timing]
   4.350 -    var threads = Map.empty[String, Int]
   4.351 +    var ml_timing = Map.empty[String, Timing]
   4.352 +    var started = Set.empty[String]
   4.353 +    var failed = Set.empty[String]
   4.354 +    var cancelled = Set.empty[String]
   4.355 +    def all_sessions: Set[String] =
   4.356 +      chapter.keySet ++ groups.keySet ++ threads.keySet ++
   4.357 +      timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started
   4.358 +
   4.359  
   4.360      for (line <- log_file.lines) {
   4.361        line match {
   4.362 +        case Session_No_Groups(Chapter_Name(chapt, name)) =>
   4.363 +          chapter += (name -> chapt)
   4.364 +          groups += (name -> Nil)
   4.365 +        case Session_Groups(Chapter_Name(chapt, name), grps) =>
   4.366 +          chapter += (name -> chapt)
   4.367 +          groups += (name -> Word.explode(grps))
   4.368 +        case Session_Started(name) =>
   4.369 +          started += name
   4.370          case Session_Finished1(name,
   4.371              Value.Int(e1), Value.Int(e2), Value.Int(e3),
   4.372              Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
   4.373            val elapsed = Time.hms(e1, e2, e3)
   4.374            val cpu = Time.hms(c1, c2, c3)
   4.375 -          finished += (name -> Timing(elapsed, cpu, Time.zero))
   4.376 +          timing += (name -> Timing(elapsed, cpu, Time.zero))
   4.377          case Session_Finished2(name,
   4.378              Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
   4.379            val elapsed = Time.hms(e1, e2, e3)
   4.380 -          finished += (name -> Timing(elapsed, Time.zero, Time.zero))
   4.381 +          timing += (name -> Timing(elapsed, Time.zero, Time.zero))
   4.382          case Session_Timing(name,
   4.383              Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
   4.384            val elapsed = Time.seconds(e)
   4.385            val cpu = Time.seconds(c)
   4.386            val gc = Time.seconds(g)
   4.387 -          timing += (name -> Timing(elapsed, cpu, gc))
   4.388 +          ml_timing += (name -> Timing(elapsed, cpu, gc))
   4.389            threads += (name -> t)
   4.390 -        case ML_Option(a, b) => ml_options += (a -> b)
   4.391          case _ =>
   4.392        }
   4.393      }
   4.394  
   4.395 -    Info(ml_options.toList, finished, timing, threads)
   4.396 +    val sessions =
   4.397 +      Map(
   4.398 +        (for (name <- all_sessions.toList) yield {
   4.399 +          val status =
   4.400 +            if (failed(name)) Session_Status.FAILED
   4.401 +            else if (cancelled(name)) Session_Status.CANCELLED
   4.402 +            else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
   4.403 +              Session_Status.FINISHED
   4.404 +            else if (started(name)) Session_Status.FAILED
   4.405 +            else Session_Status.EXISTING
   4.406 +          val entry =
   4.407 +            Session_Entry(
   4.408 +              chapter.getOrElse(name, ""),
   4.409 +              groups.getOrElse(name, Nil),
   4.410 +              threads.get(name),
   4.411 +              timing.getOrElse(name, Timing.zero),
   4.412 +              ml_timing.getOrElse(name, Timing.zero),
   4.413 +              status)
   4.414 +          (name -> entry)
   4.415 +        }):_*)
   4.416 +    Build_Info(sessions)
   4.417    }
   4.418  }
     5.1 --- a/src/Pure/Tools/build_stats.scala	Fri Oct 07 17:59:19 2016 +0200
     5.2 +++ b/src/Pure/Tools/build_stats.scala	Fri Oct 07 21:19:15 2016 +0200
     5.3 @@ -29,16 +29,16 @@
     5.4  
     5.5      val all_infos =
     5.6        Par_List.map((job_info: CI_API.Job_Info) =>
     5.7 -        (job_info.timestamp / 1000, job_info.read_output.parse_info), job_infos)
     5.8 +        (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos)
     5.9      val all_sessions =
    5.10        (Set.empty[String] /: all_infos)(
    5.11 -        { case (s, (_, info)) => s ++ info.sessions })
    5.12 +        { case (s, (_, info)) => s ++ info.sessions.keySet })
    5.13  
    5.14 -    def check_threshold(info: Build_Log.Info, session: String): Boolean =
    5.15 -      info.finished.get(session) match {
    5.16 -        case Some(t) => t.elapsed >= elapsed_threshold
    5.17 -        case None => false
    5.18 -      }
    5.19 +    def check_threshold(info: Build_Log.Build_Info, session: String): Boolean =
    5.20 +    {
    5.21 +      val t = info.timing(session)
    5.22 +      !t.is_zero && t.elapsed >= elapsed_threshold
    5.23 +    }
    5.24  
    5.25      val sessions =
    5.26        for {
    5.27 @@ -51,12 +51,16 @@
    5.28        Isabelle_System.with_tmp_file(session, "png") { data_file =>
    5.29          Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file =>
    5.30            val data =
    5.31 -            for { (t, info) <- all_infos if info.finished.isDefinedAt(session) }
    5.32 +            for { (t, info) <- all_infos if info.finished(session) }
    5.33              yield {
    5.34 -              val finished = info.finished.getOrElse(session, Timing.zero)
    5.35 -              val timing = info.timing.getOrElse(session, Timing.zero)
    5.36 -              List(t.toString, finished.elapsed.minutes, finished.cpu.minutes,
    5.37 -                timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ")
    5.38 +              val timing1 = info.timing(session)
    5.39 +              val timing2 = info.ml_timing(session)
    5.40 +              List(t.toString,
    5.41 +                timing1.elapsed.minutes,
    5.42 +                timing1.cpu.minutes,
    5.43 +                timing2.elapsed.minutes,
    5.44 +                timing2.cpu.minutes,
    5.45 +                timing2.gc.minutes).mkString(" ")
    5.46              }
    5.47            File.write(data_file, cat_lines(data))
    5.48  
     6.1 --- a/src/Pure/Tools/ci_api.scala	Fri Oct 07 17:59:19 2016 +0200
     6.2 +++ b/src/Pure/Tools/ci_api.scala	Fri Oct 07 21:19:15 2016 +0200
     6.3 @@ -45,12 +45,9 @@
     6.4      session_logs: List[(String, URL)])
     6.5    {
     6.6      def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
     6.7 -    def read_log(name: String, full: Boolean): Build_Log.Session_Info =
     6.8 -    {
     6.9 -      val text =
    6.10 -        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    6.11 -      Build_Log.Log_File(name, text).parse_session_info(name, full)
    6.12 -    }
    6.13 +    def read_log_file(name: String): Build_Log.Log_File =
    6.14 +      Build_Log.Log_File(name,
    6.15 +        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    6.16    }
    6.17  
    6.18    def build_job_builds(job_name: String): List[Job_Info] =
     7.1 --- a/src/Pure/Tools/ci_profile.scala	Fri Oct 07 17:59:19 2016 +0200
     7.2 +++ b/src/Pure/Tools/ci_profile.scala	Fri Oct 07 21:19:15 2016 +0200
     7.3 @@ -86,7 +86,7 @@
     7.4    override final def apply(args: List[String]): Unit =
     7.5    {
     7.6      print_section("CONFIGURATION")
     7.7 -    Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt))))
     7.8 +    println(Build_Log.Settings.show())
     7.9      val props = load_properties()
    7.10      System.getProperties().putAll(props)
    7.11