src/Pure/Admin/build_stats.scala
author wenzelm
Sat, 06 May 2017 12:59:16 +0200
changeset 65742 b9e0f25ba16a
parent 65741 cf42659364c9
permissions -rw-r--r--
tuned messages;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64106
diff changeset
     1
/*  Title:      Pure/Admin/build_stats.scala
63686
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
     3
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
     4
Performance statistics from build log database.
63686
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
     5
*/
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
     6
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
     7
package isabelle
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
     8
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
     9
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
    10
object Build_Stats
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
    11
{
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    12
  private val default_target_dir = Path.explode("stats")
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    13
  private val default_history_length = 30
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    14
  private val default_image_size = (800, 600)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    15
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    16
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    17
  /* data profiles */
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
    18
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    19
  sealed case class Profile(name: String, sql: String)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    20
  {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    21
    def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    22
    {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    23
      val sql_sessions =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    24
        if (only_sessions.isEmpty) ""
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    25
        else
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    26
          only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    27
            .mkString("(", " OR ", ") AND ")
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
    28
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    29
      Build_Log.Data.universal_table.select(columns, distinct = true,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    30
        sql = "WHERE " +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    31
          Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    32
          Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    33
          " AND " + sql_sessions + SQL.enclose(sql) +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    34
          " ORDER BY " + Build_Log.Data.pull_date + " DESC")
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    35
    }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    36
  }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    37
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    38
  val standard_profiles: List[Profile] =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    39
    Jenkins.build_log_profiles :::
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    40
    Isabelle_Cronjob.remote_builds.flatten.toList.map(r => Profile(r.name, r.sql))
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    41
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    42
  sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing)
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
    43
  {
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    44
    def check(elapsed_threshold: Time): Boolean =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    45
      !timing.is_zero && timing.elapsed >= elapsed_threshold
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    46
  }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    47
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    48
  type Data = Map[String, Map[String, List[Entry]]]
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    49
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
    50
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    51
  /* read data */
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    52
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    53
  def read_data(options: Options,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    54
    profiles: List[Profile] = standard_profiles,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    55
    progress: Progress = No_Progress,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    56
    history_length: Int = default_history_length,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    57
    only_sessions: Set[String] = Set.empty,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    58
    elapsed_threshold: Time = Time.zero): Data =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    59
  {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    60
    var data: Data = Map.empty
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
    61
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    62
    val store = Build_Log.store(options)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    63
    using(store.open_database())(db =>
64089
10d719dbb3ee more permissive timing data;
wenzelm
parents: 64085
diff changeset
    64
    {
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    65
      for (profile <- profiles) {
65742
b9e0f25ba16a tuned messages;
wenzelm
parents: 65741
diff changeset
    66
        progress.echo("input " + quote(profile.name))
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    67
        val columns =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    68
          List(
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    69
            Build_Log.Data.pull_date,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    70
            Build_Log.Settings.ML_PLATFORM,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    71
            Build_Log.Data.session_name,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    72
            Build_Log.Data.threads,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    73
            Build_Log.Data.timing_elapsed,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    74
            Build_Log.Data.timing_cpu,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    75
            Build_Log.Data.timing_gc,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    76
            Build_Log.Data.ml_timing_elapsed,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    77
            Build_Log.Data.ml_timing_cpu,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    78
            Build_Log.Data.ml_timing_gc)
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
    79
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    80
        db.using_statement(profile.select(columns, history_length, only_sessions))(stmt =>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    81
        {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65737
diff changeset
    82
          val res = stmt.execute_query()
83388f09e9ab clarified signature;
wenzelm
parents: 65737
diff changeset
    83
          while (res.next()) {
83388f09e9ab clarified signature;
wenzelm
parents: 65737
diff changeset
    84
            val ml_platform = res.string(Build_Log.Settings.ML_PLATFORM)
83388f09e9ab clarified signature;
wenzelm
parents: 65737
diff changeset
    85
            val threads = res.get_int(Build_Log.Data.threads)
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    86
            val name =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    87
              profile.name +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    88
                "_m" + (if (ml_platform.startsWith("x86_64")) "64" else "32") +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    89
                "_M" + threads.getOrElse(1)
63703
ec095a532a2b provide index.html;
wenzelm
parents: 63702
diff changeset
    90
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65737
diff changeset
    91
            val session = res.string(Build_Log.Data.session_name)
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
    92
            val entry =
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65737
diff changeset
    93
              Entry(res.date(Build_Log.Data.pull_date),
65741
wenzelm
parents: 65740
diff changeset
    94
                res.timing(
wenzelm
parents: 65740
diff changeset
    95
                  Build_Log.Data.timing_elapsed,
wenzelm
parents: 65740
diff changeset
    96
                  Build_Log.Data.timing_cpu,
wenzelm
parents: 65740
diff changeset
    97
                  Build_Log.Data.timing_gc),
wenzelm
parents: 65740
diff changeset
    98
                res.timing(
wenzelm
parents: 65740
diff changeset
    99
                  Build_Log.Data.ml_timing_elapsed,
wenzelm
parents: 65740
diff changeset
   100
                  Build_Log.Data.ml_timing_cpu,
wenzelm
parents: 65740
diff changeset
   101
                  Build_Log.Data.ml_timing_gc))
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   102
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   103
            val session_entries = data.getOrElse(name, Map.empty)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   104
            val entries = session_entries.getOrElse(session, Nil)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   105
            data += (name -> (session_entries + (session -> (entry :: entries))))
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   106
          }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   107
        })
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   108
      }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   109
    })
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   110
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   111
    for {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   112
      (name, session_entries) <- data
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   113
      session_entries1 <-
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   114
        {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   115
          val session_entries1 =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   116
            for {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   117
              (session, entries) <- session_entries
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   118
              if entries.filter(_.check(elapsed_threshold)).length >= 3
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   119
            } yield (session, entries)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   120
          if (session_entries1.isEmpty) None
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   121
          else Some(session_entries1)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   122
        }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   123
    } yield (name, session_entries1)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   124
  }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   125
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   126
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   127
  /* present data */
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   128
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   129
  private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   130
