src/Pure/Admin/build_log.scala
author wenzelm
Fri, 03 Jul 2020 16:48:57 +0200
changeset 71992 c8c3f4f0f68b
parent 71982 cea6087e8a70
child 72012 c81e58a81b8c
permissions -rw-r--r--
clarified log message (more uniform);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64160
1eea419fab65 clarified files;
wenzelm
parents: 64155
diff changeset
     1
/*  Title:      Pure/Admin/build_log.scala
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
     3
65608
d526ba7b0a2d tuned comment;
wenzelm
parents: 65607
diff changeset
     4
Management of build log files and database storage.
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
     6
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
     8
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
     9
64100
9b1573213ebe tuned error;
wenzelm
parents: 64099
diff changeset
    10
import java.io.{File => JFile}
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
    11
import java.time.format.{DateTimeFormatter, DateTimeParseException}
64096
5edeb60a7ec5 more flexible date formats;
wenzelm
parents: 64095
diff changeset
    12
import java.util.Locale
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
    13
65600
138ffa41dc54 clarified filter_files: sorted and unique;
wenzelm
parents: 65599
diff changeset
    14
import scala.collection.immutable.SortedMap
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
    15
import scala.collection.mutable
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
    16
import scala.util.matching.Regex
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
    17
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
    18
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
    19
object Build_Log
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
    20
{
64298
wenzelm
parents: 64297
diff changeset
    21
  /** content **/
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
    22
64298
wenzelm
parents: 64297
diff changeset
    23
  /* properties */
64150
b10f2ddd7679 clarified modules;
wenzelm
parents: 64120
diff changeset
    24
64298
wenzelm
parents: 64297
diff changeset
    25
  object Prop
wenzelm
parents: 64297
diff changeset
    26
  {
65624
32fa61f694ef clarified multi-line properties;
wenzelm
parents: 65623
diff changeset
    27
    val build_tags = SQL.Column.string("build_tags")  // lines
32fa61f694ef clarified multi-line properties;
wenzelm
parents: 65623
diff changeset
    28
    val build_args = SQL.Column.string("build_args")  // lines
65591
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    29
    val build_group_id = SQL.Column.string("build_group_id")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    30
    val build_id = SQL.Column.string("build_id")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    31
    val build_engine = SQL.Column.string("build_engine")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    32
    val build_host = SQL.Column.string("build_host")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    33
    val build_start = SQL.Column.date("build_start")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    34
    val build_end = SQL.Column.date("build_end")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    35
    val isabelle_version = SQL.Column.string("isabelle_version")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    36
    val afp_version = SQL.Column.string("afp_version")
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    37
65611
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    38
    val all_props: List[SQL.Column] =
65591
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    39
      List(build_tags, build_args, build_group_id, build_id, build_engine,
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
    40
        build_host, build_start, build_end, isabelle_version, afp_version)
64298
wenzelm
parents: 64297
diff changeset
    41
  }
64150
b10f2ddd7679 clarified modules;
wenzelm
parents: 64120
diff changeset
    42
b10f2ddd7679 clarified modules;
wenzelm
parents: 64120
diff changeset
    43
64298
wenzelm
parents: 64297
diff changeset
    44
  /* settings */
64080
2e5c0bd708af clarified modules;
wenzelm
parents: 64079
diff changeset
    45
64081
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    46
  object Settings
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    47
  {
65611
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    48
    val ISABELLE_BUILD_OPTIONS = SQL.Column.string("ISABELLE_BUILD_OPTIONS")
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    49
    val ML_PLATFORM = SQL.Column.string("ML_PLATFORM")
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    50
    val ML_HOME = SQL.Column.string("ML_HOME")
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    51
    val ML_SYSTEM = SQL.Column.string("ML_SYSTEM")
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    52
    val ML_OPTIONS = SQL.Column.string("ML_OPTIONS")
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    53
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    54
    val ml_settings = List(ML_PLATFORM, ML_HOME, ML_SYSTEM, ML_OPTIONS)
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    55
    val all_settings = ISABELLE_BUILD_OPTIONS :: ml_settings
64081
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    56
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    57
    type Entry = (String, String)
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    58
    type T = List[Entry]
64080
2e5c0bd708af clarified modules;
wenzelm
parents: 64079
diff changeset
    59
64081
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    60
    object Entry
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    61
    {
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    62
      def unapply(s: String): Option[Entry] =
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    63
        s.indexOf('=') match {
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    64
          case -1 => None
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    65
          case i =>
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    66
            val a = s.substring(0, i)
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    67
            val b = Library.perhaps_unquote(s.substring(i + 1))
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    68
            Some((a, b))
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    69
        }
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    70
      def apply(a: String, b: String): String = a + "=" + quote(b)
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    71
      def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    72
    }
64080
2e5c0bd708af clarified modules;
wenzelm
parents: 64079
diff changeset
    73
71992
c8c3f4f0f68b clarified log message (more uniform);
wenzelm
parents: 71982
diff changeset
    74
    def show(): String =
64081
38bb09ed965b more uniform treatment of settings;
wenzelm
parents: 64080
diff changeset
    75
      cat_lines(
71992
c8c3f4f0f68b clarified log message (more uniform);
wenzelm
parents: 71982
diff changeset
    76
        List(Entry.getenv("ISABELLE_TOOL_JAVA_OPTIONS"),
c8c3f4f0f68b clarified log message (more uniform);
wenzelm
parents: 71982
diff changeset
    77
          Entry.getenv(ISABELLE_BUILD_OPTIONS.name), "") :::
65611
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
    78
        ml_settings.map(c => Entry.getenv(c.name)))
64080
2e5c0bd708af clarified modules;
wenzelm
parents: 64079
diff changeset
    79
  }
2e5c0bd708af clarified modules;
wenzelm
parents: 64079
diff changeset
    80
2e5c0bd708af clarified modules;
wenzelm
parents: 64079
diff changeset
    81
64298
wenzelm
parents: 64297
diff changeset
    82
  /* file names */
wenzelm
parents: 64297
diff changeset
    83
wenzelm
parents: 64297
diff changeset
    84
  def log_date(date: Date): String =
wenzelm
parents: 64297
diff changeset
    85
    String.format(Locale.ROOT, "%s.%05d",
wenzelm
parents: 64297
diff changeset
    86
      DateTimeFormatter.ofPattern("yyyy-MM-dd").format(date.rep),
71163
b5822f4c3fde tuned -- avoid deprecated constructors;
wenzelm
parents: 69980
diff changeset
    87
      java.lang.Long.valueOf((date.time - date.midnight.time).ms / 1000))
64298
wenzelm
parents: 64297
diff changeset
    88
wenzelm
parents: 64297
diff changeset
    89
  def log_subdir(date: Date): Path =
wenzelm
parents: 64297
diff changeset
    90
    Path.explode("log") + Path.explode(date.rep.getYear.toString)
wenzelm
parents: 64297
diff changeset
    91
wenzelm
parents: 64297
diff changeset
    92
  def log_filename(engine: String, date: Date, more: List[String] = Nil): Path =
wenzelm
parents: 64297
diff changeset
    93
    Path.explode((engine :: log_date(date) :: more).mkString("", "_", ".log"))
wenzelm
parents: 64297
diff changeset
    94
wenzelm
parents: 64297
diff changeset
    95
64100
9b1573213ebe tuned error;
wenzelm
parents: 64099
diff changeset
    96
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
    97
  /** log file **/
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
    98
64155
646c4d6a6a02 tuned signature;
wenzelm
parents: 64150
diff changeset
    99
  def print_date(date: Date): String = Log_File.Date_Format(date)
