# HG changeset patch # User wenzelm # Date 1494191903 -7200 # Node ID 1af6d544c2a38971b01cd7bea23455d0ac714083 # Parent dbadcc3fbe33ccc62d6ae2a6ceafe9d358d0527d clarified description vs. file name; diff -r dbadcc3fbe33 -r 1af6d544c2a3 src/Pure/Admin/build_status.scala --- 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))) }))))) } diff -r dbadcc3fbe33 -r 1af6d544c2a3 src/Pure/Admin/isabelle_cronjob.scala --- 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")))) } diff -r dbadcc3fbe33 -r 1af6d544c2a3 src/Pure/Admin/jenkins.scala --- 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)))