src/Pure/Admin/build_status.scala
changeset 65762 295b845243d3
parent 65760 a51290fd62d9
child 65763 dbadcc3fbe33
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 21:38:16 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 21:42:23 2017 +0200
     1.3 @@ -38,14 +38,16 @@
     1.4    val standard_profiles: List[Profile] =
     1.5      Jenkins.build_status_profiles ::: Isabelle_Cronjob.build_status_profiles
     1.6  
     1.7 -  sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
     1.8  
     1.9 -  sealed case class Data(date: Date, entries: Map[String, Map[String, List[Entry]]])
    1.10 +  sealed case class Data(date: Date, entries: List[(String, List[Session])])
    1.11 +  sealed case class Session(name: String, entries: List[Entry])
    1.12    {
    1.13 -    def sorted_entries: List[(String, List[(String, List[Entry])])] =
    1.14 -      entries.toList.sortBy(_._1).map({ case (name, session_entries) =>
    1.15 -        (name, session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse) })
    1.16 +    def timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.timing
    1.17 +    def ml_timing: Timing = if (entries.isEmpty) Timing.zero else entries.head.ml_timing
    1.18 +    def order: Long = - timing.elapsed.ms
    1.19 +    def check: Boolean = entries.length >= 3
    1.20    }
    1.21 +  sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
    1.22  
    1.23  
    1.24    /* read data */
    1.25 @@ -58,7 +60,7 @@
    1.26      verbose: Boolean = false): Data =
    1.27    {
    1.28      val date = Date.now()
    1.29 -    var data_entries = Map.empty[String, Map[String, List[Entry]]]
    1.30 +    var data_entries = Map.empty[String, Map[String, Session]]
    1.31  
    1.32      val store = Build_Log.store(options)
    1.33      using(store.open_database())(db =>
    1.34 @@ -97,12 +99,12 @@
    1.35                }
    1.36              val threads = res.get_int(Build_Log.Data.threads).getOrElse(1)
    1.37  
    1.38 -            val name =
    1.39 +            val data_name =
    1.40                profile.name +
    1.41                  "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
    1.42                  "_M" + (threads_option max threads)
    1.43  
    1.44 -            val session = res.string(Build_Log.Data.session_name)
    1.45 +            val name = res.string(Build_Log.Data.session_name)
    1.46              val entry =
    1.47                Entry(res.date(Build_Log.Data.pull_date),
    1.48                  res.timing(
    1.49 @@ -114,26 +116,19 @@
    1.50                    Build_Log.Data.ml_timing_cpu,
    1.51                    Build_Log.Data.ml_timing_gc))
    1.52  
    1.53 -            val session_entries = data_entries.getOrElse(name, Map.empty)
    1.54 -            val entries = session_entries.getOrElse(session, Nil)
    1.55 -            data_entries += (name -> (session_entries + (session -> (entry :: entries))))
    1.56 +            val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.57 +            val entries = sessions.get(name).map(_.entries) getOrElse Nil
    1.58 +            data_entries += (data_name -> (sessions + (name -> Session(name, entry :: entries))))
    1.59            }
    1.60          })
    1.61        }
    1.62      })
    1.63  
    1.64      Data(date,
    1.65 -      for {
    1.66 -        (name, session_entries) <- data_entries
    1.67 -        session_entries1 <-
    1.68 -          {
    1.69 -            val session_entries1 =
    1.70 -              for { (session, entries) <- session_entries if entries.length >= 3 }
    1.71 -              yield (session, entries)
    1.72 -            if (session_entries1.isEmpty) None
    1.73 -            else Some(session_entries1)
    1.74 -          }
    1.75 -      } yield (name, session_entries1))
    1.76 +      (for {
    1.77 +        (data_name, sessions) <- data_entries.toList
    1.78 +        sorted_sessions <- proper_list(sessions.toList.map(_._2).filter(_.check).sortBy(_.order))
    1.79 +      } yield (data_name, sorted_sessions)).sortBy(_._1))
    1.80    }
    1.81  
    1.82  
    1.83 @@ -144,93 +139,86 @@
    1.84      target_dir: Path = default_target_dir,
    1.85      image_size: (Int, Int) = default_image_size)
    1.86    {
    1.87 -    val data_entries = data.sorted_entries
    1.88 -
    1.89 -    for ((data_name, session_entries) <- data_entries) {
    1.90 +    for ((data_name, sessions) <- data.entries) {
    1.91        val dir = target_dir + Path.explode(data_name)
    1.92        progress.echo("output " + dir)
    1.93        Isabelle_System.mkdirs(dir)
    1.94  
    1.95 -      Par_List.map[(String, List[isabelle.Build_Status.Entry]), List[Process_Result]](
    1.96 -        { case (session, entries) =>
    1.97 -          Isabelle_System.with_tmp_file(session, "data") { data_file =>
    1.98 -            Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
    1.99 +      Par_List.map[Session, List[Process_Result]]((session: Session) =>
   1.100 +        Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
   1.101 +          Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
   1.102  
   1.103 -              File.write(data_file,
   1.104 -                cat_lines(
   1.105 -                  entries.map(entry =>
   1.106 -                    List(entry.date.unix_epoch.toString,
   1.107 -                      entry.timing.elapsed.minutes,
   1.108 -                      entry.timing.resources.minutes,
   1.109 -                      entry.ml_timing.elapsed.minutes,
   1.110 -                      entry.ml_timing.resources.minutes).mkString(" "))))
   1.111 +            File.write(data_file,
   1.112 +              cat_lines(
   1.113 +                session.entries.map(entry =>
   1.114 +                  List(entry.date.unix_epoch.toString,
   1.115 +                    entry.timing.elapsed.minutes,
   1.116 +                    entry.timing.resources.minutes,
   1.117 +                    entry.ml_timing.elapsed.minutes,
   1.118 +                    entry.ml_timing.resources.minutes).mkString(" "))))
   1.119  
   1.120 -              def gnuplot(plots: List[String], kind: String): Process_Result =
   1.121 -              {
   1.122 -                val name = session + "_" + kind
   1.123 -                File.write(gnuplot_file, """
   1.124 +            def gnuplot(plots: List[String], kind: String): Process_Result =
   1.125 +            {
   1.126 +              val name = session.name + "_" + kind
   1.127 +              File.write(gnuplot_file, """
   1.128  set terminal png size """ + image_size._1 + "," + image_size._2 + """
   1.129  set output """ + quote(File.standard_path(dir + Path.basic(name + ".png"))) + """
   1.130  set xdata time
   1.131  set timefmt "%s"
   1.132  set format x "%d-%b"
   1.133 -set xlabel """ + quote(session) + """ noenhanced
   1.134 +set xlabel """ + quote(session.name) + """ noenhanced
   1.135  set key left top
   1.136  plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   1.137  
   1.138 -                val result =
   1.139 -                  Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   1.140 -                if (result.ok) result
   1.141 -                else result.error("Gnuplot failed for " + data_name + "/" + name)
   1.142 -              }
   1.143 +              val result =
   1.144 +                Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   1.145 +              if (result.ok) result
   1.146 +              else result.error("Gnuplot failed for " + data_name + "/" + name)
   1.147 +            }
   1.148  
   1.149 -              val timing_plots =
   1.150 -                List(
   1.151 -                  """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   1.152 -                  """ using 1:3 smooth csplines title "cpu time" """,
   1.153 -                  """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   1.154 -                  """ using 1:2 smooth csplines title "elapsed time" """)
   1.155 -              val ml_timing_plots =
   1.156 -                List(
   1.157 -                  """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   1.158 -                  """ using 1:5 smooth csplines title "ML cpu time" """,
   1.159 -                  """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   1.160 -                  """ using 1:4 smooth csplines title "ML elapsed time" """)
   1.161 +            val timing_plots =
   1.162 +              List(
   1.163 +                """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   1.164 +                """ using 1:3 smooth csplines title "cpu time" """,
   1.165 +                """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   1.166 +                """ using 1:2 smooth csplines title "elapsed time" """)
   1.167 +            val ml_timing_plots =
   1.168 +              List(
   1.169 +                """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   1.170 +                """ using 1:5 smooth csplines title "ML cpu time" """,
   1.171 +                """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   1.172 +                """ using 1:4 smooth csplines title "ML elapsed time" """)
   1.173  
   1.174 -              List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
   1.175 -            }
   1.176 +            List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
   1.177            }
   1.178 -        }, session_entries).flatten.foreach(_.check)
   1.179 -
   1.180 -      val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
   1.181 +        }, sessions).flatten.foreach(_.check)
   1.182  
   1.183        File.write(dir + Path.basic("index.html"),
   1.184          HTML.output_document(
   1.185            List(HTML.title("Isabelle build status for " + data_name)),
   1.186            HTML.chapter("Isabelle build status for " + data_name + " (" + data.date + ")") ::
   1.187            HTML.itemize(
   1.188 -            sessions.map({ case (name, entries) =>
   1.189 -              HTML.link("#session_" + name, HTML.text(name)) ::
   1.190 -              HTML.text(" (" + entries.head.timing.message_resources + ")") })) ::
   1.191 -          sessions.flatMap({ case (name, entries) =>
   1.192 +            sessions.map(session =>
   1.193 +              HTML.link("#session_" + session.name, HTML.text(session.name)) ::
   1.194 +              HTML.text(" (" + session.timing.message_resources + ")"))) ::
   1.195 +          sessions.flatMap(session =>
   1.196              List(
   1.197 -              HTML.section(name) + HTML.id("session_" + name),
   1.198 +              HTML.section(session.name) + HTML.id("session_" + session.name),
   1.199                HTML.par(
   1.200                  List(
   1.201                    HTML.itemize(List(
   1.202 -                    HTML.bold(HTML.text("timing: ")) ::
   1.203 -                      HTML.text(entries.head.timing.message_resources),
   1.204 +                    HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
   1.205                      HTML.bold(HTML.text("ML timing: ")) ::
   1.206 -                      HTML.text(entries.head.ml_timing.message_resources))),
   1.207 -                  HTML.image(name + "_timing.png"),
   1.208 -                  HTML.image(name + "_ml_timing.png")))) })))
   1.209 +                      HTML.text(session.ml_timing.message_resources))),
   1.210 +                  HTML.image(session.name + "_timing.png"),
   1.211 +                  HTML.image(session.name + "_ml_timing.png")))))))
   1.212      }
   1.213  
   1.214      File.write(target_dir + Path.basic("index.html"),
   1.215        HTML.output_document(
   1.216          List(HTML.title("Isabelle build status")),
   1.217          List(HTML.chapter("Isabelle build status (" + data.date + ")"),
   1.218 -          HTML.itemize(data_entries.map({ case (name, _) =>
   1.219 +          HTML.itemize(data.entries.map({ case (name, _) =>
   1.220              List(HTML.link(name + "/index.html", HTML.text(name))) })))))
   1.221    }
   1.222