src/Pure/Admin/build_status.scala
changeset 65764 1af6d544c2a3
parent 65763 dbadcc3fbe33
child 65765 c67bb109cd7b
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 22:10:48 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 23:18:23 2017 +0200
     1.3 @@ -16,7 +16,10 @@
     1.4  
     1.5    /* data profiles */
     1.6  
     1.7 -  sealed case class Profile(name: String, sql: String)
     1.8 +  def clean_name(name: String): String =
     1.9 +    name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.10 +
    1.11 +  sealed case class Profile(description: String, sql: String)
    1.12    {
    1.13      def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
    1.14      {
    1.15 @@ -65,8 +68,8 @@
    1.16      val store = Build_Log.store(options)
    1.17      using(store.open_database())(db =>
    1.18      {
    1.19 -      for (profile <- profiles.sortBy(_.name)) {
    1.20 -        progress.echo("input " + quote(profile.name))
    1.21 +      for (profile <- profiles.sortBy(_.description)) {
    1.22 +        progress.echo("input " + quote(profile.description))
    1.23          val columns =
    1.24            List(
    1.25              Build_Log.Data.pull_date,
    1.26 @@ -92,17 +95,21 @@
    1.27            while (res.next()) {
    1.28              val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
    1.29  
    1.30 -            val threads_option =
    1.31 -              res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
    1.32 -                case Threads_Option(Value.Int(i)) => i
    1.33 -                case _ => 1
    1.34 -              }
    1.35 -            val threads = res.get_int(Build_Log.Data.threads).getOrElse(1)
    1.36 +            val threads =
    1.37 +            {
    1.38 +              val threads1 =
    1.39 +                res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
    1.40 +                  case Threads_Option(Value.Int(i)) => i
    1.41 +                  case _ => 1
    1.42 +                }
    1.43 +              val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
    1.44 +              threads1 max threads2
    1.45 +            }
    1.46  
    1.47              val data_name =
    1.48 -              profile.name +
    1.49 -                "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
    1.50 -                "_M" + (threads_option max threads)
    1.51 +              profile.description +
    1.52 +                (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") +
    1.53 +                (if (threads == 1) "" else ", " + threads + " threads")
    1.54  
    1.55              val name = res.string(Build_Log.Data.session_name)
    1.56              val entry =
    1.57 @@ -140,66 +147,72 @@
    1.58      image_size: (Int, Int) = default_image_size)
    1.59    {
    1.60      for ((data_name, sessions) <- data.entries) {
    1.61 -      val dir = target_dir + Path.explode(data_name)
    1.62 +      val dir = target_dir + Path.basic(clean_name(data_name))
    1.63 +
    1.64        progress.echo("output " + dir)
    1.65        Isabelle_System.mkdirs(dir)
    1.66  
    1.67 -      Par_List.map[Session, List[Process_Result]]((session: Session) =>
    1.68 -        Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
    1.69 -          Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
    1.70 +      val session_plots =
    1.71 +        Par_List.map((session: Session) =>
    1.72 +          Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
    1.73 +            Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
    1.74  
    1.75 -            File.write(data_file,
    1.76 -              cat_lines(
    1.77 -                session.entries.map(entry =>
    1.78 -                  List(entry.date.unix_epoch.toString,
    1.79 -                    entry.timing.elapsed.minutes,
    1.80 -                    entry.timing.resources.minutes,
    1.81 -                    entry.ml_timing.elapsed.minutes,
    1.82 -                    entry.ml_timing.resources.minutes).mkString(" "))))
    1.83 +              File.write(data_file,
    1.84 +                cat_lines(
    1.85 +                  session.entries.map(entry =>
    1.86 +                    List(entry.date.unix_epoch.toString,
    1.87 +                      entry.timing.elapsed.minutes,
    1.88 +                      entry.timing.resources.minutes,
    1.89 +                      entry.ml_timing.elapsed.minutes,
    1.90 +                      entry.ml_timing.resources.minutes).mkString(" "))))
    1.91  
    1.92 -            val max_time =
    1.93 -              ((0.0 /: session.entries){ case (m, entry) =>
    1.94 -                m.max(entry.timing.elapsed.minutes).
    1.95 -                  max(entry.timing.resources.minutes).
    1.96 -                  max(entry.ml_timing.elapsed.minutes).
    1.97 -                  max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
    1.98 +              val max_time =
    1.99 +                ((0.0 /: session.entries){ case (m, entry) =>
   1.100 +                  m.max(entry.timing.elapsed.minutes).
   1.101 +                    max(entry.timing.resources.minutes).
   1.102 +                    max(entry.ml_timing.elapsed.minutes).
   1.103 +                    max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
   1.104  
   1.105 -            def gnuplot(plots: List[String], kind: String): Process_Result =
   1.106 -            {
   1.107 -              val name = session.name + "_" + kind
   1.108 -              File.write(gnuplot_file, """
   1.109 +              def gnuplot(plots: List[String], kind: String): String =
   1.110 +              {
   1.111 +                val plot_name = session.name + "_" + kind + ".png"
   1.112 +
   1.113 +                File.write(gnuplot_file, """
   1.114  set terminal png size """ + image_size._1 + "," + image_size._2 + """
   1.115 -set output """ + quote(File.standard_path(dir + Path.basic(name + ".png"))) + """
   1.116 +set output """ + quote(File.standard_path(dir + Path.basic(plot_name))) + """
   1.117  set xdata time
   1.118  set timefmt "%s"
   1.119  set format x "%d-%b"
   1.120  set xlabel """ + quote(session.name) + """ noenhanced
   1.121  set key left bottom
   1.122  plot [] [0:""" + max_time + "] " +
   1.123 -                plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   1.124 +                  plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   1.125  
   1.126 -              val result =
   1.127 -                Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   1.128 -              if (result.ok) result
   1.129 -              else result.error("Gnuplot failed for " + data_name + "/" + name)
   1.130 -            }
   1.131 +                val result =
   1.132 +                  Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   1.133 +                if (!result.ok)
   1.134 +                  result.error("Gnuplot failed for " + data_name + "/" + plot_name).check
   1.135 +
   1.136 +                plot_name
   1.137 +              }
   1.138  
   1.139 -            val timing_plots =
   1.140 -              List(
   1.141 -                """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   1.142 -                """ using 1:3 smooth csplines title "cpu time" """,
   1.143 -                """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   1.144 -                """ using 1:2 smooth csplines title "elapsed time" """)
   1.145 -            val ml_timing_plots =
   1.146 -              List(
   1.147 -                """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   1.148 -                """ using 1:5 smooth csplines title "ML cpu time" """,
   1.149 -                """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   1.150 -                """ using 1:4 smooth csplines title "ML elapsed time" """)
   1.151 +              val timing_plots =
   1.152 +                List(
   1.153 +                  """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   1.154 +                  """ using 1:3 smooth csplines title "cpu time" """,
   1.155 +                  """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   1.156 +                  """ using 1:2 smooth csplines title "elapsed time" """)
   1.157 +              val ml_timing_plots =
   1.158 +                List(
   1.159 +                  """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   1.160 +                  """ using 1:5 smooth csplines title "ML cpu time" """,
   1.161 +                  """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   1.162 +                  """ using 1:4 smooth csplines title "ML elapsed time" """)
   1.163  
   1.164 -            List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
   1.165 -          }
   1.166 -        }, sessions).flatten.foreach(_.check)
   1.167 +              session.name ->
   1.168 +                List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
   1.169 +            }
   1.170 +          }, sessions).toMap
   1.171  
   1.172        File.write(dir + Path.basic("index.html"),
   1.173          HTML.output_document(
   1.174 @@ -213,21 +226,19 @@
   1.175              List(
   1.176                HTML.section(session.name) + HTML.id("session_" + session.name),
   1.177                HTML.par(
   1.178 -                List(
   1.179 -                  HTML.itemize(List(
   1.180 -                    HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
   1.181 -                    HTML.bold(HTML.text("ML timing: ")) ::
   1.182 -                      HTML.text(session.ml_timing.message_resources))),
   1.183 -                  HTML.image(session.name + "_timing.png"),
   1.184 -                  HTML.image(session.name + "_ml_timing.png")))))))
   1.185 +                HTML.itemize(List(
   1.186 +                  HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
   1.187 +                  HTML.bold(HTML.text("ML timing: ")) ::
   1.188 +                    HTML.text(session.ml_timing.message_resources))) ::
   1.189 +                session_plots.getOrElse(session.name, Nil).map(HTML.image(_)))))))
   1.190      }
   1.191  
   1.192      File.write(target_dir + Path.basic("index.html"),
   1.193        HTML.output_document(
   1.194          List(HTML.title("Isabelle build status")),
   1.195          List(HTML.chapter("Isabelle build status (" + data.date + ")"),
   1.196 -          HTML.itemize(data.entries.map({ case (name, _) =>
   1.197 -            List(HTML.link(name + "/index.html", HTML.text(name))) })))))
   1.198 +          HTML.itemize(data.entries.map({ case (data_name, _) =>
   1.199 +            List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
   1.200    }
   1.201  
   1.202