clarified description vs. file name;
--- a/src/Pure/Admin/build_status.scala Sun May 07 22:10:48 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sun May 07 23:18:23 2017 +0200
@@ -16,7 +16,10 @@
/* data profiles */
- sealed case class Profile(name: String, sql: String)
+ def clean_name(name: String): String =
+ name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
+
+ sealed case class Profile(description: String, sql: String)
{
def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
{
@@ -65,8 +68,8 @@
val store = Build_Log.store(options)
using(store.open_database())(db =>
{
- for (profile <- profiles.sortBy(_.name)) {
- progress.echo("input " + quote(profile.name))
+ for (profile <- profiles.sortBy(_.description)) {
+ progress.echo("input " + quote(profile.description))
val columns =
List(
Build_Log.Data.pull_date,
@@ -92,17 +95,21 @@
while (res.next()) {
val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
- val threads_option =
- res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
- case Threads_Option(Value.Int(i)) => i
- case _ => 1
- }
- val threads = res.get_int(Build_Log.Data.threads).getOrElse(1)
+ val threads =
+ {
+ val threads1 =
+ res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
+ case Threads_Option(Value.Int(i)) => i
+ case _ => 1
+ }
+ val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
+ threads1 max threads2
+ }
val data_name =
- profile.name +
- "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
- "_M" + (threads_option max threads)
+ profile.description +
+ (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") +
+ (if (threads == 1) "" else ", " + threads + " threads")
val name = res.string(Build_Log.Data.session_name)
val entry =
@@ -140,66 +147,72 @@
image_size: (Int, Int) = default_image_size)
{
for ((data_name, sessions) <- data.entries) {
- val dir = target_dir + Path.explode(data_name)
+ val dir = target_dir + Path.basic(clean_name(data_name))
+
progress.echo("output " + dir)
Isabelle_System.mkdirs(dir)
- Par_List.map[Session, List[Process_Result]]((session: Session) =>
- Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
- Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
+ val session_plots =
+ Par_List.map((session: Session) =>
+ Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
+ Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
- File.write(data_file,
- cat_lines(
- session.entries.map(entry =>
- List(entry.date.unix_epoch.toString,
- entry.timing.elapsed.minutes,
- entry.timing.resources.minutes,
- entry.ml_timing.elapsed.minutes,
- entry.ml_timing.resources.minutes).mkString(" "))))
+ File.write(data_file,
+ cat_lines(
+ session.entries.map(entry =>
+ List(entry.date.unix_epoch.toString,
+ entry.timing.elapsed.minutes,
+ entry.timing.resources.minutes,
+ entry.ml_timing.elapsed.minutes,
+ entry.ml_timing.resources.minutes).mkString(" "))))
- val max_time =
- ((0.0 /: session.entries){ case (m, entry) =>
- m.max(entry.timing.elapsed.minutes).
- max(entry.timing.resources.minutes).
- max(entry.ml_timing.elapsed.minutes).
- max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
+ val max_time =
+ ((0.0 /: session.entries){ case (m, entry) =>
+ m.max(entry.timing.elapsed.minutes).
+ max(entry.timing.resources.minutes).
+ max(entry.ml_timing.elapsed.minutes).
+ max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
- def gnuplot(plots: List[String], kind: String): Process_Result =
- {
- val name = session.name + "_" + kind
- File.write(gnuplot_file, """
+ def gnuplot(plots: List[String], kind: String): String =
+ {
+ val plot_name = session.name + "_" + kind + ".png"
+
+ File.write(gnuplot_file, """
set terminal png size """ + image_size._1 + "," + image_size._2 + """
-set output """ + quote(File.standard_path(dir + Path.basic(name + ".png"))) + """
+set output """ + quote(File.standard_path(dir + Path.basic(plot_name))) + """
set xdata time
set timefmt "%s"
set format x "%d-%b"
set xlabel """ + quote(session.name) + """ noenhanced
set key left bottom
plot [] [0:""" + max_time + "] " +
- plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
+ plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
- val result =
- Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
- if (result.ok) result
- else result.error("Gnuplot failed for " + data_name + "/" + name)
- }
+ val result =
+ Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
+ if (!result.ok)
+ result.error("Gnuplot failed for " + data_name + "/" + plot_name).check
+
+ plot_name
+ }
- val timing_plots =
- List(
- """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
- """ using 1:3 smooth csplines title "cpu time" """,
- """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
- """ using 1:2 smooth csplines title "elapsed time" """)
- val ml_timing_plots =
- List(
- """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
- """ using 1:5 smooth csplines title "ML cpu time" """,
- """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
- """ using 1:4 smooth csplines title "ML elapsed time" """)
+ val timing_plots =
+ List(
+ """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
+ """ using 1:3 smooth csplines title "cpu time" """,
+ """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
+ """ using 1:2 smooth csplines title "elapsed time" """)
+ val ml_timing_plots =
+ List(
+ """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
+ """ using 1:5 smooth csplines title "ML cpu time" """,
+ """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
+ """ using 1:4 smooth csplines title "ML elapsed time" """)
- List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
- }
- }, sessions).flatten.foreach(_.check)
+ session.name ->
+ List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
+ }
+ }, sessions).toMap
File.write(dir + Path.basic("index.html"),
HTML.output_document(
@@ -213,21 +226,19 @@
List(
HTML.section(session.name) + HTML.id("session_" + session.name),
HTML.par(
- List(
- HTML.itemize(List(
- HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
- HTML.bold(HTML.text("ML timing: ")) ::
- HTML.text(session.ml_timing.message_resources))),
- HTML.image(session.name + "_timing.png"),
- HTML.image(session.name + "_ml_timing.png")))))))
+ HTML.itemize(List(
+ HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
+ HTML.bold(HTML.text("ML timing: ")) ::
+ HTML.text(session.ml_timing.message_resources))) ::
+ session_plots.getOrElse(session.name, Nil).map(HTML.image(_)))))))
}
File.write(target_dir + Path.basic("index.html"),
HTML.output_document(
List(HTML.title("Isabelle build status")),
List(HTML.chapter("Isabelle build status (" + data.date + ")"),
- HTML.itemize(data.entries.map({ case (name, _) =>
- List(HTML.link(name + "/index.html", HTML.text(name))) })))))
+ HTML.itemize(data.entries.map({ case (data_name, _) =>
+ List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Sun May 07 22:10:48 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun May 07 23:18:23 2017 +0200
@@ -88,7 +88,7 @@
/* remote build_history */
sealed case class Remote_Build(
- name: String,
+ description: String,
host: String,
user: String = "",
port: Int = 0,
@@ -103,37 +103,37 @@
Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
Build_Log.Prop.build_host + " = " + SQL.string(host) +
(if (detect == "") "" else " AND " + SQL.enclose(detect))
- Build_Status.Profile(name, sql)
+ Build_Status.Profile(description, sql)
}
}
private val remote_builds: List[List[Remote_Build]] =
{
List(
- List(Remote_Build("polyml-test", "lxbroy8",
+ List(Remote_Build("Poly/ML test", "lxbroy8",
options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
args = "-N -g timing",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test"))),
- List(Remote_Build("linux1", "lxbroy9",
+ List(Remote_Build("Linux A", "lxbroy9",
options = "-m32 -B -M1x2,2", args = "-N -g timing")),
- List(Remote_Build("linux2", "lxbroy10",
+ List(Remote_Build("Linux B", "lxbroy10",
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
List(
- Remote_Build("macos1", "macbroy2", options = "-m32 -M8", args = "-a",
+ Remote_Build("Mac OS X Mavericks", "macbroy2", options = "-m32 -M8", args = "-a",
detect = Build_Log.Prop.build_tags + " IS NULL"),
- Remote_Build("macos1_quick_and_dirty", "macbroy2",
+ Remote_Build("Mac OS X Mavericks, quick_and_dirty", "macbroy2",
options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")),
- Remote_Build("macos1_skip_proofs", "macbroy2",
+ Remote_Build("Mac OS X Mavericks, skip_proofs", "macbroy2",
options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"))),
- List(Remote_Build("macos2", "macbroy30", options = "-m32 -M2", args = "-a")),
- List(Remote_Build("macos3", "macbroy31", options = "-m32 -M2", args = "-a")),
+ List(Remote_Build("Mac OS X Yosemite", "macbroy30", options = "-m32 -M2", args = "-a")),
+ List(Remote_Build("Mac OS X Sierra", "macbroy31", options = "-m32 -M2", args = "-a")),
List(
- Remote_Build("windows", "vmnipkow9", shared_home = false,
+ Remote_Build("Windows", "vmnipkow9", shared_home = false,
options = "-m32 -M4", args = "-a",
detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
- Remote_Build("windows", "vmnipkow9", shared_home = false,
+ Remote_Build("Windows", "vmnipkow9", shared_home = false,
options = "-m64 -M4", args = "-a",
detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
}
--- a/src/Pure/Admin/jenkins.scala Sun May 07 22:10:48 2017 +0200
+++ b/src/Pure/Admin/jenkins.scala Sun May 07 23:18:23 2017 +0200
@@ -54,7 +54,7 @@
val build_status_profiles: List[Build_Status.Profile] =
build_log_jobs.map(job_name =>
- Build_Status.Profile("jenkins_" + job_name,
+ Build_Status.Profile("Jenkins " + job_name,
Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))