src/Pure/Admin/build_status.scala
changeset 65792 c58752102b34
parent 65791 cf48ef4f4e63
child 65794 a880f41a8d0f
     1.1 --- a/src/Pure/Admin/build_status.scala	Tue May 09 20:02:31 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 09 20:36:34 2017 +0200
     1.3 @@ -57,7 +57,8 @@
     1.4  
     1.5    /* read data */
     1.6  
     1.7 -  sealed case class Data(date: Date, entries: List[(String, List[Session])])
     1.8 +  sealed case class Data(date: Date, entries: List[Data_Entry])
     1.9 +  sealed case class Data_Entry(name: String, hosts: List[String], sessions: List[Session])
    1.10    sealed case class Session(name: String, threads: Int, entries: List[Entry])
    1.11    {
    1.12      def timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.timing
    1.13 @@ -76,8 +77,12 @@
    1.14      verbose: Boolean = false): Data =
    1.15    {
    1.16      val date = Date.now()
    1.17 +    var data_hosts = Map.empty[String, Set[String]]
    1.18      var data_entries = Map.empty[String, Map[String, Session]]
    1.19  
    1.20 +    def get_hosts(data_name: String): Set[String] =
    1.21 +      data_hosts.getOrElse(data_name, Set.empty)
    1.22 +
    1.23      val store = Build_Log.store(options)
    1.24      using(store.open_database())(db =>
    1.25      {
    1.26 @@ -86,6 +91,7 @@
    1.27          val columns =
    1.28            List(
    1.29              Build_Log.Data.pull_date,
    1.30 +            Build_Log.Prop.build_host,
    1.31              Build_Log.Settings.ISABELLE_BUILD_OPTIONS,
    1.32              Build_Log.Settings.ML_PLATFORM,
    1.33              Build_Log.Data.session_name,
    1.34 @@ -136,6 +142,9 @@
    1.35                    Build_Log.Data.ml_timing_gc),
    1.36                  heap_size = res.long(Build_Log.Data.heap_size))
    1.37  
    1.38 +            res.get_string(Build_Log.Prop.build_host).foreach(host =>
    1.39 +              data_hosts += (data_name -> (get_hosts(data_name) + host)))
    1.40 +
    1.41              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.42              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.43              val session = Session(session_name, threads, entry :: entries)
    1.44 @@ -145,12 +154,14 @@
    1.45        }
    1.46      })
    1.47  
    1.48 -    Data(date,
    1.49 +    val sorted_entries =
    1.50        (for {
    1.51 -        (data_name, sessions) <- data_entries.toList
    1.52 +        (name, sessions) <- data_entries.toList
    1.53          sorted_sessions <-
    1.54            proper_list(sessions.toList.map(_._2).filter(_.check_timing).sortBy(_.order))
    1.55 -      } yield (data_name, sorted_sessions)).sortBy(_._1))
    1.56 +      } yield Data_Entry(name, get_hosts(name).toList.sorted, sorted_sessions)).sortBy(_.name)
    1.57 +
    1.58 +    Data(date, sorted_entries)
    1.59    }
    1.60  
    1.61  
    1.62 @@ -168,11 +179,14 @@
    1.63      File.write(target_dir + Path.basic("index.html"),
    1.64        HTML.output_document(
    1.65          List(HTML.title("Isabelle build status")),
    1.66 -        List(HTML.chapter("Isabelle build status (" + data.date + ")"),
    1.67 -          HTML.itemize(data.entries.map({ case (data_name, _) =>
    1.68 -            List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
    1.69 +        List(HTML.chapter("Isabelle build status"),
    1.70 +          HTML.itemize(data.entries.map({ case data_entry =>
    1.71 +            List(HTML.link(clean_name(data_entry.name) + "/index.html", HTML.text(data_entry.name)))
    1.72 +          })))))
    1.73  
    1.74 -    for ((data_name, sessions) <- data.entries) {
    1.75 +    for (data_entry <- data.entries) {
    1.76 +      val data_name = data_entry.name
    1.77 +
    1.78        progress.echo("output " + quote(data_name))
    1.79  
    1.80        val dir = target_dir + Path.basic(clean_name(data_name))
    1.81 @@ -257,17 +271,23 @@
    1.82  
    1.83                session.name -> plot_names
    1.84              }
    1.85 -          }, sessions).toMap
    1.86 +          }, data_entry.sessions).toMap
    1.87  
    1.88        File.write(dir + Path.basic("index.html"),
    1.89          HTML.output_document(
    1.90            List(HTML.title("Isabelle build status for " + data_name)),
    1.91 -          HTML.chapter("Isabelle build status for " + data_name + " (" + data.date + ")") ::
    1.92 -          HTML.itemize(
    1.93 -            sessions.map(session =>
    1.94 -              HTML.link("#session_" + session.name, HTML.text(session.name)) ::
    1.95 -              HTML.text(" (" + session.timing.message_resources + ")"))) ::
    1.96 -          sessions.flatMap(session =>
    1.97 +          HTML.chapter("Isabelle build status for " + data_name) ::
    1.98 +          HTML.par(
    1.99 +            List(HTML.itemize(
   1.100 +              List(
   1.101 +                HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)),
   1.102 +                HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))) ::
   1.103 +          HTML.par(
   1.104 +            List(HTML.itemize(
   1.105 +              data_entry.sessions.map(session =>
   1.106 +                HTML.link("#session_" + session.name, HTML.text(session.name)) ::
   1.107 +                HTML.text(" (" + session.timing.message_resources + ")"))))) ::
   1.108 +          data_entry.sessions.flatMap(session =>
   1.109              List(
   1.110                HTML.section(session.name) + HTML.id("session_" + session.name),
   1.111                HTML.par(