src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Sat, 25 Jul 2020 23:23:59 +0200
changeset 72304 f3e1144a1cec
parent 72303 f56522a44564
child 72550 d24a8cea343b
permissions -rw-r--r--
clarified name to avoid duplication (no distinction of data on host = lrzcloud2);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Admin/isabelle_cronjob.scala
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     3
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     4
Main entry point for administrative cronjob at TUM.
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     5
*/
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     6
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     7
package isabelle
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     8
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
     9
67854
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    10
import java.nio.file.Files
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    11
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    12
import scala.annotation.tailrec
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    13
import scala.collection.mutable
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    14
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    15
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
    16
object Isabelle_Cronjob
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
    17
{
66897
wenzelm
parents: 66896
diff changeset
    18
  /* global resources: owned by main cronjob */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    19
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    20
  val backup = "lxbroy10:cronjob"
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    21
  val main_dir: Path = Path.explode("~/cronjob")
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    22
  val main_state_file: Path = main_dir + Path.explode("run/main.state")
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    23
  val current_log: Path = main_dir + Path.explode("run/main.log")  // owned by log service
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    24
  val cumulative_log: Path = main_dir + Path.explode("log/main.log")  // owned by log service
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    25
68651
7538b5f301ea evade odd connection problems to https://isabelle.in.tum.de from some remote hosts;
wenzelm
parents: 68531
diff changeset
    26
  val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle"
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    27
  val isabelle_repos: Path = main_dir + Path.explode("isabelle")
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    28
  val afp_repos: Path = main_dir + Path.explode("AFP")
64236
358f9ff08681 discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
wenzelm
parents: 64235
diff changeset
    29
66896
85e6748bf8b2 clarified signature;
wenzelm
parents: 66895
diff changeset
    30
  val build_log_dirs =
85e6748bf8b2 clarified signature;
wenzelm
parents: 66895
diff changeset
    31
    List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
85e6748bf8b2 clarified signature;
wenzelm
parents: 66895
diff changeset
    32
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    33
64192
wenzelm
parents: 64187
diff changeset
    34
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    35
  /** logger tasks **/
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    36
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    37
  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
    38
64192
wenzelm
parents: 64187
diff changeset
    39
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    40
  /* init and exit */
64192
wenzelm
parents: 64187
diff changeset
    41
67753
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    42
  def get_rev(): String = Mercurial.repository(isabelle_repos).id()
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    43
  def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    44
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    45
  val init: Logger_Task =
67751
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    46
    Logger_Task("init", logger =>
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    47
      {
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    48
        Isabelle_Devel.make_index()
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    49
67753
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    50
        Mercurial.setup_repository(isabelle_repos_source, isabelle_repos)
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    51
        Mercurial.setup_repository(AFP.repos_source, afp_repos)
64192
wenzelm
parents: 64187
diff changeset
    52
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    53
        File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
67753
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
    54
          Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    55
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    56
        Isabelle_System.bash(
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    57
          """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ +
69202
e5e4de2b93d9 more robust: allow log to be a symlink;
wenzelm
parents: 68651
diff changeset
    58
            Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
67854
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    59
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    60
        if (!Isabelle_Devel.cronjob_log.is_file)
8374c80165e1 publish current log file, e.g. for easy error detection;
wenzelm
parents: 67775
diff changeset
    61
          Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    62
      })
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    63
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    64
  val exit: Logger_Task =
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    65
    Logger_Task("exit", logger =>
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    66
      {
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
    67
        Isabelle_System.bash(
69202
e5e4de2b93d9 more robust: allow log to be a symlink;
wenzelm
parents: 68651
diff changeset
    68
          "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
67769
20c262dcfdf5 proper target directory;
wenzelm
parents: 67766
diff changeset
    69
            .check
67751
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    70
      })
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    71
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    72
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    73
  /* build release */
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    74
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    75
  val build_release: Logger_Task =
67751
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    76
    Logger_Task("build_release", logger =>
361d41701de0 clarified tasks;
wenzelm
parents: 67750
diff changeset
    77
      {
69442
d072f3287ffa discontinued somewhat point dmg: plain .tar.gz is smaller and more convenient to install;
wenzelm
parents: 69411
diff changeset
    78
        Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    79
      })
64192
wenzelm
parents: 64187
diff changeset
    80
wenzelm
parents: 64187
diff changeset
    81
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    82
  /* integrity test of build_history vs. build_history_base */
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    83
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
    84
  val build_history_base: Logger_Task =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    85
    Logger_Task("build_history_base", logger =>
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    86
      {
67774
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    87
        using(logger.ssh_context.open_session("lxbroy10"))(ssh =>
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    88
          {
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    89
            val results =
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    90
              Build_History.remote_build_history(ssh,
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    91
                isabelle_repos,
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    92
                isabelle_repos.ext("build_history_base"),
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    93
                isabelle_identifier = "cronjob_build_history",
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    94
                self_update = true,
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    95
                rev = "build_history_base",
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    96
                options = "-f",
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    97
                args = "HOL")
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    98
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
    99
            for ((log_name, bytes) <- results) {
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
   100
              Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
   101
            }
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
   102
          })
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   103
      })
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   104
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   105
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   106
  /* remote build_history */
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   107
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   108
  sealed case class Item(
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   109
    known: Boolean,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   110
    isabelle_version: String,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   111
    afp_version: Option[String],
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   112
    pull_date: Date)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   113
  {
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   114
    def unknown: Boolean = !known
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   115
    def versions: (String, Option[String]) = (isabelle_version, afp_version)
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   116
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   117
    def known_versions(rev: String, afp_rev: Option[String]): Boolean =
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   118
      known && rev != "" && isabelle_version == rev &&
71589
5965e6e3c3ec proper comparison of Option values, following hint by IntelliJ;
wenzelm
parents: 70947
diff changeset
   119
      (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   120
  }
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   121
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   122
  def recent_items(db: SQL.Database,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   123
    days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
65807
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   124
  {
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66879
diff changeset
   125
    val afp = afp_rev.isDefined
65807
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   126
    val select =
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   127
      Build_Log.Data.select_recent_versions(
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   128
        days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
65807
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   129
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   130
    db.using_statement(select)(stmt =>
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   131
      stmt.execute_query().iterator(res =>
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   132
      {
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   133
        val known = res.bool(Build_Log.Data.known)
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   134
        val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66879
diff changeset
   135
        val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66879
diff changeset
   136
        val pull_date = res.date(Build_Log.Data.pull_date(afp))
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   137
        Item(known, isabelle_version, afp_version, pull_date)
65807
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   138
      }).toList)
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   139
  }
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   140
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   141
  def unknown_runs(items: List[Item]): List[List[Item]] =
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   142
  {
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   143
    val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   144
    if (run.nonEmpty) run :: unknown_runs(rest) else Nil
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   145
  }
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   146
64409
70c87ca55f2c tuned signature -- more friendly for experimentation;
wenzelm
parents: 64405
diff changeset
   147
  sealed case class Remote_Build(
65764
1af6d544c2a3 clarified description vs. file name;
wenzelm
parents: 65747
diff changeset
   148
    description: String,
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   149
    host: String,
71779
03133befa33b support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents: 71778
diff changeset
   150
    actual_host: String = "",
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   151
    user: String = "",
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 65063
diff changeset
   152
    port: Int = 0,
67746
cb0f0f5f8876 more ssh options;
wenzelm
parents: 67608
diff changeset
   153
    proxy_host: String = "",
cb0f0f5f8876 more ssh options;
wenzelm
parents: 67608
diff changeset
   154
    proxy_user: String = "",
cb0f0f5f8876 more ssh options;
wenzelm
parents: 67608
diff changeset
   155
    proxy_port: Int = 0,
67775
8fe8424ff0d3 clarified signature;
wenzelm
parents: 67774
diff changeset
   156
    self_update: Boolean = false,
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   157
    historic: Boolean = false,
65789
fccd7be5fa55 enter deeper into history;
wenzelm
parents: 65785
diff changeset
   158
    history: Int = 0,
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   159
    history_base: String = "build_history_base",
72223
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   160
    java_heap: String = "",
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   161
    options: String = "",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65724
diff changeset
   162
    args: String = "",
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   163
    afp: Boolean = false,
69708
06153e2e0cdb more official AFP.groups;
wenzelm
parents: 69442
diff changeset
   164
    bulky: Boolean = false,
67076
eada9bd5fff2 avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries;
wenzelm
parents: 67071
diff changeset
   165
    more_hosts: List[String] = Nil,
67080
2c0f24e927dd macbroy2 is inactive: system update;
wenzelm
parents: 67076
diff changeset
   166
    detect: SQL.Source = "",
2c0f24e927dd macbroy2 is inactive: system update;
wenzelm
parents: 67076
diff changeset
   167
    active: Boolean = true)
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65724
diff changeset
   168
  {
67750
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   169
    def ssh_session(context: SSH.Context): SSH.Session =
71779
03133befa33b support actual_host for lrzcloud2: the proxy_host/sshd cannot resolve invented hostname (amending 1d8b6c2253e6);
wenzelm
parents: 71778
diff changeset
   170
      context.open_session(host = host, user = user, port = port, actual_host = actual_host,
67772
71a318559e30 proxy setup for lrzcloud1;
wenzelm
parents: 67769
diff changeset
   171
        proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
71769
2a82462276db more robust connection via proxy_host;
wenzelm
parents: 71752
diff changeset
   172
        permissive = proxy_host.nonEmpty)
67750
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   173
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   174
    def sql: SQL.Source =
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   175
      Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
67076
eada9bd5fff2 avoid lxbroy7, which is presently inaccessible, but retain its build history in db queries;
wenzelm
parents: 67071
diff changeset
   176
      SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   177
      (if (detect == "") "" else " AND " + SQL.enclose(detect))
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   178
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   179
    def profile: Build_Status.Profile =
69708
06153e2e0cdb more official AFP.groups;
wenzelm
parents: 69442
diff changeset
   180
      Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   181
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   182
    def pick(
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   183
      options: Options,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   184
      rev: String = "",
66865
c8b18abf23e1 tuned (graph.all_succs already contains origin);
wenzelm
parents: 66864
diff changeset
   185
      filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   186
    {
67753
f28aee3ad1e6 uniform setup_repository (pull/clone without update);
wenzelm
parents: 67752
diff changeset
   187
      val afp_rev = if (afp) Some(get_afp_rev()) else None
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   188
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   189
      val store = Build_Log.store(options)
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   190
      using(store.open_database())(db =>
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   191
      {
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   192
        def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   193
        {
66865
c8b18abf23e1 tuned (graph.all_succs already contains origin);
wenzelm
parents: 66864
diff changeset
   194
          val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
66007
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   195
          def runs = unknown_runs(items).filter(run => run.length >= gap)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   196
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   197
          if (historic || items.exists(_.known_versions(rev, afp_rev))) {
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   198
            val longest_run =
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   199
              (List.empty[Item] /: runs)({ case (item1, item2) =>
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   200
                if (item1.length >= item2.length) item1 else item2
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   201
              })
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   202
            if (longest_run.isEmpty) None
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   203
            else Some(longest_run(longest_run.length / 2).versions)
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   204
          }
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   205
          else if (rev != "") Some((rev, afp_rev))
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   206
          else runs.flatten.headOption.map(_.versions)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   207
        }
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   208
66007
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   209
        pick_days(options.int("build_log_history") max history, 2) orElse
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   210
        pick_days(200, 5) orElse
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   211
        pick_days(2000, 1)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   212
      })
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   213
    }
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65724
diff changeset
   214
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   215
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   216
  val remote_builds_old: List[Remote_Build] =
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   217
    List(
72303
f56522a44564 clarified names;
wenzelm
parents: 72229
diff changeset
   218
      Remote_Build("AFP old bulky", "lrzcloud1", self_update = true,
70947
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70663
diff changeset
   219
        proxy_host = "lxbroy10", proxy_user = "i21isatest",
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70663
diff changeset
   220
        options = "-m64 -M6 -U30000 -s10 -t AFP",
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70663
diff changeset
   221
        args = "-g large -g slow",
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70663
diff changeset
   222
        afp = true,
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70663
diff changeset
   223
        bulky = true,
6a835635fa93 disable lrzcloud1 -- superseded by lrzcloud2;
wenzelm
parents: 70663
diff changeset
   224
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
72303
f56522a44564 clarified names;
wenzelm
parents: 72229
diff changeset
   225
      Remote_Build("AFP old", "lxbroy7",
69708
06153e2e0cdb more official AFP.groups;
wenzelm
parents: 69442
diff changeset
   226
          args = "-N -X large -X slow",
67608
1b2be3666b89 retain remote_builds_old for build_status;
wenzelm
parents: 67607
diff changeset
   227
          afp = true,
1b2be3666b89 retain remote_builds_old for build_status;
wenzelm
parents: 67607
diff changeset
   228
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   229
      Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   230
        history_base = "37074e22e8be",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   231
        options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   232
        args = "-N -g timing",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   233
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " +
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   234
          Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
66931
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   235
      Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   236
        history_base = "a9d5b59c3e12",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   237
        options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   238
        args = "-N -g timing",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   239
        detect =
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   240
          Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   241
          Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   242
      Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   243
        history_base = "37074e22e8be",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   244
        options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   245
        args = "-a",
9bef97f78b60 updated test version;
wenzelm
parents: 66613
diff changeset
   246
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")),
66931
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   247
      Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   248
        history_base = "a9d5b59c3e12",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   249
        options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   250
        args = "-a",
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   251
        detect =
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   252
        Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
4ff031d249b2 deactivated old tests;
wenzelm
parents: 66923
diff changeset
   253
        Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   254
      Remote_Build("Poly/ML test", "lxbroy8",
65843
d547173212d2 proper init_settings for init_component (before generated ML_OPTIONS etc.);
wenzelm
parents: 65840
diff changeset
   255
        options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   256
        args = "-N -g timing",
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   257
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   258
      Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
72203
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   259
        detect = Build_Log.Prop.build_start + " < date '2017-03-03'")) :::
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   260
      {
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   261
        for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   262
        yield {
72303
f56522a44564 clarified names;
wenzelm
parents: 72229
diff changeset
   263
          Remote_Build("AFP old", host = hosts.head, more_hosts = hosts.tail,
72203
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   264
            options = "-m32 -M1x2 -t AFP -P" + n +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   265
              " -e ISABELLE_GHC=ghc" +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   266
              " -e ISABELLE_MLTON=mlton" +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   267
              " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   268
              " -e ISABELLE_SMLNJ=sml",
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   269
            args = "-N -X large -X slow",
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   270
            afp = true,
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   271
            detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   272
        }
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   273
      }
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   274
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   275
  val remote_builds1: List[List[Remote_Build]] =
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65724
diff changeset
   276
  {
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   277
    List(
65764
1af6d544c2a3 clarified description vs. file name;
wenzelm
parents: 65747
diff changeset
   278
      List(Remote_Build("Linux A", "lxbroy9",
72224
bbec0acf2592 use less memory on old hardware;
wenzelm
parents: 72223
diff changeset
   279
        java_heap = "2g", options = "-m32 -B -M1x2,2", args = "-N -g timing")),
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   280
      List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65724
diff changeset
   281
        options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
68386
4a3fc3420747 full benchmarks, including all conditional theories;
wenzelm
parents: 68209
diff changeset
   282
      List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
72224
bbec0acf2592 use less memory on old hardware;
wenzelm
parents: 72223
diff changeset
   283
        java_heap = "2g",
72225
cb7ddc321f52 tuned whitespace;
wenzelm
parents: 72224
diff changeset
   284
        options = "-m32 -B -M1x2,2 -t Benchmarks" +
cb7ddc321f52 tuned whitespace;
wenzelm
parents: 72224
diff changeset
   285
          " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
cb7ddc321f52 tuned whitespace;
wenzelm
parents: 72224
diff changeset
   286
          " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind -e ISABELLE_SMLNJ=sml" +
cb7ddc321f52 tuned whitespace;
wenzelm
parents: 72224
diff changeset
   287
          " -e ISABELLE_SWIPL=swipl",
cb7ddc321f52 tuned whitespace;
wenzelm
parents: 72224
diff changeset
   288
        args = "-N -a -d '~~/src/Benchmarks'",
cb7ddc321f52 tuned whitespace;
wenzelm
parents: 72224
diff changeset
   289
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))),
64351
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   290
      List(
67103
39cc38a06610 clarified description for mixed Mavericks / El Capitan system;
wenzelm
parents: 67089
diff changeset
   291
        Remote_Build("Mac OS X", "macbroy2",
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   292
          options = "-m32 -M8" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   293
            " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
70109
f387618d9053 updated settings: ISABELLE_OCAMLFIND, ISABELLE_OCAML_SETUP, but retain compatibility with historic versions that require ISABELLE_OCAMLC;
wenzelm
parents: 69709
diff changeset
   294
            " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
70137
160fcaf502d7 avoid global .opam directory: shared home leads to confusion about explicit vs. implicit ISABELLE_OCAMLFIND;
wenzelm
parents: 70134
diff changeset
   295
            " -e ISABELLE_OPAM_ROOT=\"$ISABELLE_HOME/opam\"" +
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   296
            " -e ISABELLE_SMLNJ=/home/isabelle/smlnj/110.85/bin/sml" +
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   297
            " -p pide_session=false",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   298
          args = "-a",
67080
2c0f24e927dd macbroy2 is inactive: system update;
wenzelm
parents: 67076
diff changeset
   299
          detect = Build_Log.Prop.build_tags.undefined,
67089
c96ee0eb0d5f macbroy2 is back, still pretending to be on Mavericks for better comparison of performance;
wenzelm
parents: 67080
diff changeset
   300
          history_base = "2c0f24e927dd"),
67103
39cc38a06610 clarified description for mixed Mavericks / El Capitan system;
wenzelm
parents: 67089
diff changeset
   301
        Remote_Build("Mac OS X, quick_and_dirty", "macbroy2",
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   302
          options = "-m32 -M8 -t quick_and_dirty -p pide_session=false", args = "-a -o quick_and_dirty",
67080
2c0f24e927dd macbroy2 is inactive: system update;
wenzelm
parents: 67076
diff changeset
   303
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"),
67089
c96ee0eb0d5f macbroy2 is back, still pretending to be on Mavericks for better comparison of performance;
wenzelm
parents: 67080
diff changeset
   304
          history_base = "2c0f24e927dd"),
67103
39cc38a06610 clarified description for mixed Mavericks / El Capitan system;
wenzelm
parents: 67089
diff changeset
   305
        Remote_Build("Mac OS X, skip_proofs", "macbroy2",
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   306
          options = "-m32 -M8 -t skip_proofs -p pide_session=false", args = "-a -o skip_proofs",
67080
2c0f24e927dd macbroy2 is inactive: system update;
wenzelm
parents: 67076
diff changeset
   307
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"),
67089
c96ee0eb0d5f macbroy2 is back, still pretending to be on Mavericks for better comparison of performance;
wenzelm
parents: 67080
diff changeset
   308
          history_base = "2c0f24e927dd")),
65768
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   309
      List(
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   310
        Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2 -p pide_session=false", args = "-a",
65768
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   311
          detect = Build_Log.Prop.build_start + " > date '2017-03-03'")),
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   312
      List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2 -p pide_session=false", args = "-a")),
71780
24b68a932f26 back to old-style names for uniform sorting of build_status (amending 138e8226961e);
wenzelm
parents: 71779
diff changeset
   313
      List(Remote_Build("Mac OS X 10.13 High Sierra", "lapbroy68",
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   314
        options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
71752
138e8226961e tuned OS names;
wenzelm
parents: 71751
diff changeset
   315
        self_update = true, args = "-a -d '~~/src/Benchmarks'")),
71780
24b68a932f26 back to old-style names for uniform sorting of build_status (amending 138e8226961e);
wenzelm
parents: 71779
diff changeset
   316
      List(Remote_Build("Mac OS X 10.14 Mojave", "lapnipkow3",
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   317
        options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
71752
138e8226961e tuned OS names;
wenzelm
parents: 71751
diff changeset
   318
        self_update = true, args = "-a -d '~~/src/Benchmarks'")),
71780
24b68a932f26 back to old-style names for uniform sorting of build_status (amending 138e8226961e);
wenzelm
parents: 71779
diff changeset
   319
      List(Remote_Build("Mac OS X 10.15 Catalina", "laramac01", user = "makarius",
71751
93bdbac68d8d standard tests for macOS 10.15 Catalina;
wenzelm
parents: 71589
diff changeset
   320
        proxy_host = "laraserver", proxy_user = "makarius",
72213
694009ed4ee1 clarified options --- potentially more robust;
wenzelm
parents: 72207
diff changeset
   321
        self_update = true,
72229
720b72513ae5 no pide_session on macos: avoid odd "hang" of remote_build_history;
wenzelm
parents: 72225
diff changeset
   322
        options = "-m32 -M4 -e ISABELLE_GHC_SETUP=true -p pide_session=false",
71751
93bdbac68d8d standard tests for macOS 10.15 Catalina;
wenzelm
parents: 71589
diff changeset
   323
        args = "-a -d '~~/src/Benchmarks'")),
64351
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   324
      List(
67775
8fe8424ff0d3 clarified signature;
wenzelm
parents: 67774
diff changeset
   325
        Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   326
          options = "-m32 -M4" +
70113
31ee094dea3d prefer ISABELLE_OCAML_SETUP: Cygwin lacks libzarith;
wenzelm
parents: 70109
diff changeset
   327
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
70134
385458b950e1 clarified GHC and OCaml test setup;
wenzelm
parents: 70119
diff changeset
   328
            " -e ISABELLE_GHC_SETUP=true" +
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   329
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   330
          args = "-a",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65724
diff changeset
   331
          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
67775
8fe8424ff0d3 clarified signature;
wenzelm
parents: 67774
diff changeset
   332
        Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   333
          options = "-m64 -M4" +
70113
31ee094dea3d prefer ISABELLE_OCAML_SETUP: Cygwin lacks libzarith;
wenzelm
parents: 70109
diff changeset
   334
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
70134
385458b950e1 clarified GHC and OCaml test setup;
wenzelm
parents: 70119
diff changeset
   335
            " -e ISABELLE_GHC_SETUP=true" +
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   336
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   337
          args = "-a",
72203
e5fe4d40326d discontinued old AFP test: ancient hardware with insufficient resources;
wenzelm
parents: 71976
diff changeset
   338
          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))))
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65724
diff changeset
   339
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   340
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   341
  val remote_builds2: List[List[Remote_Build]] =
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   342
    List(
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   343
      List(
72303
f56522a44564 clarified names;
wenzelm
parents: 72229
diff changeset
   344
        Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true,
70653
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   345
          proxy_host = "lxbroy10", proxy_user = "i21isatest",
72223
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   346
          java_heap = "8g",
70653
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   347
          options = "-m32 -M1x8 -t AFP" +
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   348
            " -e ISABELLE_GHC=ghc" +
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   349
            " -e ISABELLE_MLTON=mlton" +
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   350
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAMLFIND=ocamlfind" +
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   351
            " -e ISABELLE_SMLNJ=sml",
70663
90acc6ce5beb proper build options;
wenzelm
parents: 70653
diff changeset
   352
          args = "-a -X large -X slow",
70653
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   353
          afp = true,
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   354
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
72304
f3e1144a1cec clarified name to avoid duplication (no distinction of data on host = lrzcloud2);
wenzelm
parents: 72303
diff changeset
   355
        Remote_Build("AFP", "lrzcloud2", actual_host = "10.195.4.41", self_update = true,
70653
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   356
          proxy_host = "lxbroy10", proxy_user = "i21isatest",
72223
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   357
          java_heap = "8g",
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   358
          options = "-m64 -M8 -U30000 -s10 -t AFP",
70653
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   359
          args = "-g large -g slow",
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   360
          afp = true,
b32d571f1190 full AFP test on lrzcloud2;
wenzelm
parents: 70652
diff changeset
   361
          bulky = true,
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   362
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   363
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   364
  def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   365
    : Logger_Task =
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   366
  {
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   367
    val task_name = "build_history-" + r.host
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   368
    Logger_Task(task_name, logger =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   369
      {
67750
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   370
        using(r.ssh_session(logger.ssh_context))(ssh =>
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   371
          {
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   372
            val results =
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   373
              Build_History.remote_build_history(ssh,
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   374
                isabelle_repos,
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   375
                isabelle_repos.ext(r.host),
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   376
                isabelle_identifier = "cronjob_build_history",
67775
8fe8424ff0d3 clarified signature;
wenzelm
parents: 67774
diff changeset
   377
                self_update = r.self_update,
67750
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   378
                rev = rev,
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   379
                afp_rev = afp_rev,
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   380
                options =
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   381
                  " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
72223
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   382
                  " -f -h " + Bash.string(r.host) + " " +
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   383
                  (r.java_heap match {
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   384
                    case "" => ""
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   385
                    case h =>
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   386
                      "-e 'ISABELLE_TOOL_JAVA_OPTIONS=\"$ISABELLE_TOOL_JAVA_OPTIONS -Xmx" + h + "\"' "
088e3aa85250 clarified signature;
wenzelm
parents: 72213
diff changeset
   387
                  }) + r.options,
67750
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   388
                args = "-o timeout=10800 " + r.args)
64346
5f49765a25ec process results immediately;
wenzelm
parents: 64338
diff changeset
   389
67750
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   390
            for ((log_name, bytes) <- results) {
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   391
              logger.log(Date.now(), log_name)
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   392
              Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   393
            }
58a33c568464 tuned signature;
wenzelm
parents: 67746
diff changeset
   394
          })
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   395
      })
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   396
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   397
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   398
  val build_status_profiles: List[Build_Status.Profile] =
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   399
    (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   400
65746
dead16007097 present build status;
wenzelm
parents: 65736
diff changeset
   401
64192
wenzelm
parents: 64187
diff changeset
   402
wenzelm
parents: 64187
diff changeset
   403
  /** task logging **/
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   404
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   405
  object Log_Service
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   406
  {
71942
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71899
diff changeset
   407
    def apply(options: Options, progress: Progress = new Progress): Log_Service =
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   408
      new Log_Service(SSH.init_context(options), progress)
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   409
  }
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   410
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   411
  class Log_Service private(val ssh_context: SSH.Context, progress: Progress)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   412
  {
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   413
    current_log.file.delete
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   414
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   415
    private val thread: Consumer_Thread[String] =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   416
      Consumer_Thread.fork("cronjob: logger", daemon = true)(
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   417
        consume = (text: String) =>
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   418
          { // critical
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   419
            File.append(current_log, text + "\n")
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   420
            File.append(cumulative_log, text + "\n")
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   421
            progress.echo(text)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   422
            true
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   423
          })
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   424
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   425
    def shutdown() { thread.shutdown() }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   426
71816
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71780
diff changeset
   427
    val hostname: String = Isabelle_System.hostname()
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   428
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   429
    def log(date: Date, task_name: String, msg: String): Unit =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   430
      if (task_name != "")
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   431
        thread.send(
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   432
          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   433
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   434
    def start_logger(start_date: Date, task_name: String): Logger =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   435
      new Logger(this, start_date, task_name)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   436
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   437
    def run_task(start_date: Date, task: Logger_Task)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   438
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   439
      val logger = start_logger(start_date, task.name)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   440
      val res = Exn.capture { task.body(logger) }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   441
      val end_date = Date.now()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   442
      val err =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   443
        res match {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   444
          case Exn.Res(_) => None
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   445
          case Exn.Exn(exn) =>
67178
70576478bda9 avoid println with its extra CR on Windows;
wenzelm
parents: 67103
diff changeset
   446
            Output.writeln("Exception trace for " + quote(task.name) + ":")
64397
6e9c22c494c5 more informative error (stderr);
wenzelm
parents: 64351
diff changeset
   447
            exn.printStackTrace()
66923
wenzelm
parents: 66903
diff changeset
   448
            val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   449
            Some(first_line)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   450
        }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   451
      logger.log_end(end_date, err)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   452
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   453
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   454
    def fork_task(start_date: Date, task: Logger_Task): Task =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   455
      new Task(task.name, run_task(start_date, task))
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   456
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   457
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   458
  class Logger private[Isabelle_Cronjob](
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   459
    val log_service: Log_Service, val start_date: Date, val task_name: String)
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64157
diff changeset
   460
  {
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64252
diff changeset
   461
    def ssh_context: SSH.Context = log_service.ssh_context
65640
7a26c337e016 maintain build_log database;
wenzelm
parents: 65594
diff changeset
   462
    def options: Options = ssh_context.options
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   463
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   464
    def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   465
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   466
    def log_end(end_date: Date, err: Option[String])
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   467
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   468
      val elapsed_time = end_date.time - start_date.time
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   469
      val msg =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   470
        (if (err.isEmpty) "finished" else "ERROR " + err.get) +
64197
c43dedbb8118 tuned message;
wenzelm
parents: 64195
diff changeset
   471
        (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   472
      log(end_date, msg)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   473
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   474
64195
wenzelm
parents: 64194
diff changeset
   475
    val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
wenzelm
parents: 64194
diff changeset
   476
wenzelm
parents: 64194
diff changeset
   477
    Isabelle_System.mkdirs(log_dir)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   478
    log(start_date, "started")
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   479
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   480
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   481
  class Task private[Isabelle_Cronjob](name: String, body: => Unit)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   482
  {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   483
    private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   484
    def is_finished: Boolean = future.is_finished
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64157
diff changeset
   485
  }
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   486
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   487
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   488
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   489
  /** cronjob **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   490
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   491
  def cronjob(progress: Progress, exclude_task: Set[String])
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   492
  {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   493
    /* soft lock */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   494
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   495
    val still_running =
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   496
      try { Some(File.read(main_state_file)) }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   497
      catch { case ERROR(_) => None }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   498
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   499
    still_running match {
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   500
      case None | Some("") =>
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   501
      case Some(running) =>
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   502
        error("Isabelle cronjob appears to be still running: " + running)
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   503
    }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   504
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   505
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   506
    /* log service */
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   507
67752
636f633552a3 clarified signature: facilitate interactive experimentation;
wenzelm
parents: 67751
diff changeset
   508
    val log_service = Log_Service(Options.init(), progress = progress)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   509
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   510
    def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   511
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   512
    def run_now(task: Logger_Task) { run(Date.now(), task) }
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   513
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   514
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   515
    /* structured tasks */
64184
wenzelm
parents: 64173
diff changeset
   516
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   517
    def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   518
      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   519
        run_now(task))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   520
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   521
    def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   522
      {
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   523
        @tailrec def join(running: List[Task])
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   524
        {
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   525
          running.partition(_.is_finished) match {
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   526
            case (Nil, Nil) =>
71899
5036edb025b7 clarified signature;
wenzelm
parents: 71848
diff changeset
   527
            case (Nil, _ :: _) => Time.seconds(0.5).sleep; join(running)
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   528
            case (_ :: _, remaining) => join(remaining)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   529
          }
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   530
        }
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   531
        val start_date = Date.now()
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   532
        val running =
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   533
          for (task <- tasks if !exclude_task(task.name))
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   534
            yield log_service.fork_task(start_date, task)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   535
        join(running)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   536
      })
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   537
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   538
66897
wenzelm
parents: 66896
diff changeset
   539
    /* repository structure */
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   540
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   541
    val hg = Mercurial.repository(isabelle_repos)
66895
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   542
    val hg_graph = hg.graph()
67048
ec438988b65a local user_home for improved performance, but only after given changeset for stability of measurement history;
wenzelm
parents: 67008
diff changeset
   543
66895
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   544
    def history_base_filter(r: Remote_Build): Item => Boolean =
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   545
    {
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   546
      val base_rev = hg.id(r.history_base)
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   547
      val nodes = hg_graph.all_succs(List(base_rev)).toSet
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   548
      (item: Item) => nodes(item.isabelle_version)
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   549
    }
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66887
diff changeset
   550
66897
wenzelm
parents: 66896
diff changeset
   551
wenzelm
parents: 66896
diff changeset
   552
    /* main */
wenzelm
parents: 66896
diff changeset
   553
wenzelm
parents: 66896
diff changeset
   554
    val main_start_date = Date.now()
wenzelm
parents: 66896
diff changeset
   555
    File.write(main_state_file, main_start_date + " " + log_service.hostname)
wenzelm
parents: 66896
diff changeset
   556
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   557
    run(main_start_date,
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   558
      Logger_Task("isabelle_cronjob", logger =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   559
        run_now(
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   560
          SEQ(List(
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   561
            init,
67774
5437491732d2 build_history_base as remote build on lxbroy10: thus self_update has already happened once, and thus avoids conflicts with parallel builds on shared home directory;
wenzelm
parents: 67772
diff changeset
   562
            build_history_base,
70380
e4abb5235c5e sequential build_release: it uses some of the test machines for pre-built images;
wenzelm
parents: 70137
diff changeset
   563
            build_release,
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   564
            PAR(
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   565
              List(remote_builds1, remote_builds2).map(remote_builds =>
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   566
              SEQ(List(
67080
2c0f24e927dd macbroy2 is inactive: system update;
wenzelm
parents: 67076
diff changeset
   567
                PAR(remote_builds.map(_.filter(_.active)).map(seq =>
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   568
                  SEQ(
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   569
                    for {
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   570
                      (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
67048
ec438988b65a local user_home for improved performance, but only after given changeset for stability of measurement history;
wenzelm
parents: 67008
diff changeset
   571
                      (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
67071
85e6c1ff5be3 removed pointless user_home: no measurable impact;
wenzelm
parents: 67049
diff changeset
   572
                    } yield remote_build_history(rev, afp_rev, i, r)))),
67008
eed58245b579 superseded by plain_identify;
wenzelm
parents: 66980
diff changeset
   573
                Logger_Task("jenkins_logs", _ =>
68209
aeffd8f1f079 support Store with options;
wenzelm
parents: 67868
diff changeset
   574
                  Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)),
66898
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   575
                Logger_Task("build_log_database",
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   576
                  logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
8b7c4679c05b parallel remote_builds2 for the sake of "AFP slow" (with theoretical data race on build_log_dirs);
wenzelm
parents: 66897
diff changeset
   577
                Logger_Task("build_status",
67766
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   578
                  logger => Isabelle_Devel.build_status(logger.options)))))),
603334230303 consolidated main cronjob server on virtual machine together with build_log database;
wenzelm
parents: 67763
diff changeset
   579
            exit)))))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   580
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   581
    log_service.shutdown()
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   582
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   583
    main_state_file.file.delete
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   584
  }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   585
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   586
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   587
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   588
  /** command line entry point **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   589
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   590
  def main(args: Array[String])
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   591
  {
71848
c1bc38327bc2 clarified signature;
wenzelm
parents: 71816
diff changeset
   592
    Command_Line.tool {
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   593
      var force = false
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   594
      var verbose = false
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   595
      var exclude_task = Set.empty[String]
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   596
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   597
      val getopts = Getopts("""
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   598
Usage: Admin/cronjob/main [OPTIONS]
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   599
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   600
  Options are:
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   601
    -f           apply force to do anything
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   602
    -v           verbose
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   603
    -x NAME      exclude tasks with this name
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   604
""",
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   605
        "f" -> (_ => force = true),
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   606
        "v" -> (_ => verbose = true),
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   607
        "x:" -> (arg => exclude_task += arg))
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   608
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   609
      val more_args = getopts(args)
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   610
      if (more_args.nonEmpty) getopts.usage()
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   611
71942
a5fda30edae2 clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents: 71899
diff changeset
   612
      val progress = if (verbose) new Console_Progress() else new Progress
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   613
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   614
      if (force) cronjob(progress, exclude_task)
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   615
      else error("Need to apply force to do anything")
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   616
    }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   617
  }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   618
}