build_history log files with formal meta info;
authorwenzelm
Sat Oct 08 22:36:22 2016 +0200 (2016-10-08)
changeset 64117c2b41b073d8a
parent 64116 6cfd429a4296
child 64118 0996fab2ec03
build_history log files with formal meta info;
src/Pure/General/date.scala
src/Pure/System/progress.scala
src/Pure/Tools/build_history.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/General/date.scala	Sat Oct 08 22:08:31 2016 +0200
     1.2 +++ b/src/Pure/General/date.scala	Sat Oct 08 22:36:22 2016 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  
     1.6  import java.util.Locale
     1.7 -import java.time.{Instant, ZonedDateTime, ZoneId}
     1.8 +import java.time.{Instant, ZonedDateTime, LocalTime, ZoneId}
     1.9  import java.time.format.{DateTimeFormatter, DateTimeParseException}
    1.10  import java.time.temporal.TemporalAccessor
    1.11  
    1.12 @@ -85,6 +85,9 @@
    1.13  
    1.14  sealed case class Date(rep: ZonedDateTime)
    1.15  {
    1.16 +  def midnight: Date =
    1.17 +    new Date(ZonedDateTime.of(rep.toLocalDate, LocalTime.MIDNIGHT, rep.getZone))
    1.18 +
    1.19    def to(zone: ZoneId): Date = new Date(rep.withZoneSameInstant(zone))
    1.20    def to_utc: Date = to(ZoneId.of("UTC"))
    1.21  
     2.1 --- a/src/Pure/System/progress.scala	Sat Oct 08 22:08:31 2016 +0200
     2.2 +++ b/src/Pure/System/progress.scala	Sat Oct 08 22:36:22 2016 +0200
     2.3 @@ -18,9 +18,13 @@
     2.4  
     2.5  object Ignore_Progress extends Progress
     2.6  
     2.7 -class Console_Progress(verbose: Boolean = false) extends Progress
     2.8 +class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
     2.9  {
    2.10 -  override def echo(msg: String) { Console.println(msg) }
    2.11 +  override def echo(msg: String)
    2.12 +  {
    2.13 +    if (stderr) Console.err.println(msg) else Console.println(msg)
    2.14 +  }
    2.15 +
    2.16    override def theory(session: String, theory: String): Unit =
    2.17      if (verbose) echo(session + ": theory " + theory)
    2.18  
     3.1 --- a/src/Pure/Tools/build_history.scala	Sat Oct 08 22:08:31 2016 +0200
     3.2 +++ b/src/Pure/Tools/build_history.scala	Sat Oct 08 22:36:22 2016 +0200
     3.3 @@ -8,11 +8,27 @@
     3.4  
     3.5  
     3.6  import java.io.{File => JFile}
     3.7 -import java.util.Calendar
     3.8 +import java.time.format.DateTimeFormatter
     3.9 +import java.util.{Calendar, Locale}
    3.10  
    3.11  
    3.12  object Build_History
    3.13  {
    3.14 +  /* log files */
    3.15 +
    3.16 +  val BUILD_HISTORY = "build_history"
    3.17 +  val META_INFO = "\fmeta_info = "
    3.18 +
    3.19 +  def log_date(date: Date): String =
    3.20 +    String.format(Locale.ROOT, "%s.%05d",
    3.21 +      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
    3.22 +      new java.lang.Long((date.time - date.midnight.time).ms / 1000))
    3.23 +
    3.24 +  def log_name(date: Date, parts: String*): String =
    3.25 +    (BUILD_HISTORY :: log_date(date) :: parts.toList).mkString("", "_", ".log.gz")
    3.26 +
    3.27 +
    3.28 +
    3.29    /** other Isabelle environment **/
    3.30  
    3.31    private class Other_Isabelle(progress: Progress, isabelle_home: Path, isabelle_identifier: String)
    3.32 @@ -42,6 +58,7 @@
    3.33        Path.explode(other_isabelle("getenv -b ISABELLE_HOME_USER").check.out)
    3.34  
    3.35      val etc_settings: Path = isabelle_home_user + Path.explode("etc/settings")
    3.36 +    val log_dir: Path = isabelle_home_user + Path.explode("log")
    3.37  
    3.38  
    3.39      /* reset settings */
    3.40 @@ -80,9 +97,9 @@
    3.41        arch_64: Boolean = false,
    3.42        heap: Int = default_heap,
    3.43        max_heap: Option[Int] = None,
    3.44 -      more_settings: List[String])
    3.45 +      more_settings: List[String]): String =
    3.46      {
    3.47 -      val ml_settings =
    3.48 +      val (ml_platform, ml_settings) =
    3.49        {
    3.50          val windows_32 = "x86-windows"
    3.51          val windows_64 = "x86_64-windows"
    3.52 @@ -122,10 +139,11 @@
    3.53            " --gcthreads " + threads +
    3.54            (if (ml_platform.endsWith("-windows")) " --codepage utf8" else "")
    3.55  
    3.56 -        List(
    3.57 -          "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
    3.58 -          "ML_PLATFORM=" + quote(ml_platform),
    3.59 -          "ML_OPTIONS=" + quote(ml_options))
    3.60 +        (ml_platform,
    3.61 +          List(
    3.62 +            "ML_HOME=" + File.bash_path(ml_home(ml_platform)),
    3.63 +            "ML_PLATFORM=" + quote(ml_platform),
    3.64 +            "ML_OPTIONS=" + quote(ml_options)))
    3.65        }
    3.66  
    3.67        val thread_settings =
    3.68 @@ -138,6 +156,8 @@
    3.69            (if (more_settings.isEmpty) Nil else List(more_settings))
    3.70  
    3.71        File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_))))
    3.72 +
    3.73 +      ml_platform
    3.74      }
    3.75    }
    3.76  
    3.77 @@ -190,11 +210,15 @@
    3.78      hg.update(rev = rev, clean = true)
    3.79      progress.echo_if(verbose, hg.log(rev, options = "-l1"))
    3.80  
    3.81 +    val isabelle_version = hg.identify(rev, options = "-i")
    3.82      val other_isabelle = new Other_Isabelle(progress, hg.root, isabelle_identifier)
    3.83  
    3.84  
    3.85      /* main */
    3.86  
    3.87 +    val build_history_date = Date.now()
    3.88 +    val build_host = Library.trim_line(Isabelle_System.bash("hostname").check.out)
    3.89 +
    3.90      var first_build = true
    3.91      for (threads <- threads_list) yield
    3.92      {
    3.93 @@ -202,7 +226,8 @@
    3.94  
    3.95        other_isabelle.reset_settings(components_base, nonfree)
    3.96        other_isabelle.resolve_components(verbose)
    3.97 -      other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
    3.98 +      val ml_platform =
    3.99 +        other_isabelle.augment_settings(threads, arch_64, heap, max_heap, more_settings)
   3.100  
   3.101        val isabelle_output = Path.explode(other_isabelle("getenv -b ISABELLE_OUTPUT").check.out)
   3.102        val isabelle_output_log = isabelle_output + Path.explode("log")
   3.103 @@ -227,7 +252,26 @@
   3.104        if (multicore_base && !first_build && isabelle_base_log.is_dir)
   3.105          other_isabelle.copy_dir(isabelle_base_log, isabelle_output_log)
   3.106  
   3.107 -      val res = other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = true)
   3.108 +      val build_start = Date.now()
   3.109 +      val res = other_isabelle("build " + File.bash_args(build_args), redirect = true, echo = verbose)
   3.110 +      val build_end = Date.now()
   3.111 +
   3.112 +      val log_path =
   3.113 +        other_isabelle.log_dir + Path.explode(build_history_date.rep.getYear.toString) +
   3.114 +          Path.explode(log_name(build_history_date, ml_platform, "M" + threads))
   3.115 +      Isabelle_System.mkdirs(log_path.dir)
   3.116 +
   3.117 +      val meta_info =
   3.118 +        List(Build_Log.Field.build_engine -> BUILD_HISTORY,
   3.119 +          Build_Log.Field.build_host -> build_host,
   3.120 +          Build_Log.Field.build_start -> Build_Log.Log_File.Date_Format(build_start),
   3.121 +          Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end),
   3.122 +          Build_Log.Field.isabelle_version -> isabelle_version)
   3.123 +
   3.124 +      File.write_gzip(log_path,
   3.125 +        Build_Log.Log_File.print_props(META_INFO, meta_info) + "\n" + res.out)
   3.126 +
   3.127 +      Output.writeln(log_path.implode, stdout = true)
   3.128  
   3.129        if (multicore_base && first_build && isabelle_output_log.is_dir)
   3.130          other_isabelle.copy_dir(isabelle_output_log, isabelle_base_log)
   3.131 @@ -304,7 +348,7 @@
   3.132  
   3.133        using(Mercurial.open_repository(Path.explode(root)))(hg =>
   3.134          {
   3.135 -          val progress = new Console_Progress(false)
   3.136 +          val progress = new Console_Progress(stderr = true)
   3.137            val results =
   3.138              build_history(progress, hg, rev = rev, isabelle_identifier = isabelle_identifier,
   3.139                components_base = components_base, fresh = fresh, nonfree = nonfree,
     4.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 22:08:31 2016 +0200
     4.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 22:36:22 2016 +0200
     4.3 @@ -132,6 +132,12 @@
     4.4  
     4.5        Date.Format.make(fmts, tune)
     4.6      }
     4.7 +
     4.8 +
     4.9 +    /* inlined content */
    4.10 +
    4.11 +    def print_props(prefix: String, props: Properties.T): String =
    4.12 +      prefix + YXML.string_of_body(XML.Encode.properties(props))
    4.13    }
    4.14  
    4.15    class Log_File private(val name: String, val lines: List[String])
    4.16 @@ -294,6 +300,10 @@
    4.17      }
    4.18  
    4.19      log_file.lines match {
    4.20 +      case line :: _ if line.startsWith(Build_History.META_INFO) =>
    4.21 +        Meta_Info(log_file.find_props(Build_History.META_INFO).get,
    4.22 +          log_file.get_settings(Settings.all_settings))
    4.23 +
    4.24        case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
    4.25          parse(Isatest.engine, host, start, Isatest.End,
    4.26            Isatest.Isabelle_Version, Isatest.No_AFP_Version)