parallel gnuplot invocation;
authorwenzelm
Sun May 07 16:42:36 2017 +0200 (2017-05-07)
changeset 657562c6b5dd59db3
parent 65755 21b4bfa6d204
child 65757 a6522bb9acfa
parallel gnuplot invocation;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 16:31:39 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 16:42:36 2017 +0200
     1.3 @@ -159,42 +159,43 @@
     1.4        progress.echo("output " + dir)
     1.5        Isabelle_System.mkdirs(dir)
     1.6  
     1.7 -      for ((session, entries) <- session_entries) {
     1.8 -        Isabelle_System.with_tmp_file(session, "data") { data_file =>
     1.9 -          Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
    1.10 +      Par_List.map[(String, List[isabelle.Build_Status.Entry]), Process_Result](
    1.11 +        { case (session, entries) =>
    1.12 +          Isabelle_System.with_tmp_file(session, "data") { data_file =>
    1.13 +            Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
    1.14  
    1.15 -            File.write(data_file,
    1.16 -              cat_lines(
    1.17 -                entries.map(entry =>
    1.18 -                  List(entry.date.unix_epoch.toString,
    1.19 -                    entry.timing.elapsed.minutes,
    1.20 -                    entry.timing.cpu.minutes,
    1.21 -                    entry.ml_timing.elapsed.minutes,
    1.22 -                    entry.ml_timing.cpu.minutes,
    1.23 -                    entry.ml_timing.gc.minutes).mkString(" "))))
    1.24 +              File.write(data_file,
    1.25 +                cat_lines(
    1.26 +                  entries.map(entry =>
    1.27 +                    List(entry.date.unix_epoch.toString,
    1.28 +                      entry.timing.elapsed.minutes,
    1.29 +                      entry.timing.cpu.minutes,
    1.30 +                      entry.ml_timing.elapsed.minutes,
    1.31 +                      entry.ml_timing.cpu.minutes,
    1.32 +                      entry.ml_timing.gc.minutes).mkString(" "))))
    1.33  
    1.34 -            val plots1 =
    1.35 -              List(
    1.36 -                """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
    1.37 -                """ using 1:3 smooth csplines title "cpu time" """,
    1.38 -                """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    1.39 -                """ using 1:2 smooth csplines title "elapsed time" """)
    1.40 -            val plots2 =
    1.41 -              List(
    1.42 -                """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
    1.43 -                """ using 1:5 smooth csplines title "ML cpu time" """,
    1.44 -                """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
    1.45 -                """ using 1:4 smooth csplines title "ML elapsed time" """,
    1.46 -                """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
    1.47 -                """ using 1:6 smooth csplines title "ML gc time" """)
    1.48 -            val plots =
    1.49 -              ml_timing match {
    1.50 -                case None => plots1
    1.51 -                case Some(false) => plots1 ::: plots2
    1.52 -                case Some(true) => plots2
    1.53 -              }
    1.54 +              val plots1 =
    1.55 +                List(
    1.56 +                  """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
    1.57 +                  """ using 1:3 smooth csplines title "cpu time" """,
    1.58 +                  """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
    1.59 +                  """ using 1:2 smooth csplines title "elapsed time" """)
    1.60 +              val plots2 =
    1.61 +                List(
    1.62 +                  """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
    1.63 +                  """ using 1:5 smooth csplines title "ML cpu time" """,
    1.64 +                  """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
    1.65 +                  """ using 1:4 smooth csplines title "ML elapsed time" """,
    1.66 +                  """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
    1.67 +                  """ using 1:6 smooth csplines title "ML gc time" """)
    1.68 +              val plots =
    1.69 +                ml_timing match {
    1.70 +                  case None => plots1
    1.71 +                  case Some(false) => plots1 ::: plots2
    1.72 +                  case Some(true) => plots2
    1.73 +                }
    1.74  
    1.75 -            File.write(gnuplot_file, """
    1.76 +              File.write(gnuplot_file, """
    1.77  set terminal png size """ + image_size._1 + "," + image_size._2 + """
    1.78  set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
    1.79  set xdata time
    1.80 @@ -204,13 +205,13 @@
    1.81  set key left top
    1.82  plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
    1.83  
    1.84 -            val result =
    1.85 -              Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
    1.86 -            if (result.rc != 0)
    1.87 -              result.error("Gnuplot failed for " + data_name + "/" + session).check
    1.88 +              val result =
    1.89 +                Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
    1.90 +              if (result.ok) result
    1.91 +              else result.error("Gnuplot failed for " + data_name + "/" + session)
    1.92 +            }
    1.93            }
    1.94 -        }
    1.95 -      }
    1.96 +        }, session_entries).foreach(_.check)
    1.97  
    1.98        val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
    1.99        val heading = "Build status for " + data_name + " (" + data.date + ")"