<html>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   131
<head><title>Performance statistics from build log database</title></head>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   132
<body>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   133
"""
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   134
  private val html_footer = """
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   135
</body>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   136
</html>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   137
"""
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   138
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   139
  def present_data(data: Data,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   140
    progress: Progress = No_Progress,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   141
    target_dir: Path = default_target_dir,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   142
    image_size: (Int, Int) = default_image_size,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   143
    ml_timing: Option[Boolean] = None)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   144
  {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   145
    val data_entries = data.toList.sortBy(_._1)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   146
    for ((name, session_entries) <- data_entries) {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   147
      val dir = target_dir + Path.explode(name)
65742
b9e0f25ba16a tuned messages;
wenzelm
parents: 65741
diff changeset
   148
      progress.echo("output " + dir)
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   149
      Isabelle_System.mkdirs(dir)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   150
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   151
      for ((session, entries) <- session_entries) {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   152
        Isabelle_System.with_tmp_file(session, "data") { data_file =>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   153
          Isabelle_System.with_tmp_file(session, "gnuplot") { gnuplot_file =>
63706
76c2f833abf4 present ML timing as well;
wenzelm
parents: 63703
diff changeset
   154
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   155
            File.write(data_file,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   156
              cat_lines(
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   157
                entries.map(entry =>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   158
                  List(entry.date.unix_epoch.toString,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   159
                    entry.timing.elapsed.minutes,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   160
                    entry.timing.cpu.minutes,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   161
                    entry.ml_timing.elapsed.minutes,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   162
                    entry.ml_timing.cpu.minutes,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   163
                    entry.ml_timing.gc.minutes).mkString(" "))))
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   164
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   165
            val plots1 =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   166
              List(
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   167
                """ using 1:3 smooth sbezier title "cpu time (smooth)" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   168
                """ using 1:3 smooth csplines title "cpu time" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   169
                """ using 1:2 smooth sbezier title "elapsed time (smooth)" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   170
                """ using 1:2 smooth csplines title "elapsed time" """)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   171
            val plots2 =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   172
              List(
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   173
                """ using 1:5 smooth sbezier title "ML cpu time (smooth)" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   174
                """ using 1:5 smooth csplines title "ML cpu time" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   175
                """ using 1:4 smooth sbezier title "ML elapsed time (smooth)" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   176
                """ using 1:4 smooth csplines title "ML elapsed time" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   177
                """ using 1:6 smooth sbezier title "ML gc time (smooth)" """,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   178
                """ using 1:6 smooth csplines title "ML gc time" """)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   179
            val plots =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   180
              ml_timing match {
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   181
                case None => plots1
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   182
                case Some(false) => plots1 ::: plots2
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   183
                case Some(true) => plots2
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   184
              }
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   185
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   186
            File.write(gnuplot_file, """
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   187
set terminal png size """ + image_size._1 + "," + image_size._2 + """
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   188
set output """ + quote(File.standard_path(dir + Path.basic(session + ".png"))) + """
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   189
set xdata time
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   190
set timefmt "%s"
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   191
set format x "%d-%b"
63701
3744d2cf4d2f proper display of "_";
wenzelm
parents: 63700
diff changeset
   192
set xlabel """ + quote(session) + """ noenhanced
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   193
set key left top
64220
e7cbf81ec4b7 prefer Isabelle standard Path;
wenzelm
parents: 64161
diff changeset
   194
plot [] [0:] """ + plots.map(s => quote(data_file.implode) + " " + s).mkString(", ") + "\n")
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   195
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   196
            val result =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   197
              Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   198
            if (result.rc != 0)
65742
b9e0f25ba16a tuned messages;
wenzelm
parents: 65741
diff changeset
   199
              result.error("Gnuplot failed for " + name + "/" + session).check
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   200
          }
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   201
        }
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   202
      }
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   203
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   204
      File.write(dir + Path.basic("index.html"),
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   205
        html_header + "\n<h1>" + HTML.output(name) + "</h1>\n" +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   206
        cat_lines(
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   207
          session_entries.toList.map(_._1).sorted.map(session =>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   208
            """<br/><img src=""" + quote(HTML.output(session + ".png")) + """><br/>""")) +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   209
        "\n" + html_footer)
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   210
    }