646c4d6a6a02 tuned signature;
wenzelm
parents: 64150
diff changeset
   100
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   101
  object Log_File
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   102
  {
65607
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   103
    /* log file */
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   104
65609
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   105
    def plain_name(name: String): String =
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   106
    {
71621
wenzelm
parents: 71620
diff changeset
   107
      List(".log", ".log.gz", ".log.xz", ".gz", ".xz").find(name.endsWith) match {
65609
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   108
        case Some(s) => Library.try_unsuffix(s, name).get
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   109
        case None => name
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   110
      }
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   111
    }
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   112
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   113
    def apply(name: String, lines: List[String]): Log_File =
71653
6f7a54954f19 more robust: process stdout on Windows may contain CR;
wenzelm
parents: 71630
diff changeset
   114
      new Log_File(plain_name(name), lines.map(Library.trim_line))
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   115
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   116
    def apply(name: String, text: String): Log_File =
71653
6f7a54954f19 more robust: process stdout on Windows may contain CR;
wenzelm
parents: 71630
diff changeset
   117
      new Log_File(plain_name(name), Library.trim_split_lines(text))
64090
5a68280112b3 more operations;
wenzelm
parents: 64089
diff changeset
   118
5a68280112b3 more operations;
wenzelm
parents: 64089
diff changeset
   119
    def apply(file: JFile): Log_File =
5a68280112b3 more operations;
wenzelm
parents: 64089
diff changeset
   120
    {
5a68280112b3 more operations;
wenzelm
parents: 64089
diff changeset
   121
      val name = file.getName
65609
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   122
      val text =
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   123
        if (name.endsWith(".gz")) File.read_gzip(file)
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   124
        else if (name.endsWith(".xz")) File.read_xz(file)
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   125
        else File.read(file)
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   126
      apply(name, text)
64090
5a68280112b3 more operations;
wenzelm
parents: 64089
diff changeset
   127
    }
5a68280112b3 more operations;
wenzelm
parents: 64089
diff changeset
   128
5a68280112b3 more operations;
wenzelm
parents: 64089
diff changeset
   129
    def apply(path: Path): Log_File = apply(path.file)
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   130
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   131
65607
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   132
    /* log file collections */
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   133
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   134
    def is_log(file: JFile,
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   135
      prefixes: List[String] =
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents: 66944
diff changeset
   136
        List(Build_History.log_prefix, Identify.log_prefix, Identify.log_prefix2,
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents: 66944
diff changeset
   137
          Isatest.log_prefix, AFP_Test.log_prefix, Jenkins.log_prefix),
65609
9917b8e3b5c1 clarified plain_name / log_name;
wenzelm
parents: 65608
diff changeset
   138
      suffixes: List[String] = List(".log", ".log.gz", ".log.xz")): Boolean =
65607
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   139
    {
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   140
      val name = file.getName
65639
4c14da234221 exclude special log files;
wenzelm
parents: 65636
diff changeset
   141
71621
wenzelm
parents: 71620
diff changeset
   142
      prefixes.exists(name.startsWith) &&
wenzelm
parents: 71620
diff changeset
   143
      suffixes.exists(name.endsWith) &&
65639
4c14da234221 exclude special log files;
wenzelm
parents: 65636
diff changeset
   144
      name != "isatest.log" &&
4c14da234221 exclude special log files;
wenzelm
parents: 65636
diff changeset
   145
      name != "afp-test.log" &&
4c14da234221 exclude special log files;
wenzelm
parents: 65636
diff changeset
   146
      name != "main.log"
65607
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   147
    }
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   148
c937984c70e9 tuned signature;
wenzelm
parents: 65605
diff changeset
   149
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   150
    /* date format */
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   151
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   152
    val Date_Format =
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   153
    {
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   154
      val fmts =
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   155
        Date.Formatter.variants(
64116
6cfd429a4296 prefer explicit timezone offset for printing;
wenzelm
parents: 64111
diff changeset
   156
          List("EEE MMM d HH:mm:ss O yyyy", "EEE MMM d HH:mm:ss VV yyyy"),
64104
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   157
          List(Locale.ENGLISH, Locale.GERMAN)) :::
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   158
        List(
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   159
          DateTimeFormatter.RFC_1123_DATE_TIME,
69980
f2e3adfd916f tuned signature;
wenzelm
parents: 69299
diff changeset
   160
          Date.Formatter.pattern("EEE MMM d HH:mm:ss yyyy").withZone(Date.timezone_berlin))
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   161
64104
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   162
      def tune_timezone(s: String): String =
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   163
        s match {
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   164
          case "CET" | "MET" => "GMT+1"
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   165
          case "CEST" | "MEST" => "GMT+2"
64104
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   166
          case "EST" => "Europe/Berlin"
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   167
          case _ => s
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   168
        }
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   169
      def tune_weekday(s: String): String =
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   170
        s match {
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   171
          case "Die" => "Di"
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   172
          case "Mit" => "Mi"
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   173
          case "Don" => "Do"
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   174
          case "Fre" => "Fr"
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   175
          case "Sam" => "Sa"
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   176
          case "Son" => "So"
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   177
          case _ => s
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   178
        }
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   179
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   180
      def tune(s: String): String =
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   181
        Word.implode(
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   182
          Word.explode(s) match {
71621
wenzelm
parents: 71620
diff changeset
   183
            case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone)
wenzelm
parents: 71620
diff changeset
   184
            case a :: bs => tune_weekday(a) :: bs.map(tune_timezone)
64104
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   185
            case Nil => Nil
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   186
          }
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   187
        )
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   188
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   189
      Date.Format.make(fmts, tune)
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   190
    }
64102
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   191
  }
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   192
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   193
  class Log_File private(val name: String, val lines: List[String])
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   194
  {
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   195
    log_file =>
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   196
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   197
    override def toString: String = name
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   198
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   199
    def text: String = cat_lines(lines)
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   200
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   201
    def err(msg: String): Nothing =
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   202
      error("Error in log file " + quote(name) + ": " + msg)
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   203
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   204
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   205
    /* date format */
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   206
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   207
    object Strict_Date
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   208
    {
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   209
      def unapply(s: String): Some[Date] =
64102
1ec2adddf16b prefer static Date_Format;
wenzelm
parents: 64101
diff changeset
   210
        try { Some(Log_File.Date_Format.parse(s)) }
64101
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   211
        catch { case exn: DateTimeParseException => log_file.err(exn.getMessage) }
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   212
    }
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   213
976289c733e6 more formal directory content;
wenzelm
parents: 64100
diff changeset
   214
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   215
    /* inlined text */
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   216
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   217
    def filter(Marker: Protocol_Message.Marker): List[String] =
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   218
      for (Marker(text) <- lines) yield text
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   219
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   220
    def find(Marker: Protocol_Message.Marker): Option[String] =
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   221
      lines.collectFirst({ case Marker(text) => text })
64196
6688b9cd443b more robust wrt. old versions that use clear-text properties (e.g. Timing in build_history_base);
wenzelm
parents: 64193
diff changeset
   222
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   223
    def find_match(regexes: List[Regex]): Option[String] =
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   224
      regexes match {
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   225
        case Nil => None
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   226
        case regex :: rest =>
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   227
          lines.iterator.map(regex.unapplySeq(_)).find(res => res.isDefined && res.get.length == 1).
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   228
            map(res => res.get.head) orElse find_match(rest)
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   229
      }
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   230
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   231
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   232
    /* settings */
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   233
64091
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   234
    def get_setting(a: String): Option[Settings.Entry] =
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   235
      lines.find(_.startsWith(a + "=")) match {
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   236
        case Some(line) => Settings.Entry.unapply(line)
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   237
        case None => None
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   238
      }
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
   239
65611
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   240
    def get_all_settings: Settings.T =
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   241
      for { c <- Settings.all_settings; entry <- get_setting(c.name) }
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   242
      yield entry
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   243
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   244
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   245
    /* properties (YXML) */
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   246
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   247
    val xml_cache: XML.Cache = XML.make_cache()
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   248
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   249
    def parse_props(text: String): Properties.T =
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   250
      try { xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) }
66046
37226f74f33a tuned message;
wenzelm
parents: 65937
diff changeset
   251
      catch { case _: XML.Error => log_file.err("malformed properties") }
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   252
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   253
    def filter_props(marker: Protocol_Message.Marker): List[Properties.T] =
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   254
      for (text <- filter(marker) if YXML.detect(text)) yield parse_props(text)
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   255
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   256
    def find_props(marker: Protocol_Message.Marker): Option[Properties.T] =
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   257
      for (text <- find(marker) if YXML.detect(text)) yield parse_props(text)
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   258
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   259
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   260
    /* parse various formats */
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   261
64105
d93bd6d253c6 tuned signature;
wenzelm
parents: 64104
diff changeset
   262
    def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
d93bd6d253c6 tuned signature;
wenzelm
parents: 64104
diff changeset
   263
65646
014dbbe5331f parse ml_statistics only when required;
wenzelm
parents: 65645
diff changeset
   264
    def parse_build_info(ml_statistics: Boolean = false): Build_Info =
014dbbe5331f parse ml_statistics only when required;
wenzelm
parents: 65645
diff changeset
   265
      Build_Log.parse_build_info(log_file, ml_statistics)
64105
d93bd6d253c6 tuned signature;
wenzelm
parents: 64104
diff changeset
   266
64082
d57c7295f601 clarified signature;
wenzelm
parents: 64081
diff changeset
   267
    def parse_session_info(
d57c7295f601 clarified signature;
wenzelm
parents: 64081
diff changeset
   268
        command_timings: Boolean = false,
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66863
diff changeset
   269
        theory_timings: Boolean = false,
64082
d57c7295f601 clarified signature;
wenzelm
parents: 64081
diff changeset
   270
        ml_statistics: Boolean = false,
d57c7295f601 clarified signature;
wenzelm
parents: 64081
diff changeset
   271
        task_statistics: Boolean = false): Session_Info =
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66863
diff changeset
   272
      Build_Log.parse_session_info(
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66863
diff changeset
   273
        log_file, command_timings, theory_timings, ml_statistics, task_statistics)
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
   274
  }
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
   275
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
   276
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
   277
65276
fa1a5efee2ec tuned comments;
wenzelm
parents: 65052
diff changeset
   278
  /** digested meta info: produced by Admin/build_history in log.xz file **/
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
   279
64108
623abb8fecdf clarified meta info;
wenzelm
parents: 64107
diff changeset
   280
  object Meta_Info
64099
wenzelm
parents: 64098
diff changeset
   281
  {
64108
623abb8fecdf clarified meta info;
wenzelm
parents: 64107
diff changeset
   282
    val empty: Meta_Info = Meta_Info(Nil, Nil)
64099
wenzelm
parents: 64098
diff changeset
   283
  }
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
   284
65611
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   285
  sealed case class Meta_Info(props: Properties.T, settings: Settings.T)
