src/Pure/Admin/build_status.scala
changeset 65756 2c6b5dd59db3
parent 65755 21b4bfa6d204
child 65757 a6522bb9acfa
equal deleted inserted replaced
65755:21b4bfa6d204 65756:2c6b5dd59db3
   157     for ((data_name, session_entries) <- data_entries) {
   157     for ((data_name, session_entries) <- data_entries) {
   158       val dir = target_dir + Path.explode(data_name)
   158       val dir = target_dir + Path.explode(data_name)
   159       progress.echo("output " + dir)
   159       progress.echo("output " + dir)
   160       Isabelle_System.mkdirs(dir)
   160       Isabelle_System.mkdirs(dir)
   161 
   161 
   162       for ((session, entries) <- session_entries) {
   162       Par_List.map[(String, List[isabelle.Build_Status.Entry]), Process_Result](
   163         Isabelle_System.with_tmp_file(session, "data") { data_file =>
   163         { case (session, entries) =>
   164           Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
   164           Isabelle_System.with_tmp_file(session, "data") { data_file =>
   165 
   165             Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
   166             File.write(data_file,
   166 
   167               cat_lines(
   167               File.write(data_file,
   168                 entries.map(entry =>
   168                 cat_lines(
   169                   List(entry.date.unix_epoch.toString,
   169                   entries.map(entry =>
   170                     entry.timing.elapsed.minutes,
   170                     List(entry.date.unix_epoch.toString,
   171                     entry.timing.cpu.minutes,
   171                       entry.timing.elapsed.minutes,
   172                     entry.ml_timing.elapsed.minutes,
   172                       entry.timing.cpu.minutes,
   173                     entry.ml_timing.cpu.minutes,
   173                       entry.ml_timing.elapsed.minutes,
   174                     entry.ml_timing.gc.minutes).mkString(" "))))
   174                       entry.ml_timing.cpu.minutes,
   175 
   175                       entry.ml_timing.gc.minutes).mkString(" "))))
   176             val plots1 =
   176 
   177               List(
   177               val plots1 =
   178                 """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   178                 List(
   179                 """ using 1:3 smooth csplines title "cpu time" """,
   179                   """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   180                 """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   180                   """ using 1:3 smooth csplines title "cpu time" """,
   181                 """ using 1:2 smooth csplines title "elapsed time" """)
   181                   """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   182             val plots2 =
   182                   """ using 1:2 smooth csplines title "elapsed time" """)
   183               List(
   183               val plots2 =
   184                 """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   184                 List(
   185                 """ using 1:5 smooth csplines title "ML cpu time" """,
   185                   """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   186                 """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   186                   """ using 1:5 smooth csplines title "ML cpu time" """,
   187                 """ using 1:4 smooth csplines title "ML elapsed time" """,
   187                   """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   188                 """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
   188                   """ using 1:4 smooth csplines title "ML elapsed time" """,
   189                 """ using 1:6 smooth csplines title "ML gc time" """)
   189                   """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
   190             val plots =
   190                   """ using 1:6 smooth csplines title "ML gc time" """)
   191               ml_timing match {
   191               val plots =
   192                 case None => plots1
   192                 ml_timing match {
   193                 case Some(false) => plots1 ::: plots2
   193                   case None => plots1
   194                 case Some(true) => plots2
   194                   case Some(false) => plots1 ::: plots2
   195               }
   195                   case Some(true) => plots2
   196 
   196                 }
   197             File.write(gnuplot_file, """
   197 
       
   198               File.write(gnuplot_file, """
   198 set terminal png size """ + image_size._1 + "," + image_size._2 + """
   199 set terminal png size """ + image_size._1 + "," + image_size._2 + """
   199 set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
   200 set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
   200 set xdata time
   201 set xdata time
   201 set timefmt "%s"
   202 set timefmt "%s"
   202 set format x "%d-%b"
   203 set format x "%d-%b"
   203 set xlabel """ + quote(session) + """ noenhanced
   204 set xlabel """ + quote(session) + """ noenhanced
   204 set key left top
   205 set key left top
   205 plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   206 plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   206 
   207 
   207             val result =
   208               val result =
   208               Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   209                 Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   209             if (result.rc != 0)
   210               if (result.ok) result
   210               result.error("Gnuplot failed for " + data_name + "/" + session).check
   211               else result.error("Gnuplot failed for " + data_name + "/" + session)
       
   212             }
   211           }
   213           }
   212         }
   214         }, session_entries).foreach(_.check)
   213       }
       
   214 
   215 
   215       val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
   216       val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
   216       val heading = "Build status for " + data_name + " (" + data.date + ")"
   217       val heading = "Build status for " + data_name + " (" + data.date + ")"
   217 
   218 
   218       File.write(dir + Path.basic("index.html"),
   219       File.write(dir + Path.basic("index.html"),