clarified description vs. file name;
authorwenzelm
Sun May 07 23:18:23 2017 +0200 (2017-05-07)
changeset 657641af6d544c2a3
parent 65763 dbadcc3fbe33
child 65765 c67bb109cd7b
clarified description vs. file name;
src/Pure/Admin/build_status.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/jenkins.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 22:10:48 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 23:18:23 2017 +0200
     1.3 @@ -16,7 +16,10 @@
     1.4  
     1.5    /* data profiles */
     1.6  
     1.7 -  sealed case class Profile(name: String, sql: String)
     1.8 +  def clean_name(name: String): String =
     1.9 +    name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.10 +
    1.11 +  sealed case class Profile(description: String, sql: String)
    1.12    {
    1.13      def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
    1.14      {
    1.15 @@ -65,8 +68,8 @@
    1.16      val store = Build_Log.store(options)
    1.17      using(store.open_database())(db =>
    1.18      {
    1.19 -      for (profile <- profiles.sortBy(_.name)) {
    1.20 -        progress.echo("input " + quote(profile.name))
    1.21 +      for (profile <- profiles.sortBy(_.description)) {
    1.22 +        progress.echo("input " + quote(profile.description))
    1.23          val columns =
    1.24            List(
    1.25              Build_Log.Data.pull_date,
    1.26 @@ -92,17 +95,21 @@
    1.27            while (res.next()) {
    1.28              val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
    1.29  
    1.30 -            val threads_option =
    1.31 -              res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
    1.32 -                case Threads_Option(Value.Int(i)) => i
    1.33 -                case _ => 1
    1.34 -              }
    1.35 -            val threads = res.get_int(Build_Log.Data.threads).getOrElse(1)
    1.36 +            val threads =
    1.37 +            {
    1.38 +              val threads1 =
    1.39 +                res.string(Build_Log.Settings.ISABELLE_BUILD_OPTIONS) match {
    1.40 +                  case Threads_Option(Value.Int(i)) => i
    1.41 +                  case _ => 1
    1.42 +                }
    1.43 +              val threads2 = res.get_int(Build_Log.Data.threads).getOrElse(1)
    1.44 +              threads1 max threads2
    1.45 +            }
    1.46  
    1.47              val data_name =
    1.48 -              profile.name +
    1.49 -                "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
    1.50 -                "_M" + (threads_option max threads)
    1.51 +              profile.description +
    1.52 +                (if (ml_platform.startsWith("x86_64")) ", 64bit" else "") +
    1.53 +                (if (threads == 1) "" else ", " + threads + " threads")
    1.54  
    1.55              val name = res.string(Build_Log.Data.session_name)
    1.56              val entry =
    1.57 @@ -140,66 +147,72 @@
    1.58      image_size: (Int, Int) = default_image_size)
    1.59    {
    1.60      for ((data_name, sessions) <- data.entries) {
    1.61 -      val dir = target_dir + Path.explode(data_name)
    1.62 +      val dir = target_dir + Path.basic(clean_name(data_name))
    1.63 +
    1.64        progress.echo("output " + dir)
    1.65        Isabelle_System.mkdirs(dir)
    1.66  
    1.67 -      Par_List.map[Session, List[Process_Result]]((session: Session) =>
    1.68 -        Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
    1.69 -          Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
    1.70 +      val session_plots =
    1.71 +        Par_List.map((session: Session) =>
    1.72 +          Isabelle_System.with_tmp_file(session.name, "data") { data_file =>
    1.73 +            Isabelle_System.with_tmp_file(session.name, "gnuplot") { gnuplot_file =>
    1.74  
    1.75 -            File.write(data_file,
    1.76 -              cat_lines(
    1.77 -                session.entries.map(entry =>
    1.78 -                  List(entry.date.unix_epoch.toString,
    1.79 -                    entry.timing.elapsed.minutes,
    1.80 -                    entry.timing.resources.minutes,
    1.81 -                    entry.ml_timing.elapsed.minutes,
    1.82 -                    entry.ml_timing.resources.minutes).mkString(" "))))
    1.83 +              File.write(data_file,
    1.84 +                cat_lines(
    1.85 +                  session.entries.map(entry =>
    1.86 +                    List(entry.date.unix_epoch.toString,
    1.87 +                      entry.timing.elapsed.minutes,
    1.88 +                      entry.timing.resources.minutes,
    1.89 +                      entry.ml_timing.elapsed.minutes,
    1.90 +                      entry.ml_timing.resources.minutes).mkString(" "))))
    1.91  
    1.92 -            val max_time =
    1.93 -              ((0.0 /: session.entries){ case (m, entry) =>
    1.94 -                m.max(entry.timing.elapsed.minutes).
    1.95 -                  max(entry.timing.resources.minutes).
    1.96 -                  max(entry.ml_timing.elapsed.minutes).
    1.97 -                  max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
    1.98 +              val max_time =
    1.99 +                ((0.0 /: session.entries){ case (m, entry) =>
   1.100 +                  m.max(entry.timing.elapsed.minutes).
   1.101 +                    max(entry.timing.resources.minutes).
   1.102 +                    max(entry.ml_timing.elapsed.minutes).
   1.103 +                    max(entry.ml_timing.resources.minutes) } max 0.1) * 1.1
   1.104  
   1.105 -            def gnuplot(plots: List[String], kind: String): Process_Result =
   1.106 -            {
   1.107 -              val name = session.name + "_" + kind
   1.108 -              File.write(gnuplot_file, """
   1.109 +              def gnuplot(plots: List[String], kind: String): String =
   1.110 +              {
   1.111 +                val plot_name = session.name + "_" + kind + ".png"
   1.112 +
   1.113 +                File.write(gnuplot_file, """
   1.114  set terminal png size """ + image_size._1 + "," + image_size._2 + """
   1.115 -set output """ + quote(File.standard_path(dir + Path.basic(name + ".png"))) + """
   1.116 +set output """ + quote(File.standard_path(dir + Path.basic(plot_name))) + """
   1.117  set xdata time
   1.118  set timefmt "%s"
   1.119  set format x "%d-%b"
   1.120  set xlabel """ + quote(session.name) + """ noenhanced
   1.121  set key left bottom
   1.122  plot [] [0:""" + max_time + "] " +
   1.123 -                plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   1.124 +                  plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
   1.125  
   1.126 -              val result =
   1.127 -                Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   1.128 -              if (result.ok) result
   1.129 -              else result.error("Gnuplot failed for " + data_name + "/" + name)
   1.130 -            }
   1.131 +                val result =
   1.132 +                  Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   1.133 +                if (!result.ok)
   1.134 +                  result.error("Gnuplot failed for " + data_name + "/" + plot_name).check
   1.135 +
   1.136 +                plot_name
   1.137 +              }
   1.138  
   1.139 -            val timing_plots =
   1.140 -              List(
   1.141 -                """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   1.142 -                """ using 1:3 smooth csplines title "cpu time" """,
   1.143 -                """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   1.144 -                """ using 1:2 smooth csplines title "elapsed time" """)
   1.145 -            val ml_timing_plots =
   1.146 -              List(
   1.147 -                """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   1.148 -                """ using 1:5 smooth csplines title "ML cpu time" """,
   1.149 -                """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   1.150 -                """ using 1:4 smooth csplines title "ML elapsed time" """)
   1.151 +              val timing_plots =
   1.152 +                List(
   1.153 +                  """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
   1.154 +                  """ using 1:3 smooth csplines title "cpu time" """,
   1.155 +                  """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
   1.156 +                  """ using 1:2 smooth csplines title "elapsed time" """)
   1.157 +              val ml_timing_plots =
   1.158 +                List(
   1.159 +                  """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
   1.160 +                  """ using 1:5 smooth csplines title "ML cpu time" """,
   1.161 +                  """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
   1.162 +                  """ using 1:4 smooth csplines title "ML elapsed time" """)
   1.163  
   1.164 -            List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
   1.165 -          }
   1.166 -        }, sessions).flatten.foreach(_.check)
   1.167 +              session.name ->
   1.168 +                List(gnuplot(timing_plots, "timing"), gnuplot(ml_timing_plots, "ml_timing"))
   1.169 +            }
   1.170 +          }, sessions).toMap
   1.171  
   1.172        File.write(dir + Path.basic("index.html"),
   1.173          HTML.output_document(
   1.174 @@ -213,21 +226,19 @@
   1.175              List(
   1.176                HTML.section(session.name) + HTML.id("session_" + session.name),
   1.177                HTML.par(
   1.178 -                List(
   1.179 -                  HTML.itemize(List(
   1.180 -                    HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
   1.181 -                    HTML.bold(HTML.text("ML timing: ")) ::
   1.182 -                      HTML.text(session.ml_timing.message_resources))),
   1.183 -                  HTML.image(session.name + "_timing.png"),
   1.184 -                  HTML.image(session.name + "_ml_timing.png")))))))
   1.185 +                HTML.itemize(List(
   1.186 +                  HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
   1.187 +                  HTML.bold(HTML.text("ML timing: ")) ::
   1.188 +                    HTML.text(session.ml_timing.message_resources))) ::
   1.189 +                session_plots.getOrElse(session.name, Nil).map(HTML.image(_)))))))
   1.190      }
   1.191  
   1.192      File.write(target_dir + Path.basic("index.html"),
   1.193        HTML.output_document(
   1.194          List(HTML.title("Isabelle build status")),
   1.195          List(HTML.chapter("Isabelle build status (" + data.date + ")"),
   1.196 -          HTML.itemize(data.entries.map({ case (name, _) =>
   1.197 -            List(HTML.link(name + "/index.html", HTML.text(name))) })))))
   1.198 +          HTML.itemize(data.entries.map({ case (data_name, _) =>
   1.199 +            List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
   1.200    }
   1.201  
   1.202  
     2.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Sun May 07 22:10:48 2017 +0200
     2.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sun May 07 23:18:23 2017 +0200
     2.3 @@ -88,7 +88,7 @@
     2.4    /* remote build_history */
     2.5  
     2.6    sealed case class Remote_Build(
     2.7 -    name: String,
     2.8 +    description: String,
     2.9      host: String,
    2.10      user: String = "",
    2.11      port: Int = 0,
    2.12 @@ -103,37 +103,37 @@
    2.13          Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
    2.14          Build_Log.Prop.build_host + " = " + SQL.string(host) +
    2.15          (if (detect == "") "" else " AND " + SQL.enclose(detect))
    2.16 -      Build_Status.Profile(name, sql)
    2.17 +      Build_Status.Profile(description, sql)
    2.18      }
    2.19    }
    2.20  
    2.21    private val remote_builds: List[List[Remote_Build]] =
    2.22    {
    2.23      List(
    2.24 -      List(Remote_Build("polyml-test", "lxbroy8",
    2.25 +      List(Remote_Build("Poly/ML test", "lxbroy8",
    2.26          options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
    2.27          args = "-N -g timing",
    2.28          detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test"))),
    2.29 -      List(Remote_Build("linux1", "lxbroy9",
    2.30 +      List(Remote_Build("Linux A", "lxbroy9",
    2.31          options = "-m32 -B -M1x2,2", args = "-N -g timing")),
    2.32 -      List(Remote_Build("linux2", "lxbroy10",
    2.33 +      List(Remote_Build("Linux B", "lxbroy10",
    2.34          options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
    2.35        List(
    2.36 -        Remote_Build("macos1", "macbroy2", options = "-m32 -M8", args = "-a",
    2.37 +        Remote_Build("Mac OS X Mavericks", "macbroy2", options = "-m32 -M8", args = "-a",
    2.38            detect = Build_Log.Prop.build_tags + " IS NULL"),
    2.39 -        Remote_Build("macos1_quick_and_dirty", "macbroy2",
    2.40 +        Remote_Build("Mac OS X Mavericks, quick_and_dirty", "macbroy2",
    2.41            options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
    2.42            detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")),
    2.43 -        Remote_Build("macos1_skip_proofs", "macbroy2",
    2.44 +        Remote_Build("Mac OS X Mavericks, skip_proofs", "macbroy2",
    2.45            options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
    2.46            detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"))),
    2.47 -      List(Remote_Build("macos2", "macbroy30", options = "-m32 -M2", args = "-a")),
    2.48 -      List(Remote_Build("macos3", "macbroy31", options = "-m32 -M2", args = "-a")),
    2.49 +      List(Remote_Build("Mac OS X Yosemite", "macbroy30", options = "-m32 -M2", args = "-a")),
    2.50 +      List(Remote_Build("Mac OS X Sierra", "macbroy31", options = "-m32 -M2", args = "-a")),
    2.51        List(
    2.52 -        Remote_Build("windows", "vmnipkow9", shared_home = false,
    2.53 +        Remote_Build("Windows", "vmnipkow9", shared_home = false,
    2.54            options = "-m32 -M4", args = "-a",
    2.55            detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
    2.56 -        Remote_Build("windows", "vmnipkow9", shared_home = false,
    2.57 +        Remote_Build("Windows", "vmnipkow9", shared_home = false,
    2.58            options = "-m64 -M4", args = "-a",
    2.59            detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
    2.60    }
     3.1 --- a/src/Pure/Admin/jenkins.scala	Sun May 07 22:10:48 2017 +0200
     3.2 +++ b/src/Pure/Admin/jenkins.scala	Sun May 07 23:18:23 2017 +0200
     3.3 @@ -54,7 +54,7 @@
     3.4  
     3.5    val build_status_profiles: List[Build_Status.Profile] =
     3.6      build_log_jobs.map(job_name =>
     3.7 -      Build_Status.Profile("jenkins_" + job_name,
     3.8 +      Build_Status.Profile("Jenkins " + job_name,
     3.9          Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
    3.10          Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
    3.11