63703
ec095a532a2b provide index.html;
wenzelm
parents: 63702
diff changeset
   211
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   212
    File.write(target_dir + Path.basic("index.html"),
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   213
      html_header + "\n<ul>\n" +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   214
      cat_lines(
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   215
        data_entries.map(_._1).map(name =>
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   216
          """<li> <a href=""" + quote(HTML.output(name + "/index.html")) + """>""" +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   217
            HTML.output(name) + """</a> </li>""")) +
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   218
      "\n</ul>\n" + html_footer)
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   219
  }
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   220
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   221
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   222
  /* Isabelle tool wrapper */
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   223
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   224
  val isabelle_tool =
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   225
    Isabelle_Tool("build_stats", "present statistics from build log database", args =>
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   226
    {
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   227
      var target_dir = default_target_dir
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   228
      var ml_timing: Option[Boolean] = None
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   229
      var only_sessions = Set.empty[String]
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   230
      var elapsed_threshold = Time.zero
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   231
      var history_length = default_history_length
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   232
      var options = Options.init()
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   233
      var image_size = default_image_size
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   234
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   235
      val getopts = Getopts("""
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   236
Usage: isabelle build_stats [OPTIONS]
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   237
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   238
  Options are:
65737
0729c09be90c tuned messages;
wenzelm
parents: 65736
diff changeset
   239
    -D DIR       target directory (default """ + default_target_dir + """)
63706
76c2f833abf4 present ML timing as well;
wenzelm
parents: 63703
diff changeset
   240
    -M           only ML timing
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   241
    -S SESSIONS  only given SESSIONS (comma separated)
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   242
    -T THRESHOLD only sessions with elapsed time >= THRESHOLD (minutes)
65737
0729c09be90c tuned messages;
wenzelm
parents: 65736
diff changeset
   243
    -l LENGTH    length of history (default """ + default_history_length + """)
63706
76c2f833abf4 present ML timing as well;
wenzelm
parents: 63703
diff changeset
   244
    -m           include ML timing
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   245
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
65737
0729c09be90c tuned messages;
wenzelm
parents: 65736
diff changeset
   246
    -s WxH       size of PNG image (default """ + image_size._1 + "x" + image_size._2 + """)
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   247
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   248
  Present performance statistics from build log database, which is specified
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   249
  via system options build_log_database_host, build_log_database_user etc.
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   250
""",
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   251
        "D:" -> (arg => target_dir = Path.explode(arg)),
63706
76c2f833abf4 present ML timing as well;
wenzelm
parents: 63703
diff changeset
   252
        "M" -> (_ => ml_timing = Some(true)),
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   253
        "S:" -> (arg => only_sessions = space_explode(',', arg).toSet),
63805
c272680df665 clarified modules;
wenzelm
parents: 63708
diff changeset
   254
        "T:" -> (arg => elapsed_threshold = Time.minutes(Value.Double.parse(arg))),
c272680df665 clarified modules;
wenzelm
parents: 63708
diff changeset
   255
        "l:" -> (arg => history_length = Value.Int.parse(arg)),
63706
76c2f833abf4 present ML timing as well;
wenzelm
parents: 63703
diff changeset
   256
        "m" -> (_ => ml_timing = Some(false)),
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   257
        "o:" -> (arg => options = options + arg),
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   258
        "s:" -> (arg =>
63805
c272680df665 clarified modules;
wenzelm
parents: 63708
diff changeset
   259
          space_explode('x', arg).map(Value.Int.parse(_)) match {
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   260
            case List(w, h) if w > 0 && h > 0 => image_size = (w, h)
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   261
            case _ => error("Error bad PNG image size: " + quote(arg))
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   262
          }))
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   263
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   264
      val more_args = getopts(args)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   265
      if (more_args.nonEmpty) getopts.usage()
63700
2a95d904672e clarified options and arguments;
wenzelm
parents: 63688
diff changeset
   266
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   267
      val progress = new Console_Progress
63688
cc57255bf6ae gnuplot presentation similar to former isatest-statistics;
wenzelm
parents: 63686
diff changeset
   268
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   269
      val data =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   270
        read_data(options, profiles = standard_profiles, progress = progress,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   271
          history_length = history_length, only_sessions = only_sessions,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   272
          elapsed_threshold = elapsed_threshold)
63703
ec095a532a2b provide index.html;
wenzelm
parents: 63702
diff changeset
   273
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   274
      present_data(data, progress = progress, target_dir = target_dir,
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   275
        image_size = image_size, ml_timing = ml_timing)
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65733
diff changeset
   276
64161
2b1128e95dfb explicit indication of Admin tools;
wenzelm
parents: 64106
diff changeset
   277
  }, admin = true)
63686
66f217416da7 statistics from session build output;
wenzelm
parents:
diff changeset
   278
}