# HG changeset patch # User wenzelm # Date 1475958982 -7200 # Node ID c2b41b073d8a23a1121f47c581d2071f0e5d748c # Parent 6cfd429a4296195648f5b29785d7542f559157d0 build_history log files with formal meta info; diff -r 6cfd429a4296 -r c2b41b073d8a src/Pure/General/date.scala --- a/src/Pure/General/date.scala Sat Oct 08 22:08:31 2016 +0200 +++ b/src/Pure/General/date.scala Sat Oct 08 22:36:22 2016 +0200 @@ -8,7 +8,7 @@ import java.util.Locale -import java.time.{Instant, ZonedDateTime, ZoneId} +import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId} import java.time.format.{DateTimeFormatter, DateTimeParseException} import java.time.temporal.TemporalAccessor @@ -85,6 +85,9 @@ sealed case class Date(rep: ZonedDateTime) { + def midnight: Date = + new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone)) + def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone)) def to_utc: Date = to(ZoneId.of("UTC")) diff -r 6cfd429a4296 -r c2b41b073d8a src/Pure/System/progress.scala --- a/src/Pure/System/progress.scala Sat Oct 08 22:08:31 2016 +0200 +++ b/src/Pure/System/progress.scala Sat Oct 08 22:36:22 2016 +0200 @@ -18,9 +18,13 @@ object Ignore_Progress extends Progress -class Console_Progress(verbose: Boolean = false) extends Progress +class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress { - override def echo(msg: String) { Console.println(msg) } + override def echo(msg: String) + { + if (stderr) Console.err.println(msg) else Console.println(msg) + } + override def theory(session: String, theory: String): Unit = if (verbose) echo(session + ": theory " + theory) diff -r 6cfd429a4296 -r c2b41b073d8a src/Pure/Tools/build_history.scala --- a/src/Pure/Tools/build_history.scala Sat Oct 08 22:08:31 2016 +0200 +++ b/src/Pure/Tools/build_history.scala Sat Oct 08 22:36:22 2016 +0200 @@ -8,11 +8,27 @@ import java.io.{File => JFile} -import java.util.Calendar +import java.time.format.DateTimeFormatter +import java.util.{Calendar, Locale} object Build_History { + /* log files */ + + val BUILD_HISTORY = "build_history" + val META_INFO = "\fmeta_info = " + + def log_date(date: Date): String = + String.format(Locale.ROOT, "%s.%05d", + DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep), + new java.lang.Long((date.time - date.midnight.time).ms / 1000)) + + def log_name(date: Date, parts: String*): String = + (BUILD_HISTORY :: log_date(date) :: parts.toList).mkString("", "_", ".log.gz") + + + /** other Isabelle environment **/ private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String) @@ -42,6 +58,7 @@ Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out) val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings") + val log_dir: Path = isabelle_home_user + Path.explode("log") /* reset settings */ @@ -80,9 +97,9 @@ arch_64: Boolean = false, heap: Int = default_heap, max_heap: Option[Int] = None, - more_settings: List[String]) + more_settings: List[String]): String = { - val ml_settings = + val (ml_platform, ml_settings) = { val windows_32 = "x86-windows" val windows_64 = "x86_64-windows" @@ -122,10 +139,11 @@ " --gcthreads " + threads + (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "") - List( - "ML_HOME=" + File.bash_path(ml_home(ml_platform)), - "ML_PLATFORM=" + quote(ml_platform), - "ML_OPTIONS=" + quote(ml_options)) + (ml_platform, + List( + "ML_HOME=" + File.bash_path(ml_home(ml_platform)), + "ML_PLATFORM=" + quote(ml_platform), + "ML_OPTIONS=" + quote(ml_options))) } val thread_settings = @@ -138,6 +156,8 @@ (if (more_settings.isEmpty) Nil else List(more_settings)) File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_)))) + + ml_platform } } @@ -190,11 +210,15 @@ hg.update(rev = rev, clean = true) progress.echo_if(verbose, hg.log(rev, options = "-l1")) + val isabelle_version = hg.identify(rev, options = "-i") val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier) /* main */ + val build_history_date = Date.now() + val build_host = Library.trim_line(Isabelle_System.bash("hostname").check.out) + var first_build = true for (threads <- threads_list) yield { @@ -202,7 +226,8 @@ other_isabelle.reset_settings(components_base, nonfree) other_isabelle.resolve_components(verbose) - other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings) + val ml_platform = + other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings) val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out) val isabelle_output_log = isabelle_output + Path.explode("log") @@ -227,7 +252,26 @@ if (multicore_base && !first_build && isabelle_base_log.is_dir) other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log) - val res = other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = true) + val build_start = Date.now() + val res = other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose) + val build_end = Date.now() + + val log_path = + other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) + + Path.explode(log_name(build_history_date, ml_platform, "M" + threads)) + Isabelle_System.mkdirs(log_path.dir) + + val meta_info = + List(Build_Log.Field.build_engine -> BUILD_HISTORY, + Build_Log.Field.build_host -> build_host, + Build_Log.Field.build_start -> Build_Log.Log_File.Date_Format(build_start), + Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end), + Build_Log.Field.isabelle_version -> isabelle_version) + + File.write_gzip(log_path, + Build_Log.Log_File.print_props(META_INFO, meta_info) + "\n" + res.out) + + Output.writeln(log_path.implode, stdout = true) if (multicore_base && first_build && isabelle_output_log.is_dir) other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log) @@ -304,7 +348,7 @@ using(Mercurial.open_repository(Path.explode(root)))(hg => { - val progress = new Console_Progress(false) + val progress = new Console_Progress(stderr = true) val results = build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier, components_base = components_base, fresh = fresh, nonfree = nonfree, diff -r 6cfd429a4296 -r c2b41b073d8a src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Sat Oct 08 22:08:31 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Sat Oct 08 22:36:22 2016 +0200 @@ -132,6 +132,12 @@ Date.Format.make(fmts, tune) } + + + /* inlined content */ + + def print_props(prefix: String, props: Properties.T): String = + prefix + YXML.string_of_body(XML.Encode.properties(props)) } class Log_File private(val name: String, val lines: List[String]) @@ -294,6 +300,10 @@ } log_file.lines match { + case line :: _ if line.startsWith(Build_History.META_INFO) => + Meta_Info(log_file.find_props(Build_History.META_INFO).get, + log_file.get_settings(Settings.all_settings)) + case Isatest.Start(log_file.Strict_Date(start), host) :: _ => parse(Isatest.engine, host, start, Isatest.End, Isatest.Isabelle_Version, Isatest.No_AFP_Version)