src/Pure/Admin/build_status.scala
changeset 65759 a2b041a36523
parent 65758 d79126bb5d07
child 65760 a51290fd62d9
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 17:10:03 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 17:29:38 2017 +0200
     1.3 @@ -142,8 +142,7 @@
     1.4    def present_data(data: Data,
     1.5      progress: Progress = No_Progress,
     1.6      target_dir: Path = default_target_dir,
     1.7 -    image_size: (Int, Int) = default_image_size,
     1.8 -    ml_timing: Option[Boolean] = None)
     1.9 +    image_size: (Int, Int) = default_image_size)
    1.10    {
    1.11      val data_entries = data.sorted_entries
    1.12  
    1.13 @@ -152,7 +151,7 @@
    1.14        progress.echo("output " + dir)
    1.15        Isabelle_System.mkdirs(dir)
    1.16  
    1.17 -      Par_List.map[(String, List[isabelle.Build_Status.Entry]), Process_Result](
    1.18 +      Par_List.map[(String, List[isabelle.Build_Status.Entry]), List[Process_Result]](
    1.19          { case (session, entries) =>
    1.20            Isabelle_System.with_tmp_file(session, "data") { data_file =>
    1.21              Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
    1.22 @@ -167,13 +166,32 @@
    1.23                        entry.ml_timing.cpu.minutes,
    1.24                        entry.ml_timing.gc.minutes).mkString(" "))))
    1.25  
    1.26 -              val plots1 =
    1.27 +              def gnuplot(plots: List[String], kind: String): Process_Result =
    1.28 +              {
    1.29 +                val name = session + "_" + kind
    1.30 +                File.write(gnuplot_file, """
    1.31 +set terminal png size """ + image_size._1 + "," + image_size._2 + """
    1.32 +set output """ + quote(File.standard_path(dir + Path.basic(name + ".png"))) + """
    1.33 +set xdata time
    1.34 +set timefmt "%s"
    1.35 +set format x "%d-%b"
    1.36 +set xlabel """ + quote(session) + """ noenhanced
    1.37 +set key left top
    1.38 +plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
    1.39 +
    1.40 +                val result =
    1.41 +                  Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
    1.42 +                if (result.ok) result
    1.43 +                else result.error("Gnuplot failed for " + data_name + "/" + name)
    1.44 +              }
    1.45 +
    1.46 +              val timing_plots =
    1.47                  List(
    1.48                    """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
    1.49                    """ using 1:3 smooth csplines title "cpu time" """,
    1.50                    """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    1.51                    """ using 1:2 smooth csplines title "elapsed time" """)
    1.52 -              val plots2 =
    1.53 +              val ml_timing_plots =
    1.54                  List(
    1.55                    """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
    1.56                    """ using 1:5 smooth csplines title "ML cpu time" """,
    1.57 @@ -181,30 +199,11 @@
    1.58                    """ using 1:4 smooth csplines title "ML elapsed time" """,
    1.59                    """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
    1.60                    """ using 1:6 smooth csplines title "ML gc time" """)
    1.61 -              val plots =
    1.62 -                ml_timing match {
    1.63 -                  case None => plots1
    1.64 -                  case Some(false) => plots1 ::: plots2
    1.65 -                  case Some(true) => plots2
    1.66 -                }
    1.67  
    1.68 -              File.write(gnuplot_file, """
    1.69 -set terminal png size """ + image_size._1 + "," + image_size._2 + """
    1.70 -set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
    1.71 -set xdata time
    1.72 -set timefmt "%s"
    1.73 -set format x "%d-%b"
    1.74 -set xlabel """ + quote(session) + """ noenhanced
    1.75 -set key left top
    1.76 -plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
    1.77 -
    1.78 -              val result =
    1.79 -                Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
    1.80 -              if (result.ok) result
    1.81 -              else result.error("Gnuplot failed for " + data_name + "/" + session)
    1.82 +              List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
    1.83              }
    1.84            }
    1.85 -        }, session_entries).foreach(_.check)
    1.86 +        }, session_entries).flatten.foreach(_.check)
    1.87  
    1.88        val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
    1.89        val heading = "Build status for " + data_name + " (" + data.date + ")"
    1.90 @@ -227,7 +226,8 @@
    1.91                        HTML.text(entries.head.timing.message_resources),
    1.92                      HTML.bold(HTML.text("ML timing: ")) ::
    1.93                        HTML.text(entries.head.ml_timing.message_resources))),
    1.94 -                  HTML.image(name + ".png")))) })))
    1.95 +                  HTML.image(name + "_timing.png"),
    1.96 +                  HTML.image(name + "_ml_timing.png")))) })))
    1.97      }
    1.98  
    1.99      val heading = "Build status (" + data.date + ")"
   1.100 @@ -247,7 +247,6 @@
   1.101      Isabelle_Tool("build_status", "present recent build status information from database", args =>
   1.102      {
   1.103        var target_dir = default_target_dir
   1.104 -      var ml_timing: Option[Boolean] = None
   1.105        var only_sessions = Set.empty[String]
   1.106        var history_length = default_history_length
   1.107        var options = Options.init()
   1.108 @@ -259,10 +258,8 @@
   1.109  
   1.110    Options are:
   1.111      -D DIR       target directory (default """ + default_target_dir + """)
   1.112 -    -M           only ML timing
   1.113      -S SESSIONS  only given SESSIONS (comma separated)
   1.114      -l LENGTH    length of history (default """ + default_history_length + """)
   1.115 -    -m           include ML timing
   1.116      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   1.117      -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
   1.118      -v           verbose
   1.119 @@ -271,10 +268,8 @@
   1.120    via system options build_log_database_host, build_log_database_user etc.
   1.121  """,
   1.122          "D:" -> (arg => target_dir = Path.explode(arg)),
   1.123 -        "M" -> (_ => ml_timing = Some(true)),
   1.124          "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
   1.125          "l:" -> (arg => history_length = Value.Int.parse(arg)),
   1.126 -        "m" -> (_ => ml_timing = Some(false)),
   1.127          "o:" -> (arg => options = options + arg),
   1.128          "s:" -> (arg =>
   1.129            space_explode('x', arg).map(Value.Int.parse(_)) match {
   1.130 @@ -292,8 +287,7 @@
   1.131          read_data(options, progress = progress, history_length = history_length,
   1.132            only_sessions = only_sessions, verbose = verbose)
   1.133  
   1.134 -      present_data(data, progress = progress, target_dir = target_dir,
   1.135 -        image_size = image_size, ml_timing = ml_timing)
   1.136 +      present_data(data, progress = progress, target_dir = target_dir, image_size = image_size)
   1.137  
   1.138    }, admin = true)
   1.139  }