64103
60d163f38056 accept spurious empty logs;
wenzelm
parents: 64102
diff changeset
   286
  {
60d163f38056 accept spurious empty logs;
wenzelm
parents: 64102
diff changeset
   287
    def is_empty: Boolean = props.isEmpty && settings.isEmpty
65599
08dfa79866ec database storage of Meta_Info and Build_Info;
wenzelm
parents: 65595
diff changeset
   288
65611
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   289
    def get(c: SQL.Column): Option[String] =
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   290
      Properties.get(props, c.name) orElse
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   291
      Properties.get(settings, c.name)
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   292
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   293
    def get_date(c: SQL.Column): Option[Date] =
71621
wenzelm
parents: 71620
diff changeset
   294
      get(c).map(Log_File.Date_Format.parse)
64103
60d163f38056 accept spurious empty logs;
wenzelm
parents: 64102
diff changeset
   295
  }
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   296
65625
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   297
  object Identify
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   298
  {
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   299
    val log_prefix = "isabelle_identify_"
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents: 66944
diff changeset
   300
    val log_prefix2 = "plain_identify_"
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   301
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   302
    def engine(log_file: Log_File): String =
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   303
      if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify"
66995
9cb263dbb2f7 plain identify job for Isabelle + AFP, independent of any Isabelle technology;
wenzelm
parents: 66944
diff changeset
   304
      else if (log_file.name.startsWith(log_prefix2)) "plain_identify"
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   305
      else "identify"
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   306
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   307
    def content(date: Date, isabelle_version: Option[String], afp_version: Option[String]): String =
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   308
      terminate_lines(
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   309
        List("isabelle_identify: " + Build_Log.print_date(date), "") :::
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   310
        isabelle_version.map("Isabelle version: " + _).toList :::
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   311
        afp_version.map("AFP version: " + _).toList)
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   312
65625
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   313
    val Start = new Regex("""^isabelle_identify: (.+)$""")
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   314
    val No_End = new Regex("""$.""")
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   315
    val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$"""))
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   316
    val AFP_Version = List(new Regex("""^AFP version: (\S+)$"""))
65625
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   317
  }
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   318
64095
1a6d37c31df9 support for isatest format;
wenzelm
parents: 64094
diff changeset
   319
  object Isatest
1a6d37c31df9 support for isatest format;
wenzelm
parents: 64094
diff changeset
   320
  {
65588
b0d8d97198b3 clarified signature;
wenzelm
parents: 65318
diff changeset
   321
    val log_prefix = "isatest-makeall-"
64108
623abb8fecdf clarified meta info;
wenzelm
parents: 64107
diff changeset
   322
    val engine = "isatest"
64109
wenzelm
parents: 64108
diff changeset
   323
    val Start = new Regex("""^------------------- starting test --- (.+) --- (.+)$""")
wenzelm
parents: 64108
diff changeset
   324
    val End = new Regex("""^------------------- test (?:successful|FAILED) --- (.+) --- .*$""")
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   325
    val Isabelle_Version = List(new Regex("""^Isabelle version: (\S+)$"""))
64095
1a6d37c31df9 support for isatest format;
wenzelm
parents: 64094
diff changeset
   326
  }
1a6d37c31df9 support for isatest format;
wenzelm
parents: 64094
diff changeset
   327
64109
wenzelm
parents: 64108
diff changeset
   328
  object AFP_Test
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   329
  {
65588
b0d8d97198b3 clarified signature;
wenzelm
parents: 65318
diff changeset
   330
    val log_prefix = "afp-test-devel-"
64108
623abb8fecdf clarified meta info;
wenzelm
parents: 64107
diff changeset
   331
    val engine = "afp-test"
64109
wenzelm
parents: 64108
diff changeset
   332
    val Start = new Regex("""^Start test(?: for .+)? at ([^,]+), (.*)$""")
wenzelm
parents: 64108
diff changeset
   333
    val Start_Old = new Regex("""^Start test(?: for .+)? at ([^,]+)$""")
wenzelm
parents: 64108
diff changeset
   334
    val End = new Regex("""^End test on (.+), .+, elapsed time:.*$""")
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   335
    val Isabelle_Version = List(new Regex("""^Isabelle version: .* -- hg id (\S+)$"""))
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   336
    val AFP_Version = List(new Regex("""^AFP version: .* -- hg id (\S+)$"""))
64104
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   337
    val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   338
  }
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   339
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   340
  object Jenkins
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   341
  {
65664
c84db5e0dd6d detect Jenkins log files as well;
wenzelm
parents: 65663
diff changeset
   342
    val log_prefix = "jenkins_"
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   343
    val engine = "jenkins"
65663
61cd86bb9613 detect host name;
wenzelm
parents: 65649
diff changeset
   344
    val Host = new Regex("""^Building remotely on (\S+) \((\S+)\).*$""")
65665
9b7fb07b4a96 more robust detection of Jenkins log;
wenzelm
parents: 65664
diff changeset
   345
    val Start = new Regex("""^(?:Started by an SCM change|Started from command line by admin|).*$""")
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   346
    val Start_Date = new Regex("""^Build started at (.+)$""")
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   347
    val No_End = new Regex("""$.""")
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   348
    val Isabelle_Version =
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   349
      List(new Regex("""^(?:Build for Isabelle id|Isabelle id) (\w+).*$"""),
65685
47bbf7150aae detect old log files (early 2016);
wenzelm
parents: 65684
diff changeset
   350
        new Regex("""^ISABELLE_CI_REPO_ID="(\w+)".*$"""),
47bbf7150aae detect old log files (early 2016);
wenzelm
parents: 65684
diff changeset
   351
        new Regex("""^(\w{12}) tip.*$"""))
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   352
    val AFP_Version =
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   353
      List(new Regex("""^(?:Build for AFP id|AFP id) (\w+).*$"""),
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   354
        new Regex("""^ISABELLE_CI_AFP_ID="(\w+)".*$"""))
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   355
    val CONFIGURATION = "=== CONFIGURATION ==="
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   356
    val BUILD = "=== BUILD ==="
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   357
  }
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   358
64105
d93bd6d253c6 tuned signature;
wenzelm
parents: 64104
diff changeset
   359
  private def parse_meta_info(log_file: Log_File): Meta_Info =
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   360
  {
64108
623abb8fecdf clarified meta info;
wenzelm
parents: 64107
diff changeset
   361
    def parse(engine: String, host: String, start: Date,
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   362
      End: Regex, Isabelle_Version: List[Regex], AFP_Version: List[Regex]): Meta_Info =
64091
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   363
    {
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64196
diff changeset
   364
      val build_id =
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64196
diff changeset
   365
      {
65714
wenzelm
parents: 65709
diff changeset
   366
        val prefix = proper_string(host) orElse proper_string(engine) getOrElse "build"
wenzelm
parents: 65709
diff changeset
   367
        prefix + ":" + start.time.ms
64296
544481988e65 explicit identification of builds and correlated build groups;
wenzelm
parents: 64196
diff changeset
   368
      }
65591
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
   369
      val build_engine = if (engine == "") Nil else List(Prop.build_engine.name -> engine)
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
   370
      val build_host = if (host == "") Nil else List(Prop.build_host.name -> host)
64108
623abb8fecdf clarified meta info;
wenzelm
parents: 64107
diff changeset
   371
65599
08dfa79866ec database storage of Meta_Info and Build_Info;
wenzelm
parents: 65595
diff changeset
   372
      val start_date = List(Prop.build_start.name -> print_date(start))
64091
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   373
      val end_date =
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   374
        log_file.lines.last match {
64109
wenzelm
parents: 64108
diff changeset
   375
          case End(log_file.Strict_Date(end_date)) =>
65599
08dfa79866ec database storage of Meta_Info and Build_Info;
wenzelm
parents: 65595
diff changeset
   376
            List(Prop.build_end.name -> print_date(end_date))
64091
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   377
          case _ => Nil
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   378
        }
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   379
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   380
      val isabelle_version =
65591
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
   381
        log_file.find_match(Isabelle_Version).map(Prop.isabelle_version.name -> _)
64091
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   382
      val afp_version =
65591
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
   383
        log_file.find_match(AFP_Version).map(Prop.afp_version.name -> _)
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   384
65591
5953c7fbc2b8 more SQL operations;
wenzelm
parents: 65590
diff changeset
   385
      Meta_Info((Prop.build_id.name -> build_id) :: build_engine ::: build_host :::
64108
623abb8fecdf clarified meta info;
wenzelm
parents: 64107
diff changeset
   386
          start_date ::: end_date ::: isabelle_version.toList ::: afp_version.toList,
65611
a4a7841ae84f more uniform storage of Meta_Info;
wenzelm
parents: 65609
diff changeset
   387
        log_file.get_all_settings)
64091
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   388
    }
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   389
f8dfba90e73f more liberal parsing for old AFP logs;
wenzelm
parents: 64090
diff changeset
   390
    log_file.lines match {
71630
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   391
      case line :: _ if Protocol.Meta_Info_Marker.test_yxml(line) =>
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   392
        Meta_Info(log_file.find_props(Protocol.Meta_Info_Marker).get, log_file.get_all_settings)
64117
c2b41b073d8a build_history log files with formal meta info;
wenzelm
parents: 64116
diff changeset
   393
65625
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   394
      case Identify.Start(log_file.Strict_Date(start)) :: _ =>
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65670
diff changeset
   395
        parse(Identify.engine(log_file), "", start, Identify.No_End,
65625
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   396
          Identify.Isabelle_Version, Identify.AFP_Version)
13552d5c0005 more log files;
wenzelm
parents: 65624
diff changeset
   397
64109
wenzelm
parents: 64108
diff changeset
   398
      case Isatest.Start(log_file.Strict_Date(start), host) :: _ =>
wenzelm
parents: 64108
diff changeset
   399
        parse(Isatest.engine, host, start, Isatest.End,
65684
00d4663270d9 explicit support for multiple regexes;
wenzelm
parents: 65683
diff changeset
   400
          Isatest.Isabelle_Version, Nil)
64099
wenzelm
parents: 64098
diff changeset
   401
64109
wenzelm
parents: 64108
diff changeset
   402
      case AFP_Test.Start(log_file.Strict_Date(start), host) :: _ =>
wenzelm
parents: 64108
diff changeset
   403
        parse(AFP_Test.engine, host, start, AFP_Test.End,
wenzelm
parents: 64108
diff changeset
   404
          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
64099
wenzelm
parents: 64098
diff changeset
   405
64109
wenzelm
parents: 64108
diff changeset
   406
      case AFP_Test.Start_Old(log_file.Strict_Date(start)) :: _ =>
wenzelm
parents: 64108
diff changeset
   407
        parse(AFP_Test.engine, "", start, AFP_Test.End,
wenzelm
parents: 64108
diff changeset
   408
          AFP_Test.Isabelle_Version, AFP_Test.AFP_Version)
64099
wenzelm
parents: 64098
diff changeset
   409
65665
9b7fb07b4a96 more robust detection of Jenkins log;
wenzelm
parents: 65664
diff changeset
   410
      case Jenkins.Start() :: _ =>
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   411
        log_file.lines.dropWhile(_ != Jenkins.BUILD) match {
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   412
          case Jenkins.BUILD :: _ :: Jenkins.Start_Date(log_file.Strict_Date(start)) :: _ =>
65663
61cd86bb9613 detect host name;
wenzelm
parents: 65649
diff changeset
   413
            val host =
61cd86bb9613 detect host name;
wenzelm
parents: 65649
diff changeset
   414
              log_file.lines.takeWhile(_ != Jenkins.CONFIGURATION).collectFirst({
61cd86bb9613 detect host name;
wenzelm
parents: 65649
diff changeset
   415
                case Jenkins.Host(a, b) => a + "." + b
61cd86bb9613 detect host name;
wenzelm
parents: 65649
diff changeset
   416
              }).getOrElse("")
69980
f2e3adfd916f tuned signature;
wenzelm
parents: 69299
diff changeset
   417
            parse(Jenkins.engine, host, start.to(Date.timezone_berlin), Jenkins.No_End,
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   418
              Jenkins.Isabelle_Version, Jenkins.AFP_Version)
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   419
          case _ => Meta_Info.empty
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   420
        }
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   421
64341
45b6faeee56d avoid deprecated Scala;
wenzelm
parents: 64303
diff changeset
   422
      case line :: _ if line.startsWith("\u0000") => Meta_Info.empty
64109
wenzelm
parents: 64108
diff changeset
   423
      case List(Isatest.End(_)) => Meta_Info.empty
wenzelm
parents: 64108
diff changeset
   424
      case _ :: AFP_Test.Bad_Init() :: _ => Meta_Info.empty
64105
d93bd6d253c6 tuned signature;
wenzelm
parents: 64104
diff changeset
   425
      case Nil => Meta_Info.empty
64104
b70fa05d6746 more permissive: accept all historic isatest and afp-test logs;
wenzelm
parents: 64103
diff changeset
   426
64110
c0b96b34c7b9 support for Isabelle/Jenkins log file format;
wenzelm
parents: 64109
diff changeset
   427
      case _ => log_file.err("cannot detect log file format")
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   428
    }
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   429
  }
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   430
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   431
64098
099518e8af2c misc tuning and clarification;
wenzelm
parents: 64096
diff changeset
   432
65276
fa1a5efee2ec tuned comments;
wenzelm
parents: 65052
diff changeset
   433
  /** build info: toplevel output of isabelle build or Admin/build_history **/
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   434
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   435
  val SESSION_NAME = "session_name"
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   436
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   437
  object Session_Status extends Enumeration
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   438
  {
65633
wenzelm
parents: 65632
diff changeset
   439
    val existing, finished, failed, cancelled = Value
64061
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   440
  }
1bbea2b55d22 some support for header and data fields, notably from afp-test;
wenzelm
parents: 64054
diff changeset
   441
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   442
  sealed case class Session_Entry(
65643
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   443
    chapter: String = "",
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   444
    groups: List[String] = Nil,
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   445
    threads: Option[Int] = None,
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   446
    timing: Timing = Timing.zero,
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   447
    ml_timing: Timing = Timing.zero,
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   448
    sources: Option[String] = None,
65643
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   449
    heap_size: Option[Long] = None,
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   450
    status: Option[Session_Status.Value] = None,
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   451
    errors: List[String] = Nil,
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   452
    theory_timings: Map[String, Timing] = Map.empty,
65643
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   453
    ml_statistics: List[Properties.T] = Nil)
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   454
  {
65631
ee917f172912 clarified database content;
wenzelm
parents: 65629
diff changeset
   455
    def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups))
65643
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   456
    def finished: Boolean = status == Some(Session_Status.finished)
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   457
    def failed: Boolean = status == Some(Session_Status.failed)
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   458
  }
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   459
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   460
  object Build_Info
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   461
  {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   462
    val sessions_dummy: Map[String, Session_Entry] =
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   463
      Map("" -> Session_Entry(theory_timings = Map("" -> Timing.zero)))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   464
  }
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   465
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   466
  sealed case class Build_Info(sessions: Map[String, Session_Entry])
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   467
  {
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   468
    def finished_sessions: List[String] = for ((a, b) <- sessions.toList if b.finished) yield a
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   469
    def failed_sessions: List[String] = for ((a, b) <- sessions.toList if b.failed) yield a
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   470
  }
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   471
65646
014dbbe5331f parse ml_statistics only when required;
wenzelm
parents: 65645
diff changeset
   472
  private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info =
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   473
  {
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   474
    object Chapter_Name
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   475
    {
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   476
      def unapply(s: String): Some[(String, String)] =
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   477
        space_explode('/', s) match {
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   478
          case List(chapter, name) => Some((chapter, name))
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   479
          case _ => Some(("", s))
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   480
        }
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   481
    }
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   482
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   483
    val Session_No_Groups = new Regex("""^Session (\S+)$""")
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   484
    val Session_Groups = new Regex("""^Session (\S+) \((.*)\)$""")
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   485
    val Session_Finished1 =
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   486
      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   487
    val Session_Finished2 =
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   488
      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   489
    val Session_Timing =
65679
45632d594bdb more general pattern;
wenzelm
parents: 65674
diff changeset
   490
      new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
64086
ac7ae5067783 clarified status: started sessions may bomb without explicit FAILED or CANCELLED (cf. in afp-test-devel-2016-01-03.log);
wenzelm
parents: 64085
diff changeset
   491
    val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   492
    val Session_Failed = new Regex("""^(\S+) FAILED""")
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   493
    val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   494
    val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""")
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   495
    val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""")
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   496
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   497
    object Theory_Timing
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   498
    {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   499
      def unapply(line: String): Option[(String, (String, Timing))] =
71630
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   500
        Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props)
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   501
        match {
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   502
          case Some((SESSION_NAME, name) :: props) =>
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   503
            (props, props) match {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   504
              case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   505
              case _ => None
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   506
            }
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   507
          case _ => None
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   508
        }
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   509
    }
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   510
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   511
    var chapter = Map.empty[String, String]
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   512
    var groups = Map.empty[String, List[String]]
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   513
    var threads = Map.empty[String, Int]
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   514
    var timing = Map.empty[String, Timing]
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   515
    var ml_timing = Map.empty[String, Timing]
64086
ac7ae5067783 clarified status: started sessions may bomb without explicit FAILED or CANCELLED (cf. in afp-test-devel-2016-01-03.log);
wenzelm
parents: 64085
diff changeset
   516
    var started = Set.empty[String]
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   517
    var failed = Set.empty[String]
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   518
    var cancelled = Set.empty[String]
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   519
    var sources = Map.empty[String, String]
65627
bb185e442c95 put bulky data last;
wenzelm
parents: 65626
diff changeset
   520
    var heap_sizes = Map.empty[String, Long]
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   521
    var theory_timings = Map.empty[String, Map[String, Timing]]
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   522
    var ml_statistics = Map.empty[String, List[Properties.T]]
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   523
    var errors = Map.empty[String, List[String]]
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   524
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   525
    def all_sessions: Set[String] =
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   526
      chapter.keySet ++ groups.keySet ++ threads.keySet ++ timing.keySet ++ ml_timing.keySet ++
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   527
      failed ++ cancelled ++ started ++ sources.keySet ++ heap_sizes.keySet ++
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   528
      theory_timings.keySet ++ ml_statistics.keySet
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   529
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   530
64062
a7352cbde7d7 misc tuning and clarification;
wenzelm
parents: 64061
diff changeset
   531
    for (line <- log_file.lines) {
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   532
      line match {
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   533
        case Session_No_Groups(Chapter_Name(chapt, name)) =>
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   534
          chapter += (name -> chapt)
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   535
          groups += (name -> Nil)
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   536
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   537
        case Session_Groups(Chapter_Name(chapt, name), grps) =>
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   538
          chapter += (name -> chapt)
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   539
          groups += (name -> Word.explode(grps))
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   540
64086
ac7ae5067783 clarified status: started sessions may bomb without explicit FAILED or CANCELLED (cf. in afp-test-devel-2016-01-03.log);
wenzelm
parents: 64085
diff changeset
   541
        case Session_Started(name) =>
ac7ae5067783 clarified status: started sessions may bomb without explicit FAILED or CANCELLED (cf. in afp-test-devel-2016-01-03.log);
wenzelm
parents: 64085
diff changeset
   542
          started += name
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   543
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   544
        case Session_Finished1(name,
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   545
            Value.Int(e1), Value.Int(e2), Value.Int(e3),
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   546
            Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   547
          val elapsed = Time.hms(e1, e2, e3)
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   548
          val cpu = Time.hms(c1, c2, c3)
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   549
          timing += (name -> Timing(elapsed, cpu, Time.zero))
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   550
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   551
        case Session_Finished2(name,
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   552
            Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   553
          val elapsed = Time.hms(e1, e2, e3)
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   554
          timing += (name -> Timing(elapsed, Time.zero, Time.zero))
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   555
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   556
        case Session_Timing(name,
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   557
            Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   558
          val elapsed = Time.seconds(e)
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   559
          val cpu = Time.seconds(c)
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   560
          val gc = Time.seconds(g)
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   561
          ml_timing += (name -> Timing(elapsed, cpu, gc))
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   562
          threads += (name -> t)
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   563
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   564
        case Sources(name, s) =>
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   565
          sources += (name -> s)
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   566
64120
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   567
        case Heap(name, Value.Long(size)) =>
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   568
          heap_sizes += (name -> size)
6c5039016321 record heap sizes;
wenzelm
parents: 64119
diff changeset
   569
71630
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   570
        case _ if Protocol.Theory_Timing_Marker.test_yxml(line) =>
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   571
          line match {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   572
            case Theory_Timing(name, theory_timing) =>
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   573
              theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   574
            case _ => log_file.err("malformed theory_timing " + quote(line))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   575
          }
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   576
71630
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   577
        case _ if parse_ml_statistics && Protocol.ML_Statistics_Marker.test_yxml(line) =>
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   578
          Protocol.ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match {
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   579
            case Some((SESSION_NAME, name) :: props) =>
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   580
              ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil)))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   581
            case _ => log_file.err("malformed ML_statistics " + quote(line))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   582
          }
64119
8094eaa38d4b inline session ML statistics into main build log;
wenzelm
parents: 64117
diff changeset
   583
71630
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   584
        case _ if Protocol.Error_Message_Marker.test_yxml(line) =>
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   585
          Protocol.Error_Message_Marker.unapply(line).map(log_file.parse_props) match {
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   586
            case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) =>
71620
5a4ccef7f310 more explicit type Protocol_Message.Marker;
wenzelm
parents: 71163
diff changeset
   587
              errors += (name -> (msg :: errors.getOrElse(name, Nil)))
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   588
            case _ => log_file.err("malformed error message " + quote(line))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   589
          }
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   590
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   591
        case _ =>
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   592
      }
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   593
    }
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   594
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   595
    val sessions =
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   596
      Map(
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   597
        (for (name <- all_sessions.toList) yield {
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   598
          val status =
65633
wenzelm
parents: 65632
diff changeset
   599
            if (failed(name)) Session_Status.failed
wenzelm
parents: 65632
diff changeset
   600
            else if (cancelled(name)) Session_Status.cancelled
64086
ac7ae5067783 clarified status: started sessions may bomb without explicit FAILED or CANCELLED (cf. in afp-test-devel-2016-01-03.log);
wenzelm
parents: 64085
diff changeset
   601
            else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
65633
wenzelm
parents: 65632
diff changeset
   602
              Session_Status.finished
wenzelm
parents: 65632
diff changeset
   603
            else if (started(name)) Session_Status.failed
wenzelm
parents: 65632
diff changeset
   604
            else Session_Status.existing
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   605
          val entry =
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   606
            Session_Entry(
65643
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   607
              chapter = chapter.getOrElse(name, ""),
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   608
              groups = groups.getOrElse(name, Nil),
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   609
              threads = threads.get(name),
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   610
              timing = timing.getOrElse(name, Timing.zero),
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   611
              ml_timing = ml_timing.getOrElse(name, Timing.zero),
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   612
              sources = sources.get(name),
65643
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   613
              heap_size = heap_sizes.get(name),
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   614
              status = Some(status),
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   615
              errors = errors.getOrElse(name, Nil).reverse,
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   616
              theory_timings = theory_timings.getOrElse(name, Map.empty),
65643
a54371226182 clarified dummy Session_Entry;
wenzelm
parents: 65642
diff changeset
   617
              ml_statistics = ml_statistics.getOrElse(name, Nil).reverse)
64085
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   618
          (name -> entry)
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   619
        }):_*)
1c451e5c145f clarified parse_build_info: isabelle build output;
wenzelm
parents: 64083
diff changeset
   620
    Build_Info(sessions)
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64053
diff changeset
   621
  }
64099
wenzelm
parents: 64098
diff changeset
   622
wenzelm
parents: 64098
diff changeset
   623
wenzelm
parents: 64098
diff changeset
   624
65276
fa1a5efee2ec tuned comments;
wenzelm
parents: 65052
diff changeset
   625
  /** session info: produced by isabelle build as session log.gz file **/
64099
wenzelm
parents: 64098
diff changeset
   626
wenzelm
parents: 64098
diff changeset
   627
  sealed case class Session_Info(
wenzelm
parents: 64098
diff changeset
   628
    session_timing: Properties.T,
wenzelm
parents: 64098
diff changeset
   629
    command_timings: List[Properties.T],
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66863
diff changeset
   630
    theory_timings: List[Properties.T],
64099
wenzelm
parents: 64098
diff changeset
   631
    ml_statistics: List[Properties.T],
65934
5f202ba9f590 store errors in build db;
wenzelm
parents: 65857
diff changeset
   632
    task_statistics: List[Properties.T],
5f202ba9f590 store errors in build db;
wenzelm
parents: 65857
diff changeset
   633
    errors: List[String])
66944
05df740cb54b more informative timeout message, notably for build_status;
wenzelm
parents: 66913
diff changeset
   634
  {
05df740cb54b more informative timeout message, notably for build_status;
wenzelm
parents: 66913
diff changeset
   635
    def error(s: String): Session_Info =
05df740cb54b more informative timeout message, notably for build_status;
wenzelm
parents: 66913
diff changeset
   636
      copy(errors = errors ::: List(s))
05df740cb54b more informative timeout message, notably for build_status;
wenzelm
parents: 66913
diff changeset
   637
  }
64099
wenzelm
parents: 64098
diff changeset
   638
wenzelm
parents: 64098
diff changeset
   639
  private def parse_session_info(
wenzelm
parents: 64098
diff changeset
   640
    log_file: Log_File,
wenzelm
parents: 64098
diff changeset
   641
    command_timings: Boolean,
66873
9953ae603a23 provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents: 66863
diff changeset
   642
    theory_timings: Boolean,
64099
wenzelm
parents: 64098
diff changeset
   643
    ml_statistics: Boolean,
wenzelm
parents: 64098
diff changeset
   644
    task_statistics: Boolean): Session_Info =
wenzelm
parents: 64098
diff changeset
   645
  {
65290
wenzelm
parents: 65276
diff changeset
   646
    Session_Info(
71630
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   647
      session_timing = log_file.find_props(Protocol.Timing_Marker) getOrElse Nil,
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   648
      command_timings =
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   649
        if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil,
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   650
      theory_timings =
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   651
        if (theory_timings) log_file.filter_props(Protocol.Theory_Timing_Marker) else Nil,
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   652
      ml_statistics =
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   653
        if (ml_statistics) log_file.filter_props(Protocol.ML_Statistics_Marker) else Nil,
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   654
      task_statistics =
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   655
        if (task_statistics) log_file.filter_props(Protocol.Task_Statistics_Marker) else Nil,
50425e4c3910 clarified modules: global quasi-scope for markers;
wenzelm
parents: 71621
diff changeset
   656
      errors = log_file.filter(Protocol.Error_Message_Marker))
64099
wenzelm
parents: 64098
diff changeset
   657
  }
65595
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   658
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   659
  def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] =
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   660
    if (errors.isEmpty) None
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   661
    else {
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   662
      Some(Bytes(YXML.string_of_body(XML.Encode.list(XML.Encode.string)(errors))).
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   663
        compress(cache = cache))
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   664
    }
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   665
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   666
  def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] =
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   667
    if (bytes.isEmpty) Nil
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   668
    else {
71621
wenzelm
parents: 71620
diff changeset
   669
      XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text))
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   670
    }
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   671
65595
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   672
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   673
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   674
  /** persistent store **/
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   675
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   676
  /* SQL data model */
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   677
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   678
  object Data
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   679
  {
65702
7c6a91deb212 tuned signature;
wenzelm
parents: 65701
diff changeset
   680
    def build_log_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
65700
wenzelm
parents: 65699
diff changeset
   681
      SQL.Table("isabelle_build_log_" + name, columns, body)
wenzelm
parents: 65699
diff changeset
   682
wenzelm
parents: 65699
diff changeset
   683
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   684
    /* main content */
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   685
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66856
diff changeset
   686
    val log_name = SQL.Column.string("log_name").make_primary_key
f8f42289c4df tuned signature;
wenzelm
parents: 66856
diff changeset
   687
    val session_name = SQL.Column.string("session_name").make_primary_key
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   688
    val theory_name = SQL.Column.string("theory_name").make_primary_key
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   689
    val chapter = SQL.Column.string("chapter")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   690
    val groups = SQL.Column.string("groups")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   691
    val threads = SQL.Column.int("threads")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   692
    val timing_elapsed = SQL.Column.long("timing_elapsed")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   693
    val timing_cpu = SQL.Column.long("timing_cpu")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   694
    val timing_gc = SQL.Column.long("timing_gc")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   695
    val timing_factor = SQL.Column.double("timing_factor")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   696
    val ml_timing_elapsed = SQL.Column.long("ml_timing_elapsed")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   697
    val ml_timing_cpu = SQL.Column.long("ml_timing_cpu")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   698
    val ml_timing_gc = SQL.Column.long("ml_timing_gc")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   699
    val ml_timing_factor = SQL.Column.double("ml_timing_factor")
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   700
    val theory_timing_elapsed = SQL.Column.long("theory_timing_elapsed")
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   701
    val theory_timing_cpu = SQL.Column.long("theory_timing_cpu")
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   702
    val theory_timing_gc = SQL.Column.long("theory_timing_gc")
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   703
    val heap_size = SQL.Column.long("heap_size")
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   704
    val status = SQL.Column.string("status")
65937
fde7b5d209d5 store errors in build_history logs and database;
wenzelm
parents: 65934
diff changeset
   705
    val errors = SQL.Column.bytes("errors")
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   706
    val sources = SQL.Column.string("sources")
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   707
    val ml_statistics = SQL.Column.bytes("ml_statistics")
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   708
    val known = SQL.Column.bool("known")
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   709
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   710
    val meta_info_table =
65702
7c6a91deb212 tuned signature;
wenzelm
parents: 65701
diff changeset
   711
      build_log_table("meta_info", log_name :: Prop.all_props ::: Settings.all_settings)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   712
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   713
    val sessions_table =
65702
7c6a91deb212 tuned signature;
wenzelm
parents: 65701
diff changeset
   714
      build_log_table("sessions",
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   715
        List(log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu,
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   716
          timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
   717
          heap_size, status, errors, sources))
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   718
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   719
    val theories_table =
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   720
      build_log_table("theories",
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   721
        List(log_name, session_name, theory_name, theory_timing_elapsed, theory_timing_cpu,
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   722
          theory_timing_gc))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   723
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   724
    val ml_statistics_table =
65702
7c6a91deb212 tuned signature;
wenzelm
parents: 65701
diff changeset
   725
      build_log_table("ml_statistics", List(log_name, session_name, ml_statistics))
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   726
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   727
66855
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   728
    /* AFP versions */
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   729
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   730
    val isabelle_afp_versions_table: SQL.Table =
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   731
    {
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   732
      val version1 = Prop.isabelle_version
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   733
      val version2 = Prop.afp_version
66857
f8f42289c4df tuned signature;
wenzelm
parents: 66856
diff changeset
   734
      build_log_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
66855
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   735
        SQL.select(List(version1, version2), distinct = true) + meta_info_table +
66856
6b90c688a6dc tuned signature;
wenzelm
parents: 66855
diff changeset
   736
        " WHERE " + version1.defined + " AND " + version2.defined)
66855
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   737
    }
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   738
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   739
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   740
    /* earliest pull date for repository version (PostgreSQL queries) */
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   741
71621
wenzelm
parents: 71620
diff changeset
   742
    def pull_date(afp: Boolean = false): SQL.Column =
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   743
      if (afp) SQL.Column.date("afp_pull_date")
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   744
      else SQL.Column.date("pull_date")
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   745
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   746
    def pull_date_table(afp: Boolean = false): SQL.Table =
65709
1626b73daccf eliminated unused afp_pull_date table;
wenzelm
parents: 65708
diff changeset
   747
    {
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   748
      val (name, versions) =
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   749
        if (afp) ("afp_pull_date", List(Prop.isabelle_version, Prop.afp_version))
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   750
        else ("pull_date", List(Prop.isabelle_version))
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   751
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   752
      build_log_table(name, versions.map(_.make_primary_key) ::: List(pull_date(afp)),
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   753
        "SELECT " + versions.mkString(", ") +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   754
          ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   755
        " FROM " + meta_info_table +
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   756
        " WHERE " + (versions ::: List(Prop.build_start)).map(_.defined).mkString(" AND ") +
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   757
        " GROUP BY " + versions.mkString(", "))
66855
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   758
    }
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   759
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   760
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   761
    /* recent entries */
c9d413fca1ec support for AFP versions;
wenzelm
parents: 66046
diff changeset
   762
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65729
diff changeset
   763
    def recent_time(days: Int): SQL.Source =
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65729
diff changeset
   764
      "now() - INTERVAL '" + days.max(0) + " days'"
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65729
diff changeset
   765
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   766
    def recent_pull_date_table(
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   767
      days: Int, rev: String = "", afp_rev: Option[String] = None): SQL.Table =
65702
7c6a91deb212 tuned signature;
wenzelm
parents: 65701
diff changeset
   768
    {
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   769
      val afp = afp_rev.isDefined
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   770
      val rev2 = afp_rev.getOrElse("")
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   771
      val table = pull_date_table(afp)
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   772
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   773
      val version1 = Prop.isabelle_version
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   774
      val version2 = Prop.afp_version
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   775
      val eq1 = version1(table) + " = " + SQL.string(rev)
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   776
      val eq2 = version2(table) + " = " + SQL.string(rev2)
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   777
65777
821e77ce41be tuned signature;
wenzelm
parents: 65775
diff changeset
   778
      SQL.Table("recent_pull_date", table.columns,
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   779
        table.select(table.columns,
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   780
          "WHERE " + pull_date(afp)(table) + " > " + recent_time(days) +
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   781
          (if (rev != "" && rev2 == "") " OR " + eq1
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   782
           else if (rev == "" && rev2 != "") " OR " + eq2
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   783
           else if (rev != "" && rev2 != "") " OR (" + eq1 + " AND " + eq2 + ")"
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   784
           else "")))
65702
7c6a91deb212 tuned signature;
wenzelm
parents: 65701
diff changeset
   785
    }
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   786
65781
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   787
    def select_recent_log_names(days: Int): SQL.Source =
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   788
    {
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   789
      val table1 = meta_info_table
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   790
      val table2 = recent_pull_date_table(days)
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   791
      table1.select(List(log_name), distinct = true) + SQL.join_inner + table2.query_named +
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   792
        " ON " + Prop.isabelle_version(table1) + " = " + Prop.isabelle_version(table2)
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   793
    }
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   794
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   795
    def select_recent_versions(days: Int,
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   796
      rev: String = "", afp_rev: Option[String] = None, sql: SQL.Source = ""): SQL.Source =
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   797
    {
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   798
      val afp = afp_rev.isDefined
66858
2ca6f0275de7 support for AFP versions;
wenzelm
parents: 66857
diff changeset
   799
      val version = Prop.isabelle_version
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   800
      val table1 = recent_pull_date_table(days, rev = rev, afp_rev = afp_rev)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   801
      val table2 = meta_info_table
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   802
      val aux_table = SQL.Table("aux", table2.columns, table2.select(sql = sql))
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   803
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   804
      val columns =
66858
2ca6f0275de7 support for AFP versions;
wenzelm
parents: 66857
diff changeset
   805
        table1.columns.map(c => c(table1)) :::
2ca6f0275de7 support for AFP versions;
wenzelm
parents: 66857
diff changeset
   806
          List(known.copy(expr = log_name(aux_table).defined))
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   807
      SQL.select(columns, distinct = true) +
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   808
        table1.query_named + SQL.join_outer + aux_table.query_named +
66858
2ca6f0275de7 support for AFP versions;
wenzelm
parents: 66857
diff changeset
   809
        " ON " + version(table1) + " = " + version(aux_table) +
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   810
        " ORDER BY " + pull_date(afp)(table1) + " DESC"
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   811
    }
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65781
diff changeset
   812
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   813
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   814
    /* universal view on main data */
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   815
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   816
    val universal_table: SQL.Table =
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   817
    {
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   818
      val afp_pull_date = pull_date(afp = true)
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   819
      val version1 = Prop.isabelle_version
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   820
      val version2 = Prop.afp_version
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   821
      val table1 = meta_info_table
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   822
      val table2 = pull_date_table(afp = true)
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   823
      val table3 = pull_date_table()
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   824
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   825
      val a_columns = log_name :: afp_pull_date :: table1.columns.tail
65850
5414c14c3984 clarified universal table: include ml_statistics;
wenzelm
parents: 65804
diff changeset
   826
      val a_table =
5414c14c3984 clarified universal table: include ml_statistics;
wenzelm
parents: 65804
diff changeset
   827
        SQL.Table("a", a_columns,
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   828
          SQL.select(List(log_name, afp_pull_date) ::: table1.columns.tail.map(_.apply(table1))) +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   829
          table1 + SQL.join_outer + table2 +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   830
          " ON " + version1(table1) + " = " + version1(table2) +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   831
          " AND " + version2(table1) + " = " + version2(table2))
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   832
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   833
      val b_columns = log_name :: pull_date() :: a_columns.tail
65850
5414c14c3984 clarified universal table: include ml_statistics;
wenzelm
parents: 65804
diff changeset
   834
      val b_table =
5414c14c3984 clarified universal table: include ml_statistics;
wenzelm
parents: 65804
diff changeset
   835
        SQL.Table("b", b_columns,
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   836
          SQL.select(
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   837
            List(log_name(a_table), pull_date()(table3)) ::: a_columns.tail.map(_.apply(a_table))) +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   838
          a_table.query_named + SQL.join_outer + table3 +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   839
          " ON " + version1(a_table) + " = " + version1(table3))
65850
5414c14c3984 clarified universal table: include ml_statistics;
wenzelm
parents: 65804
diff changeset
   840
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   841
      val c_columns = b_columns ::: sessions_table.columns.tail
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   842
      val c_table =
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   843
        SQL.Table("c", c_columns,
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   844
          SQL.select(log_name(b_table) :: c_columns.tail) +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   845
          b_table.query_named + SQL.join_inner + sessions_table +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   846
          " ON " + log_name(b_table) + " = " + log_name(sessions_table))
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   847
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   848
      SQL.Table("isabelle_build_log", c_columns ::: List(ml_statistics),
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   849
        {
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   850
          SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   851
          c_table.query_named + SQL.join_outer + ml_statistics_table +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   852
          " ON " + log_name(c_table) + " = " + log_name(ml_statistics_table) +
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   853
          " AND " + session_name(c_table) + " = " + session_name(ml_statistics_table)
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   854
        })
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   855
    }
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   856
  }
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   857
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   858
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   859
  /* database access */
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   860
65595
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   861
  def store(options: Options): Store = new Store(options)
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   862
65857
5d29d93766ef clarified use of XML.Cache;
wenzelm
parents: 65856
diff changeset
   863
  class Store private[Build_Log](options: Options)
65595
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   864
  {
68169
395432e7516e tuned signature;
wenzelm
parents: 68018
diff changeset
   865
    val xml_cache: XML.Cache = XML.make_cache()
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
   866
    val xz_cache: XZ.Cache = XZ.make_cache()
65857
5d29d93766ef clarified use of XML.Cache;
wenzelm
parents: 65856
diff changeset
   867
65595
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   868
    def open_database(
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   869
      user: String = options.string("build_log_database_user"),
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   870
      password: String = options.string("build_log_database_password"),
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   871
      database: String = options.string("build_log_database_name"),
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   872
      host: String = options.string("build_log_database_host"),
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   873
      port: Int = options.int("build_log_database_port"),
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   874
      ssh_host: String = options.string("build_log_ssh_host"),
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   875
      ssh_user: String = options.string("build_log_ssh_user"),
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   876
      ssh_port: Int = options.int("build_log_ssh_port")): PostgreSQL.Database =
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   877
    {
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   878
      PostgreSQL.open_database(
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   879
        user = user, password = password, database = database, host = host, port = port,
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   880
        ssh =
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   881
          if (ssh_host == "") None
67067
02729ced9b1e tuned signature;
wenzelm
parents: 67007
diff changeset
   882
          else Some(SSH.open_session(options, host = ssh_host, user = ssh_user, port = port)),
65636
df804cdba5f9 ssh_close for proper termination after use of database;
wenzelm
parents: 65633
diff changeset
   883
        ssh_close = true)
65595
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
   884
    }
65599
08dfa79866ec database storage of Meta_Info and Build_Info;
wenzelm
parents: 65595
diff changeset
   885
65723
3ee466e89047 clarified signature: PostgreSQL manages high-volume data, SQLite only sees small snapshots;
wenzelm
parents: 65722
diff changeset
   886
    def update_database(db: PostgreSQL.Database, dirs: List[Path], ml_statistics: Boolean = false)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   887
    {
69299
2fd070377c99 clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
wenzelm
parents: 68169
diff changeset
   888
      val log_files =
2fd070377c99 clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
wenzelm
parents: 68169
diff changeset
   889
        dirs.flatMap(dir =>
2fd070377c99 clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
wenzelm
parents: 68169
diff changeset
   890
          File.find_files(dir.file, pred = Log_File.is_log(_), follow_links = true))
2fd070377c99 clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
wenzelm
parents: 68169
diff changeset
   891
      write_info(db, log_files, ml_statistics = ml_statistics)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   892
66863
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   893
      db.create_view(Data.pull_date_table())
6acd1a2bd146 clarified afp_pull_date: both repository versions are relevant;
wenzelm
parents: 66858
diff changeset
   894
      db.create_view(Data.pull_date_table(afp = true))
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   895
      db.create_view(Data.universal_table)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   896
    }
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   897
65723
3ee466e89047 clarified signature: PostgreSQL manages high-volume data, SQLite only sees small snapshots;
wenzelm
parents: 65722
diff changeset
   898
    def snapshot_database(db: PostgreSQL.Database, sqlite_database: Path,
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   899
      days: Int = 100, ml_statistics: Boolean = false)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   900
    {
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   901
      Isabelle_System.mkdirs(sqlite_database.dir)
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   902
      sqlite_database.file.delete
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   903
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   904
      using(SQLite.open_database(sqlite_database))(db2 =>
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   905
      {
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   906
        db.transaction {
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   907
          db2.transaction {
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   908
            // main content
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   909
            db2.create_table(Data.meta_info_table)
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   910
            db2.create_table(Data.sessions_table)
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   911
            db2.create_table(Data.theories_table)
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   912
            db2.create_table(Data.ml_statistics_table)
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   913
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   914
            val recent_log_names =
65781
6cd11999f3a3 tuned (again);
wenzelm
parents: 65779
diff changeset
   915
              db.using_statement(Data.select_recent_log_names(days))(stmt =>
65779
a42c9e375405 tuned -- inlined single use;
wenzelm
parents: 65778
diff changeset
   916
                stmt.execute_query().iterator(_.string(Data.log_name)).toList)
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   917
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   918
            for (log_name <- recent_log_names) {
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   919
              read_meta_info(db, log_name).foreach(meta_info =>
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   920
                update_meta_info(db2, log_name, meta_info))
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   921
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   922
              update_sessions(db2, log_name, read_build_info(db, log_name))
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   923
65856
69f4dacd31cf proper ml_statistics;
wenzelm
parents: 65853
diff changeset
   924
              if (ml_statistics) {
69f4dacd31cf proper ml_statistics;
wenzelm
parents: 65853
diff changeset
   925
                update_ml_statistics(db2, log_name,
69f4dacd31cf proper ml_statistics;
wenzelm
parents: 65853
diff changeset
   926
                  read_build_info(db, log_name, ml_statistics = true))
69f4dacd31cf proper ml_statistics;
wenzelm
parents: 65853
diff changeset
   927
              }
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   928
            }
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   929
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   930
            // pull_date
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   931
            for (afp <- List(false, true))
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   932
            {
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   933
              val afp_rev = if (afp) Some("") else None
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   934
              val table = Data.pull_date_table(afp)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   935
              db2.create_table(table)
65698
38139b2067cf clarified signature;
wenzelm
parents: 65697
diff changeset
   936
              db2.using_statement(table.insert())(stmt2 =>
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   937
              {
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   938
                db.using_statement(
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66874
diff changeset
   939
                  Data.recent_pull_date_table(days, afp_rev = afp_rev).query)(stmt =>
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   940
                {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
   941
                  val res = stmt.execute_query()
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
   942
                  while (res.next()) {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   943
                    for ((c, i) <- table.columns.zipWithIndex) {
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   944
                      stmt2.string(i + 1) = res.get_string(c)
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   945
                    }
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
   946
                    stmt2.execute()
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   947
                  }
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   948
                })
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   949
              })
65709
1626b73daccf eliminated unused afp_pull_date table;
wenzelm
parents: 65708
diff changeset
   950
            }
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   951
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   952
            // full view
65724
681cdf83ce09 clarified universal view: include pull_date;
wenzelm
parents: 65723
diff changeset
   953
            db2.create_view(Data.universal_table)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   954
          }
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   955
        }
65708
50a61990c01e slightly more compact file;
wenzelm
parents: 65706
diff changeset
   956
        db2.rebuild
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   957
      })
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   958
    }
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   959
65688
wenzelm
parents: 65685
diff changeset
   960
    def domain(db: SQL.Database, table: SQL.Table, column: SQL.Column): Set[String] =
65698
38139b2067cf clarified signature;
wenzelm
parents: 65697
diff changeset
   961
      db.using_statement(table.select(List(column), distinct = true))(stmt =>
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
   962
        stmt.execute_query().iterator(_.string(column)).toSet)
65688
wenzelm
parents: 65685
diff changeset
   963
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   964
    def update_meta_info(db: SQL.Database, log_name: String, meta_info: Meta_Info)
65632
218dbe4fb484 tuned signature;
wenzelm
parents: 65631
diff changeset
   965
    {
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   966
      val table = Data.meta_info_table
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   967
      db.using_statement(db.insert_permissive(table))(stmt =>
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   968
      {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   969
        stmt.string(1) = log_name
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   970
        for ((c, i) <- table.columns.tail.zipWithIndex) {
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   971
          if (c.T == SQL.Type.Date)
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   972
            stmt.date(i + 2) = meta_info.get_date(c)
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   973
          else
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   974
            stmt.string(i + 2) = meta_info.get(c)
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   975
        }
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   976
        stmt.execute()
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   977
      })
65600
138ffa41dc54 clarified filter_files: sorted and unique;
wenzelm
parents: 65599
diff changeset
   978
    }
138ffa41dc54 clarified filter_files: sorted and unique;
wenzelm
parents: 65599
diff changeset
   979
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
   980
    def update_sessions(db: SQL.Database, log_name: String, build_info: Build_Info)
65599
08dfa79866ec database storage of Meta_Info and Build_Info;
wenzelm
parents: 65595
diff changeset
   981
    {
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
   982
      val table = Data.sessions_table
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   983
      db.using_statement(db.insert_permissive(table))(stmt =>
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
   984
      {
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   985
        val sessions =
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   986
          if (build_info.sessions.isEmpty) Build_Info.sessions_dummy
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   987
          else build_info.sessions
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
   988
        for ((session_name, session) <- sessions) {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   989
          stmt.string(1) = log_name
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   990
          stmt.string(2) = session_name
65853
wenzelm
parents: 65852
diff changeset
   991
          stmt.string(3) = proper_string(session.chapter)
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   992
          stmt.string(4) = session.proper_groups
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   993
          stmt.int(5) = session.threads
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   994
          stmt.long(6) = session.timing.elapsed.proper_ms
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   995
          stmt.long(7) = session.timing.cpu.proper_ms
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   996
          stmt.long(8) = session.timing.gc.proper_ms
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   997
          stmt.double(9) = session.timing.factor
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   998
          stmt.long(10) = session.ml_timing.elapsed.proper_ms
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
   999
          stmt.long(11) = session.ml_timing.cpu.proper_ms
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
  1000
          stmt.long(12) = session.ml_timing.gc.proper_ms
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
  1001
          stmt.double(13) = session.ml_timing.factor
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
  1002
          stmt.long(14) = session.heap_size
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
  1003
          stmt.string(15) = session.status.map(_.toString)
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
  1004
          stmt.bytes(16) = compress_errors(session.errors, cache = xz_cache)
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
  1005
          stmt.string(17) = session.sources
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1006
          stmt.execute()
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1007
        }
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1008
      })
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1009
    }
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1010
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1011
    def update_theories(db: SQL.Database, log_name: String, build_info: Build_Info)
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1012
    {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1013
      val table = Data.theories_table
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1014
      db.using_statement(db.insert_permissive(table))(stmt =>
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1015
      {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1016
        val sessions =
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1017
          if (build_info.sessions.forall({ case (_, session) => session.theory_timings.isEmpty }))
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1018
            Build_Info.sessions_dummy
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1019
          else build_info.sessions
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1020
        for {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1021
          (session_name, session) <- sessions
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1022
          (theory_name, timing) <- session.theory_timings
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1023
        } {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1024
          stmt.string(1) = log_name
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1025
          stmt.string(2) = session_name
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1026
          stmt.string(3) = theory_name
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1027
          stmt.long(4) = timing.elapsed.ms
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1028
          stmt.long(5) = timing.cpu.ms
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1029
          stmt.long(6) = timing.gc.ms
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1030
          stmt.execute()
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1031
        }
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1032
      })
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1033
    }
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1034
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1035
    def update_ml_statistics(db: SQL.Database, log_name: String, build_info: Build_Info)
65645
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1036
    {
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
  1037
      val table = Data.ml_statistics_table
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1038
      db.using_statement(db.insert_permissive(table))(stmt =>
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1039
      {
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1040
        val ml_stats: List[(String, Option[Bytes])] =
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1041
          Par_List.map[(String, Session_Entry), (String, Option[Bytes])](
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
  1042
            { case (a, b) => (a, Properties.compress(b.ml_statistics, cache = xz_cache).proper) },
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1043
            build_info.sessions.iterator.filter(p => p._2.ml_statistics.nonEmpty).toList)
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1044
        val entries = if (ml_stats.nonEmpty) ml_stats else List("" -> None)
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1045
        for ((session_name, ml_statistics) <- entries) {
65748
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
  1046
          stmt.string(1) = log_name
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
  1047
          stmt.string(2) = session_name
1f4a80e80c88 tuned signature;
wenzelm
parents: 65741
diff changeset
  1048
          stmt.bytes(3) = ml_statistics
65703
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1049
          stmt.execute()
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1050
        }
cead65c19f2e more direct insert_permissive statement, which avoids somewhat fragile nested transactions;
wenzelm
parents: 65702
diff changeset
  1051
      })
65645
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1052
    }
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1053
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1054
    def write_info(db: SQL.Database, files: List[JFile], ml_statistics: Boolean = false)
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1055
    {
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1056
      abstract class Table_Status(table: SQL.Table)
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1057
      {
65688
wenzelm
parents: 65685
diff changeset
  1058
        db.create_table(table)
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
  1059
        private var known: Set[String] = domain(db, table, Data.log_name)
65688
wenzelm
parents: 65685
diff changeset
  1060
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1061
        def required(file: JFile): Boolean = !known(Log_File.plain_name(file.getName))
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1062
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1063
        def update_db(db: SQL.Database, log_file: Log_File): Unit
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1064
        def update(log_file: Log_File)
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1065
        {
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1066
          if (!known(log_file.name)) {
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1067
            update_db(db, log_file)
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1068
            known += log_file.name
65618
986fac3c60b4 tuned transaction granularity;
wenzelm
parents: 65616
diff changeset
  1069
          }
65614
325801edb37d clarified transaction boundaries: more robust incremental write operations;
wenzelm
parents: 65613
diff changeset
  1070
        }
65605
a6447eb6bc38 separate small meta_info vs. big build_info;
wenzelm
parents: 65603
diff changeset
  1071
      }
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1072
      val status =
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1073
        List(
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1074
          new Table_Status(Data.meta_info_table) {
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1075
            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1076
              update_meta_info(db, log_file.name, log_file.parse_meta_info())
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1077
          },
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1078
          new Table_Status(Data.sessions_table) {
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1079
            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1080
              update_sessions(db, log_file.name, log_file.parse_build_info())
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1081
          },
66874
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1082
          new Table_Status(Data.theories_table) {
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1083
            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1084
              update_theories(db, log_file.name, log_file.parse_build_info())
0b8da0fc9563 store theory timings in session in build_log database;
wenzelm
parents: 66873
diff changeset
  1085
          },
65705
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1086
          new Table_Status(Data.ml_statistics_table) {
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1087
            override def update_db(db: SQL.Database, log_file: Log_File): Unit =
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1088
            if (ml_statistics) {
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1089
              update_ml_statistics(db, log_file.name,
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1090
                log_file.parse_build_info(ml_statistics = true))
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1091
            }
d0ca2a3ea657 more snapshot content;
wenzelm
parents: 65703
diff changeset
  1092
          })
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1093
67743
7bd0a250183b avoid hardwired parameters;
wenzelm
parents: 67067
diff changeset
  1094
      for (file_group <-
7bd0a250183b avoid hardwired parameters;
wenzelm
parents: 67067
diff changeset
  1095
            files.filter(file => status.exists(_.required(file))).
7bd0a250183b avoid hardwired parameters;
wenzelm
parents: 67067
diff changeset
  1096
              grouped(options.int("build_log_transaction_size") max 1))
7bd0a250183b avoid hardwired parameters;
wenzelm
parents: 67067
diff changeset
  1097
      {
71621
wenzelm
parents: 71620
diff changeset
  1098
        val log_files = Par_List.map[JFile, Log_File](Log_File.apply, file_group)
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1099
        db.transaction { log_files.foreach(log_file => status.foreach(_.update(log_file))) }
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1100
      }
65605
a6447eb6bc38 separate small meta_info vs. big build_info;
wenzelm
parents: 65603
diff changeset
  1101
    }
a6447eb6bc38 separate small meta_info vs. big build_info;
wenzelm
parents: 65603
diff changeset
  1102
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1103
    def read_meta_info(db: SQL.Database, log_name: String): Option[Meta_Info] =
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1104
    {
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
  1105
      val table = Data.meta_info_table
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1106
      val columns = table.columns.tail
65699
9f74d9aa0bdf tuned signature;
wenzelm
parents: 65698
diff changeset
  1107
      db.using_statement(table.select(columns, Data.log_name.where_equal(log_name)))(stmt =>
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1108
      {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1109
        val res = stmt.execute_query()
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1110
        if (!res.next) None
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1111
        else {
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1112
          val results =
65642
1423cbbc542d clarified database update operations;
wenzelm
parents: 65639
diff changeset
  1113
            columns.map(c => c.name ->
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1114
              (if (c.T == SQL.Type.Date)
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1115
                res.get_date(c).map(Log_File.Date_Format(_))
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1116
               else
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1117
                res.get_string(c)))
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1118
          val n = Prop.all_props.length
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1119
          val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1120
          val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1121
          Some(Meta_Info(props, settings))
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1122
        }
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1123
      })
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1124
    }
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1125
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1126
    def read_build_info(
65629
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1127
      db: SQL.Database,
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1128
      log_name: String,
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1129
      session_names: List[String] = Nil,
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1130
      ml_statistics: Boolean = false): Build_Info =
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1131
    {
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
  1132
      val table1 = Data.sessions_table
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
  1133
      val table2 = Data.ml_statistics_table
65629
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1134
65645
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1135
      val where_log_name =
65699
9f74d9aa0bdf tuned signature;
wenzelm
parents: 65698
diff changeset
  1136
        Data.log_name(table1).where_equal(log_name) + " AND " +
65701
d788c11176e5 simplified: standard toString is SQL.ident;
wenzelm
parents: 65700
diff changeset
  1137
        Data.session_name(table1) + " <> ''"
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1138
      val where =
65645
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1139
        if (session_names.isEmpty) where_log_name
65804
wenzelm
parents: 65783
diff changeset
  1140
        else where_log_name + " AND " + SQL.member(Data.session_name(table1).ident, session_names)
65629
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1141
65645
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1142
      val columns1 = table1.columns.tail.map(_.apply(table1))
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1143
      val (columns, from) =
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1144
        if (ml_statistics) {
65694
b82f2990161a clarified modules;
wenzelm
parents: 65693
diff changeset
  1145
          val columns = columns1 ::: List(Data.ml_statistics(table2))
65668
366bc4e6a238 more operations;
wenzelm
parents: 65665
diff changeset
  1146
          val join =
65775
123f2c0995b8 tuned signature;
wenzelm
parents: 65748
diff changeset
  1147
            table1 + SQL.join_outer + table2 + " ON " +
65738
wenzelm
parents: 65736
diff changeset
  1148
            Data.log_name(table1) + " = " + Data.log_name(table2) + " AND " +
wenzelm
parents: 65736
diff changeset
  1149
            Data.session_name(table1) + " = " + Data.session_name(table2)
65668
366bc4e6a238 more operations;
wenzelm
parents: 65665
diff changeset
  1150
          (columns, SQL.enclose(join))
65645
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1151
        }
65695
4edac706bc5e tuned signature;
wenzelm
parents: 65694
diff changeset
  1152
        else (columns1, table1.ident)
65645
2c704ae04db1 clarified database layout: bulky ml_statistics are stored/retrieved separately;
wenzelm
parents: 65643
diff changeset
  1153
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1154
      val sessions =
65698
38139b2067cf clarified signature;
wenzelm
parents: 65697
diff changeset
  1155
        db.using_statement(SQL.select(columns) + from + " " + where)(stmt =>
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1156
        {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1157
          stmt.execute_query().iterator(res =>
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1158
          {
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1159
            val session_name = res.string(Data.session_name)
65626
wenzelm
parents: 65625
diff changeset
  1160
            val session_entry =
wenzelm
parents: 65625
diff changeset
  1161
              Session_Entry(
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1162
                chapter = res.string(Data.chapter),
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1163
                groups = split_lines(res.string(Data.groups)),
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1164
                threads = res.get_int(Data.threads),
65741
wenzelm
parents: 65740
diff changeset
  1165
                timing = res.timing(Data.timing_elapsed, Data.timing_cpu, Data.timing_gc),
65626
wenzelm
parents: 65625
diff changeset
  1166
                ml_timing =
65741
wenzelm
parents: 65740
diff changeset
  1167
                  res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc),
66913
7cdd4d59e95c store session sources stamp;
wenzelm
parents: 66880
diff changeset
  1168
                sources = res.get_string(Data.sources),
65740
83388f09e9ab clarified signature;
wenzelm
parents: 65738
diff changeset
  1169
                heap_size = res.get_long(Data.heap_size),
71621
wenzelm
parents: 71620
diff changeset
  1170
                status = res.get_string(Data.status).map(Session_Status.withName),
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
  1171
                errors = uncompress_errors(res.bytes(Data.errors), cache = xz_cache),
65629
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1172
                ml_statistics =
68018
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
  1173
                  if (ml_statistics) {
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
  1174
                    Properties.uncompress(
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
  1175
                      res.bytes(Data.ml_statistics), cache = xz_cache, Some(xml_cache))
3747fe57eb67 support for XZ.Cache;
wenzelm
parents: 67743
diff changeset
  1176
                  }
65629
e6c0afe672fa optional ml_statistics: much faster;
wenzelm
parents: 65628
diff changeset
  1177
                  else Nil)
65626
wenzelm
parents: 65625
diff changeset
  1178
            session_name -> session_entry
65621
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1179
          }).toMap
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1180
        })
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1181
      Build_Info(sessions)
551950dccec6 operations to read database;
wenzelm
parents: 65619
diff changeset
  1182
    }
65595
ffd8283b7be0 support for database connection;
wenzelm
parents: 65591
diff changeset
  1183
  }
64045
c6160d0b0337 clarified modules;
wenzelm
parents:
diff changeset
  1184
}