more output;
authorwenzelm
Tue May 09 21:43:46 2017 +0200 (2017-05-09)
changeset 657967d1c5150af70
parent 65795 c60b1a2c3abc
child 65797 d76c9c5c0656
more output;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Tue May 09 21:27:34 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 09 21:43:46 2017 +0200
     1.3 @@ -63,6 +63,10 @@
     1.4    {
     1.5      require(entries.nonEmpty)
     1.6  
     1.7 +    def pull_date: Date = entries.head.pull_date
     1.8 +    def isabelle_version: String = entries.head.isabelle_version
     1.9 +    def afp_version: String = entries.head.afp_version
    1.10 +
    1.11      def timing: Timing = entries.head.timing
    1.12      def ml_timing: Timing = entries.head.ml_timing
    1.13      def order: Long = - timing.elapsed.ms
    1.14 @@ -70,7 +74,8 @@
    1.15      def check_timing: Boolean = entries.length >= 3
    1.16      def check_heap: Boolean = entries.forall(_.heap_size > 0)
    1.17    }
    1.18 -  sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing, heap_size: Long)
    1.19 +  sealed case class Entry(pull_date: Date, isabelle_version: String, afp_version: String,
    1.20 +    timing: Timing, ml_timing: Timing, heap_size: Long)
    1.21  
    1.22    def read_data(options: Options,
    1.23      progress: Progress = No_Progress,
    1.24 @@ -94,6 +99,8 @@
    1.25            List(
    1.26              Build_Log.Data.pull_date,
    1.27              Build_Log.Prop.build_host,
    1.28 +            Build_Log.Prop.isabelle_version,
    1.29 +            Build_Log.Prop.afp_version,
    1.30              Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
    1.31              Build_Log.Settings.ML_PLATFORM,
    1.32              Build_Log.Data.session_name,
    1.33 @@ -133,15 +140,20 @@
    1.34                  (if (threads == 1) "" else ", " + threads + " threads")
    1.35  
    1.36              val entry =
    1.37 -              Entry(res.date(Build_Log.Data.pull_date),
    1.38 -                res.timing(
    1.39 -                  Build_Log.Data.timing_elapsed,
    1.40 -                  Build_Log.Data.timing_cpu,
    1.41 -                  Build_Log.Data.timing_gc),
    1.42 -                res.timing(
    1.43 -                  Build_Log.Data.ml_timing_elapsed,
    1.44 -                  Build_Log.Data.ml_timing_cpu,
    1.45 -                  Build_Log.Data.ml_timing_gc),
    1.46 +              Entry(
    1.47 +                pull_date = res.date(Build_Log.Data.pull_date),
    1.48 +                isabelle_version = res.string(Build_Log.Prop.isabelle_version),
    1.49 +                afp_version = res.string(Build_Log.Prop.afp_version),
    1.50 +                timing =
    1.51 +                  res.timing(
    1.52 +                    Build_Log.Data.timing_elapsed,
    1.53 +                    Build_Log.Data.timing_cpu,
    1.54 +                    Build_Log.Data.timing_gc),
    1.55 +                ml_timing =
    1.56 +                  res.timing(
    1.57 +                    Build_Log.Data.ml_timing_elapsed,
    1.58 +                    Build_Log.Data.ml_timing_cpu,
    1.59 +                    Build_Log.Data.ml_timing_gc),
    1.60                  heap_size = res.long(Build_Log.Data.heap_size))
    1.61  
    1.62              res.get_string(Build_Log.Prop.build_host).foreach(host =>
    1.63 @@ -206,7 +218,7 @@
    1.64                File.write(data_file,
    1.65                  cat_lines(
    1.66                    session.entries.map(entry =>
    1.67 -                    List(entry.date.unix_epoch.toString,
    1.68 +                    List(entry.pull_date.unix_epoch.toString,
    1.69                        entry.timing.elapsed.minutes,
    1.70                        entry.timing.resources.minutes,
    1.71                        entry.ml_timing.elapsed.minutes,
    1.72 @@ -298,11 +310,13 @@
    1.73                HTML.section(session.name) + HTML.id("session_" + session.name),
    1.74                HTML.par(
    1.75                  HTML.itemize(List(
    1.76 -                  HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString),
    1.77 -                  HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)),
    1.78                    HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
    1.79                    HTML.bold(HTML.text("ML timing: ")) ::
    1.80 -                    HTML.text(session.ml_timing.message_resources))) ::
    1.81 +                    HTML.text(session.ml_timing.message_resources)) :::
    1.82 +                  proper_string(session.isabelle_version).map(s =>
    1.83 +                    HTML.bold(HTML.text("Isabelle version: ")) :: HTML.text(s)).toList :::
    1.84 +                  proper_string(session.afp_version).map(s =>
    1.85 +                    HTML.bold(HTML.text("AFP version: ")) :: HTML.text(s)).toList) ::
    1.86                  session_plots.getOrElse(session.name, Nil).map(plot_name =>
    1.87                    HTML.image(plot_name) +
    1.88                      HTML.width(image_size._1 / 2) +