# HG changeset patch # User wenzelm # Date 1475867955 -7200 # Node ID f09f377da49d2bc122280e14284eb3f66e4e8029 # Parent 6d770c2dc60d3ac5d3d965fd9871df6bb2944326# Parent 95469c544b82272a9b9c6851ee35c194fa1999a0 merged diff -r 6d770c2dc60d -r f09f377da49d src/HOL/Library/Old_SMT.thy --- a/src/HOL/Library/Old_SMT.thy Fri Oct 07 17:59:19 2016 +0200 +++ b/src/HOL/Library/Old_SMT.thy Fri Oct 07 21:19:15 2016 +0200 @@ -142,7 +142,8 @@ method_setup old_smt = \ Scan.optional Attrib.thms [] >> (fn thms => fn ctxt => - METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))) + (legacy_feature "Proof method \"old_smt\" will be discontinued soon -- use \"smt\" instead"; + METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))) \ "apply an SMT solver to the current goal" diff -r 6d770c2dc60d -r f09f377da49d src/Pure/General/timing.scala --- a/src/Pure/General/timing.scala Fri Oct 07 17:59:19 2016 +0200 +++ b/src/Pure/General/timing.scala Fri Oct 07 21:19:15 2016 +0200 @@ -1,5 +1,4 @@ /* Title: Pure/General/timing.scala - Module: PIDE Author: Makarius Basic support for time measurement. @@ -34,27 +33,34 @@ sealed case class Timing(elapsed: Time, cpu: Time, gc: Time) { + def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant + def resources: Time = cpu + gc + + def factor: Option[Double] = + { + val t1 = elapsed.seconds + val t2 = resources.seconds + if (t1 >= 3.0 && t2 >= 3.0) Some(t2 / t1) else None + } + def + (t: Timing): Timing = Timing(elapsed + t.elapsed, cpu + t.cpu, gc + t.gc) def message: String = elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" - def resources: Time = cpu + gc def message_resources: String = { - val resources = cpu + gc - val t1 = elapsed.seconds - val t2 = resources.seconds - val factor = - if (t1 >= 3.0 && t2 >= 3.0) - String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(t2 / t1)) - else "" - if (t2 >= 3.0) - elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor + val factor_text = + factor match { + case Some(f) => String.format(Locale.ROOT, ", factor %.2f", new java.lang.Double(f)) + case None => "" + } + if (resources.seconds >= 3.0) + elapsed.message_hms + " elapsed time, " + resources.message_hms + " cpu time" + factor_text else - elapsed.message_hms + " elapsed time" + factor + elapsed.message_hms + " elapsed time" + factor_text } override def toString: String = message diff -r 6d770c2dc60d -r f09f377da49d src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri Oct 07 17:59:19 2016 +0200 +++ b/src/Pure/Tools/build.scala Fri Oct 07 21:19:15 2016 +0200 @@ -477,7 +477,7 @@ } try { - val info = Build_Log.Log_File(name, text).parse_session_info(name, false) + val info = Build_Log.Log_File(name, text).parse_session_info(name, command_timings = true) val session_timing = Markup.Elapsed.unapply(info.session_timing) getOrElse 0.0 (info.command_timings, session_timing) } @@ -686,17 +686,8 @@ /* Isabelle tool wrapper */ - val ml_options = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") - val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args => { - def show_settings(): String = - cat_lines(List( - "ISABELLE_BUILD_OPTIONS=" + - quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")), - "") ::: - ml_options.map(opt => opt + "=" + quote(Isabelle_System.getenv(opt)))) - val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")) var select_dirs: List[Path] = Nil @@ -739,7 +730,7 @@ Build and manage Isabelle sessions, depending on implicit settings: -""" + Library.prefix_lines(" ", show_settings()), +""" + Library.prefix_lines(" ", Build_Log.Settings.show()), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "R" -> (_ => requirements = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), @@ -766,7 +757,7 @@ Library.trim_line( Isabelle_System.bash( """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n") - progress.echo(show_settings() + "\n") + progress.echo(Build_Log.Settings.show() + "\n") } val start_time = Time.now() diff -r 6d770c2dc60d -r f09f377da49d src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Fri Oct 07 17:59:19 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Fri Oct 07 21:19:15 2016 +0200 @@ -7,6 +7,7 @@ package isabelle +import java.io.{File => JFile} import java.time.ZonedDateTime import java.time.format.{DateTimeFormatter, DateTimeParseException} @@ -16,6 +17,37 @@ object Build_Log { + /** settings **/ + + object Settings + { + val build_settings = List("ISABELLE_BUILD_OPTIONS") + val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") + val all_settings = build_settings ::: ml_settings + + type Entry = (String, String) + type T = List[Entry] + + object Entry + { + def unapply(s: String): Option[Entry] = + s.indexOf('=') match { + case -1 => None + case i => + val a = s.substring(0, i) + val b = Library.perhaps_unquote(s.substring(i + 1)) + Some((a, b)) + } + def apply(a: String, b: String): String = a + "=" + quote(b) + def getenv(a: String): String = apply(a, Isabelle_System.getenv(a)) + } + + def show(): String = + cat_lines( + build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_))) + } + + /** log file **/ object Log_File @@ -25,6 +57,23 @@ def apply(name: String, text: String): Log_File = Log_File(name, Library.trim_split_lines(text)) + + def apply(file: JFile): Log_File = + { + val name = file.getName + val (base_name, text) = + Library.try_unsuffix(".gz", name) match { + case Some(base_name) => (base_name, File.read_gzip(file)) + case None => + Library.try_unsuffix(".xz", name) match { + case Some(base_name) => (base_name, File.read_xz(file)) + case None => (name, File.read(file)) + } + } + apply(base_name, text) + } + + def apply(path: Path): Log_File = apply(path.file) } class Log_File private(val name: String, val lines: List[String]) @@ -51,11 +100,14 @@ /* settings */ - def get_setting(setting: String): String = - lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting) + def get_setting(a: String): Option[Settings.Entry] = + lines.find(_.startsWith(a + "=")) match { + case Some(line) => Settings.Entry.unapply(line) + case None => None + } - def get_settings(settings: List[String]): List[String] = - settings.map(get_setting(_)) + def get_settings(as: List[String]): Settings.T = + for { a <- as; entry <- get_setting(a) } yield entry /* properties (YXML) */ @@ -77,12 +129,17 @@ /* parse various formats */ - def parse_session_info(session_name: String, full: Boolean): Session_Info = - Build_Log.parse_session_info(log_file, session_name, full) + def parse_session_info( + default_name: String = "", + command_timings: Boolean = false, + ml_statistics: Boolean = false, + task_statistics: Boolean = false): Session_Info = + Build_Log.parse_session_info( + log_file, default_name, command_timings, ml_statistics, task_statistics) - def parse_header: Header = Build_Log.parse_header(log_file) + def parse_header(): Header = Build_Log.parse_header(log_file) - def parse_info: Info = Build_Log.parse_info(log_file) + def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file) } @@ -95,22 +152,30 @@ ml_statistics: List[Properties.T], task_statistics: List[Properties.T]) - private def parse_session_info(log_file: Log_File, name0: String, full: Boolean): Session_Info = + private def parse_session_info( + log_file: Log_File, + default_name: String, + command_timings: Boolean, + ml_statistics: Boolean, + task_statistics: Boolean): Session_Info = { val xml_cache = new XML.Cache() val session_name = log_file.find_line("\fSession.name = ") match { - case None => name0 - case Some(name) if name0 == "" || name0 == name => name + case None => default_name + case Some(name) if default_name == "" || default_name == name => name case Some(name) => log_file.err("log from different session " + quote(name)) } val session_timing = log_file.find_props("\fTiming = ") getOrElse Nil - val command_timings = log_file.filter_props("\fcommand_timing = ") - val ml_statistics = if (full) log_file.filter_props("\fML_statistics = ") else Nil - val task_statistics = if (full) log_file.filter_props("\ftask_statistics = ") else Nil + val command_timings_ = + if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil + val ml_statistics_ = + if (ml_statistics) log_file.filter_props("\fML_statistics = ") else Nil + val task_statistics_ = + if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil - Session_Info(session_name, session_timing, command_timings, ml_statistics, task_statistics) + Session_Info(session_name, session_timing, command_timings_, ml_statistics_, task_statistics_) } @@ -123,7 +188,8 @@ val JENKINS = Value("jenkins") } - sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String]) + sealed case class Header( + kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)]) object Field { @@ -134,125 +200,188 @@ val afp_version = "afp_version" } - val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS") - object AFP { val Date_Format = Date.Format.make_patterns(List("EEE MMM d HH:mm:ss VV yyyy", "EEE MMM d HH:mm:ss O yyyy"), // workaround for jdk-8u102 - s => Word.implode(Word.explode(s).map({ case "CEST" => "GMT+2" case a => a }))) + s => Word.implode(Word.explode(s).map({ + case "CET" | "MET" => "GMT+1" + case "CEST" | "MEST" => "GMT+2" + case "EST" => "GMT+1" // FIXME ?? + case a => a }))) - val Test_Start = new Regex("""^Start test for .+ at (.+), (\w+)$""") - val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""") - val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""") - val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""") - val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings + object Strict_Date + { + def unapply(s: String): Some[Date] = Some(Date_Format.parse(s)) + } + + val Test_Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""") + val Test_Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""") + val Test_End = new Regex("""^End test on (.+), .+, elapsed time:.*$""") + val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\S+)$""") + val AFP_Version = new Regex("""^AFP version: .* -- hg id (\S+)$""") } private def parse_header(log_file: Log_File): Header = { - log_file.lines match { - case AFP.Test_Start(start, hostname) :: _ => - (start, log_file.lines.last) match { - case (AFP.Date_Format(start_date), AFP.Test_End(AFP.Date_Format(end_date))) => - val isabelle_version = - log_file.find_match(AFP.Isabelle_Version) getOrElse - log_file.err("missing Isabelle version") - val afp_version = - log_file.find_match(AFP.AFP_Version) getOrElse - log_file.err("missing AFP version") + def parse_afp(start: Date, hostname: String): Header = + { + val start_date = Field.build_start -> start.toString + val end_date = + log_file.lines.last match { + case AFP.Test_End(AFP.Strict_Date(end_date)) => + List(Field.build_end -> end_date.toString) + case _ => Nil + } + + val build_host = if (hostname == "") Nil else List(Field.build_host -> hostname) - Header(Header_Kind.AFP_TEST, - List( - Field.build_host -> hostname, - Field.build_start -> start_date.toString, - Field.build_end -> end_date.toString, - Field.isabelle_version -> isabelle_version, - Field.afp_version -> afp_version), - log_file.get_settings(AFP.settings)) + val isabelle_version = + log_file.find_match(AFP.Isabelle_Version).map(Field.isabelle_version -> _) + + val afp_version = + log_file.find_match(AFP.AFP_Version).map(Field.afp_version -> _) - case _ => log_file.err("cannot detect start/end date in afp-test log") - } + Header(Header_Kind.AFP_TEST, + start_date :: end_date ::: build_host ::: isabelle_version.toList ::: afp_version.toList, + log_file.get_settings(Settings.all_settings)) + } + + log_file.lines match { + case AFP.Test_Start(AFP.Strict_Date(start_date), hostname) :: _ => + parse_afp(start_date, hostname) + case AFP.Test_Start_Old(AFP.Strict_Date(start_date)) :: _ => + parse_afp(start_date, "") case _ => log_file.err("cannot detect log header format") } } + + /* build info: produced by isabelle build */ + object Session_Status extends Enumeration { - val UNKNOWN = Value("unknown") + val EXISTING = Value("existing") val FINISHED = Value("finished") val FAILED = Value("failed") val CANCELLED = Value("cancelled") } - - /* main log: produced by isatest, afp-test, jenkins etc. */ + sealed case class Session_Entry( + chapter: String, + groups: List[String], + threads: Option[Int], + timing: Timing, + ml_timing: Timing, + status: Session_Status.Value) + { + def finished: Boolean = status == Session_Status.FINISHED + } - sealed case class Info( - ml_options: List[(String, String)], - finished: Map[String, Timing], - timing: Map[String, Timing], - threads: Map[String, Int]) + sealed case class Build_Info(sessions: Map[String, Session_Entry]) { - val sessions: Set[String] = finished.keySet ++ timing.keySet + def session(name: String): Session_Entry = sessions(name) + def get_session(name: String): Option[Session_Entry] = sessions.get(name) - override def toString: String = - sessions.toList.sorted.mkString("Build_Log.Info(", ", ", ")") + def get_default[A](name: String, f: Session_Entry => A, x: A): A = + get_session(name) match { + case Some(entry) => f(entry) + case None => x + } + + def finished(name: String): Boolean = get_default(name, _.finished, false) + def timing(name: String): Timing = get_default(name, _.timing, Timing.zero) + def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero) } - private val Session_Finished1 = - new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") - private val Session_Finished2 = - new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""") - private val Session_Timing = - new Regex("""^Timing (\S+) $(\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") - - private object ML_Option + private def parse_build_info(log_file: Log_File): Build_Info = { - def unapply(s: String): Option[(String, String)] = - s.indexOf('=') match { - case -1 => None - case i => - val a = s.substring(0, i) - Library.try_unquote(s.substring(i + 1)) match { - case Some(b) if Build.ml_options.contains(a) => Some((a, b)) - case _ => None - } - } - } + object Chapter_Name + { + def unapply(s: String): Some[(String, String)] = + space_explode('/', s) match { + case List(chapter, name) => Some((chapter, name)) + case _ => Some(("", s)) + } + } - private def parse_info(log_file: Log_File): Info = - { - val ml_options = new mutable.ListBuffer[(String, String)] - var finished = Map.empty[String, Timing] + val Session_No_Groups = new Regex("""^Session (\S+)$""") + val Session_Groups = new Regex("""^Session (\S+) \((.*)$$""") + val Session_Finished1 = + new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""") + val Session_Finished2 = + new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""") + val Session_Timing = + new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""") + val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""") + val Session_Failed = new Regex("""^(\S+) FAILED""") + val Session_Cancelled = new Regex("""^(\S+) CANCELLED""") + + var chapter = Map.empty[String, String] + var groups = Map.empty[String, List[String]] + var threads = Map.empty[String, Int] var timing = Map.empty[String, Timing] - var threads = Map.empty[String, Int] + var ml_timing = Map.empty[String, Timing] + var started = Set.empty[String] + var failed = Set.empty[String] + var cancelled = Set.empty[String] + def all_sessions: Set[String] = + chapter.keySet ++ groups.keySet ++ threads.keySet ++ + timing.keySet ++ ml_timing.keySet ++ failed ++ cancelled ++ started + for (line <- log_file.lines) { line match { + case Session_No_Groups(Chapter_Name(chapt, name)) => + chapter += (name -> chapt) + groups += (name -> Nil) + case Session_Groups(Chapter_Name(chapt, name), grps) => + chapter += (name -> chapt) + groups += (name -> Word.explode(grps)) + case Session_Started(name) => + started += name case Session_Finished1(name, Value.Int(e1), Value.Int(e2), Value.Int(e3), Value.Int(c1), Value.Int(c2), Value.Int(c3)) => val elapsed = Time.hms(e1, e2, e3) val cpu = Time.hms(c1, c2, c3) - finished += (name -> Timing(elapsed, cpu, Time.zero)) + timing += (name -> Timing(elapsed, cpu, Time.zero)) case Session_Finished2(name, Value.Int(e1), Value.Int(e2), Value.Int(e3)) => val elapsed = Time.hms(e1, e2, e3) - finished += (name -> Timing(elapsed, Time.zero, Time.zero)) + timing += (name -> Timing(elapsed, Time.zero, Time.zero)) case Session_Timing(name, Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) => val elapsed = Time.seconds(e) val cpu = Time.seconds(c) val gc = Time.seconds(g) - timing += (name -> Timing(elapsed, cpu, gc)) + ml_timing += (name -> Timing(elapsed, cpu, gc)) threads += (name -> t) - case ML_Option(a, b) => ml_options += (a -> b) case _ => } } - Info(ml_options.toList, finished, timing, threads) + val sessions = + Map( + (for (name <- all_sessions.toList) yield { + val status = + if (failed(name)) Session_Status.FAILED + else if (cancelled(name)) Session_Status.CANCELLED + else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name)) + Session_Status.FINISHED + else if (started(name)) Session_Status.FAILED + else Session_Status.EXISTING + val entry = + Session_Entry( + chapter.getOrElse(name, ""), + groups.getOrElse(name, Nil), + threads.get(name), + timing.getOrElse(name, Timing.zero), + ml_timing.getOrElse(name, Timing.zero), + status) + (name -> entry) + }):_*) + Build_Info(sessions) } } diff -r 6d770c2dc60d -r f09f377da49d src/Pure/Tools/build_stats.scala --- a/src/Pure/Tools/build_stats.scala Fri Oct 07 17:59:19 2016 +0200 +++ b/src/Pure/Tools/build_stats.scala Fri Oct 07 21:19:15 2016 +0200 @@ -29,16 +29,16 @@ val all_infos = Par_List.map((job_info: CI_API.Job_Info) => - (job_info.timestamp / 1000, job_info.read_output.parse_info), job_infos) + (job_info.timestamp / 1000, job_info.read_output.parse_build_info), job_infos) val all_sessions = (Set.empty[String] /: all_infos)( - { case (s, (_, info)) => s ++ info.sessions }) + { case (s, (_, info)) => s ++ info.sessions.keySet }) - def check_threshold(info: Build_Log.Info, session: String): Boolean = - info.finished.get(session) match { - case Some(t) => t.elapsed >= elapsed_threshold - case None => false - } + def check_threshold(info: Build_Log.Build_Info, session: String): Boolean = + { + val t = info.timing(session) + !t.is_zero && t.elapsed >= elapsed_threshold + } val sessions = for { @@ -51,12 +51,16 @@ Isabelle_System.with_tmp_file(session, "png") { data_file => Isabelle_System.with_tmp_file(session, "gnuplot") { plot_file => val data = - for { (t, info) <- all_infos if info.finished.isDefinedAt(session) } + for { (t, info) <- all_infos if info.finished(session) } yield { - val finished = info.finished.getOrElse(session, Timing.zero) - val timing = info.timing.getOrElse(session, Timing.zero) - List(t.toString, finished.elapsed.minutes, finished.cpu.minutes, - timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ") + val timing1 = info.timing(session) + val timing2 = info.ml_timing(session) + List(t.toString, + timing1.elapsed.minutes, + timing1.cpu.minutes, + timing2.elapsed.minutes, + timing2.cpu.minutes, + timing2.gc.minutes).mkString(" ") } File.write(data_file, cat_lines(data)) diff -r 6d770c2dc60d -r f09f377da49d src/Pure/Tools/ci_api.scala --- a/src/Pure/Tools/ci_api.scala Fri Oct 07 17:59:19 2016 +0200 +++ b/src/Pure/Tools/ci_api.scala Fri Oct 07 21:19:15 2016 +0200 @@ -45,12 +45,9 @@ session_logs: List[(String, URL)]) { def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output)) - def read_log(name: String, full: Boolean): Build_Log.Session_Info = - { - val text = - session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "" - Build_Log.Log_File(name, text).parse_session_info(name, full) - } + def read_log_file(name: String): Build_Log.Log_File = + Build_Log.Log_File(name, + session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "") } def build_job_builds(job_name: String): List[Job_Info] = diff -r 6d770c2dc60d -r f09f377da49d src/Pure/Tools/ci_profile.scala --- a/src/Pure/Tools/ci_profile.scala Fri Oct 07 17:59:19 2016 +0200 +++ b/src/Pure/Tools/ci_profile.scala Fri Oct 07 21:19:15 2016 +0200 @@ -86,7 +86,7 @@ override final def apply(args: List[String]): Unit = { print_section("CONFIGURATION") - Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt)))) + println(Build_Log.Settings.show()) val props = load_properties() System.getProperties().putAll(props)