src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Thu, 19 Oct 2017 00:55:34 +0200
changeset 66883 ee874941dfb8
parent 66880 486f4af28db9
child 66887 72b78ee82f7b
permissions -rw-r--r--
proper integer option for Admin/build_history;
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
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    10
import scala.annotation.tailrec
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    11
import scala.collection.mutable
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    12
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
    13
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
    14
object Isabelle_Cronjob
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
    15
{
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    16
  /* file-system state: owned by main cronjob */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    17
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    18
  val main_dir = Path.explode("~/cronjob")
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    19
  val main_state_file = main_dir + Path.explode("run/main.state")
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
    20
  val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
    21
  val cumulative_log = 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
    22
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    23
  val isabelle_repos = main_dir + Path.explode("isabelle")
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    24
  val isabelle_repos_test = main_dir + Path.explode("isabelle-test")
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    25
  val afp_repos = main_dir + Path.explode("AFP")
64236
358f9ff08681 discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
wenzelm
parents: 64235
diff changeset
    26
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65735
diff changeset
    27
  val jenkins_jobs = "identify" :: Jenkins.build_log_jobs
65666
45d0692bb019 incremental download of Jenkins log files, which are also added to database;
wenzelm
parents: 65647
diff changeset
    28
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    29
64192
wenzelm
parents: 64187
diff changeset
    30
wenzelm
parents: 64187
diff changeset
    31
  /** particular tasks **/
wenzelm
parents: 64187
diff changeset
    32
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    33
  /* identify Isabelle + AFP repository snapshots and build release */
64192
wenzelm
parents: 64187
diff changeset
    34
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    35
  private val build_release =
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    36
    Logger_Task("build_release", logger =>
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    37
      {
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    38
        Isabelle_Devel.make_index()
65771
688a7dd22cbb make index formally within Isabelle/Scala;
wenzelm
parents: 65770
diff changeset
    39
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    40
        val rev = Mercurial.repository(isabelle_repos).id()
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    41
        val afp_rev = Mercurial.setup_repository(AFP.repos_source, afp_repos).id()
64192
wenzelm
parents: 64187
diff changeset
    42
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    43
        File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    44
          Build_Log.Identify.content(logger.start_date, Some(rev), Some(afp_rev)))
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    45
66859
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    46
        Isabelle_Devel.release_snapshot(rev = rev, afp_rev = afp_rev,
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    47
          parallel_jobs = 4, remote_mac = "macbroy31")
dd846a805fb1 tuned whitespace;
wenzelm
parents: 66858
diff changeset
    48
      })
64192
wenzelm
parents: 64187
diff changeset
    49
wenzelm
parents: 64187
diff changeset
    50
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    51
  /* integrity test of build_history vs. build_history_base */
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    52
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    53
  private val build_history_base =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    54
    Logger_Task("build_history_base", logger =>
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    55
      {
64251
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    56
        val hg =
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    57
          Mercurial.setup_repository(
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    58
            File.standard_path(isabelle_repos), isabelle_repos_test)
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    59
        for {
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    60
          (result, log_path) <-
66861
f6676691ef8a partition AFP sessions according to structure, which happens to cut it roughly into equal parts;
wenzelm
parents: 66860
diff changeset
    61
            Build_History.build_history(logger.options, isabelle_repos_test,
66860
54ae2cc05325 support for AFP in build_history and remote_build_history;
wenzelm
parents: 66859
diff changeset
    62
              rev = "build_history_base", fresh = true, build_args = List("HOL"))
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    63
        } {
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    64
          result.check
64482
43f6c28ff496 clarified File.move: target directory like File.copy;
wenzelm
parents: 64481
diff changeset
    65
          File.move(log_path, logger.log_dir + log_path.base)
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    66
        }
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    67
      })
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    68
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    69
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    70
  /* remote build_history */
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    71
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    72
  sealed case class Item(
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    73
    known: Boolean,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    74
    isabelle_version: String,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    75
    afp_version: Option[String],
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    76
    pull_date: Date)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
    77
  {
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
    78
    def unknown: Boolean = !known
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    79
    def versions: (String, Option[String]) = (isabelle_version, afp_version)
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    80
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    81
    def known_versions(rev: String, afp_rev: Option[String]): Boolean =
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    82
      known && rev != "" && isabelle_version == rev &&
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    83
      (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev.get)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
    84
  }
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
    85
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    86
  def recent_items(db: SQL.Database,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    87
    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
    88
  {
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66879
diff changeset
    89
    val afp = afp_rev.isDefined
65807
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
    90
    val select =
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    91
      Build_Log.Data.select_recent_versions(
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
    92
        days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
65807
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
    93
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
    94
    db.using_statement(select)(stmt =>
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
    95
      stmt.execute_query().iterator(res =>
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
    96
      {
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
    97
        val known = res.bool(Build_Log.Data.known)
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
    98
        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
    99
        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
   100
        val pull_date = res.date(Build_Log.Data.pull_date(afp))
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   101
        Item(known, isabelle_version, afp_version, pull_date)
65807
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   102
      }).toList)
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   103
  }
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   104
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   105
  def unknown_runs(items: List[Item]): List[List[Item]] =
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   106
  {
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   107
    val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   108
    if (run.nonEmpty) run :: unknown_runs(rest) else Nil
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   109
  }
a830c6257393 tuned -- more open to experimentation;
wenzelm
parents: 65806
diff changeset
   110
64409
70c87ca55f2c tuned signature -- more friendly for experimentation;
wenzelm
parents: 64405
diff changeset
   111
  sealed case class Remote_Build(
65764
1af6d544c2a3 clarified description vs. file name;
wenzelm
parents: 65747
diff changeset
   112
    description: String,
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   113
    host: String,
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   114
    user: String = "",
65594
659305708959 clarified treatment of default port;
wenzelm
parents: 65063
diff changeset
   115
    port: Int = 0,
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   116
    shared_home: Boolean = true,
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   117
    historic: Boolean = false,
65789
fccd7be5fa55 enter deeper into history;
wenzelm
parents: 65785
diff changeset
   118
    history: Int = 0,
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   119
    history_base: String = "build_history_base",
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   120
    options: String = "",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   121
    args: String = "",
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   122
    afp: Boolean = false,
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   123
    detect: SQL.Source = "")
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   124
  {
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   125
    def sql: SQL.Source =
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   126
      Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   127
      Build_Log.Prop.build_host + " = " + SQL.string(host) +
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   128
      (if (detect == "") "" else " AND " + SQL.enclose(detect))
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   129
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   130
    def profile: Build_Status.Profile =
66880
486f4af28db9 more thorough treatment of afp_version and afp_pull_date;
wenzelm
parents: 66879
diff changeset
   131
      Build_Status.Profile(description, history = history, afp = afp, sql = sql)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   132
66865
c8b18abf23e1 tuned (graph.all_succs already contains origin);
wenzelm
parents: 66864
diff changeset
   133
    def history_base_filter(hg: Mercurial.Repository): Item => Boolean =
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   134
    {
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   135
      val rev0 = hg.id(history_base)
66865
c8b18abf23e1 tuned (graph.all_succs already contains origin);
wenzelm
parents: 66864
diff changeset
   136
      val nodes = hg.graph().all_succs(List(rev0)).toSet
c8b18abf23e1 tuned (graph.all_succs already contains origin);
wenzelm
parents: 66864
diff changeset
   137
      (item: Item) => nodes(item.isabelle_version)
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   138
    }
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   139
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   140
    def pick(
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   141
      options: Options,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   142
      rev: String = "",
66865
c8b18abf23e1 tuned (graph.all_succs already contains origin);
wenzelm
parents: 66864
diff changeset
   143
      filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   144
    {
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   145
      val afp_rev = if (afp) Some(Mercurial.repository(afp_repos).id()) else None
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   146
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   147
      val store = Build_Log.store(options)
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   148
      using(store.open_database())(db =>
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   149
      {
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   150
        def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   151
        {
66865
c8b18abf23e1 tuned (graph.all_succs already contains origin);
wenzelm
parents: 66864
diff changeset
   152
          val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
66007
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   153
          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
   154
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   155
          if (historic || items.exists(_.known_versions(rev, afp_rev))) {
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   156
            val longest_run =
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   157
              (List.empty[Item] /: runs)({ case (item1, item2) =>
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   158
                if (item1.length >= item2.length) item1 else item2
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   159
              })
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   160
            if (longest_run.isEmpty) None
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   161
            else Some(longest_run(longest_run.length / 2).versions)
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   162
          }
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   163
          else if (rev != "") Some((rev, afp_rev))
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   164
          else runs.flatten.headOption.map(_.versions)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   165
        }
65810
356c2b488cf3 explore older history;
wenzelm
parents: 65809
diff changeset
   166
66007
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   167
        pick_days(options.int("build_log_history") max history, 2) orElse
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   168
        pick_days(200, 5) orElse
6706d6f0afda cover more history;
wenzelm
parents: 65949
diff changeset
   169
        pick_days(2000, 1)
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   170
      })
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   171
    }
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   172
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   173
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   174
  val remote_builds_old: List[Remote_Build] =
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   175
    List(
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   176
      Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   177
        history_base = "37074e22e8be",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   178
        options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   179
        args = "-N -g timing",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   180
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " +
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   181
          Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   182
      Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   183
        history_base = "37074e22e8be",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   184
        options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   185
        args = "-a",
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   186
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")),
65806
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   187
      Remote_Build("Poly/ML test", "lxbroy8",
65843
d547173212d2 proper init_settings for init_component (before generated ML_OPTIONS etc.);
wenzelm
parents: 65840
diff changeset
   188
        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
   189
        args = "-N -g timing",
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   190
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   191
      Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   192
        detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   193
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   194
0156222f2a18 tuned -- more visible;
wenzelm
parents: 65805
diff changeset
   195
  val remote_builds: List[List[Remote_Build]] =
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   196
  {
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   197
    List(
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   198
      List(Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   199
        history_base = "37074e22e8be",
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   200
        options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre1 -i 'init_component /home/isabelle/contrib/polyml-test-e7a662f8f9c4'",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   201
        args = "-N -g timing",
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   202
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1"))),
65764
1af6d544c2a3 clarified description vs. file name;
wenzelm
parents: 65747
diff changeset
   203
      List(Remote_Build("Linux A", "lxbroy9",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   204
        options = "-m32 -B -M1x2,2", args = "-N -g timing")),
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   205
      List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   206
        options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
64351
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   207
      List(
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   208
        Remote_Build("Mac OS X 10.9 Mavericks", "macbroy2",
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   209
          options = "-m32 -M8" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   210
            " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   211
            " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_SMLNJ=/mnt/nfsbroy/home/smlnj/bin/sml",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   212
          args = "-a",
66856
6b90c688a6dc tuned signature;
wenzelm
parents: 66854
diff changeset
   213
          detect = Build_Log.Prop.build_tags.undefined),
65768
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   214
        Remote_Build("Mac OS X 10.9 Mavericks, quick_and_dirty", "macbroy2",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   215
          options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   216
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty")),
65768
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   217
        Remote_Build("Mac OS X 10.9 Mavericks, skip_proofs", "macbroy2",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   218
          options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
66009
4fe8e0b2590a more tests;
wenzelm
parents: 66008
diff changeset
   219
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs")),
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   220
        Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2",
66009
4fe8e0b2590a more tests;
wenzelm
parents: 66008
diff changeset
   221
          history_base = "37074e22e8be",
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   222
          options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre1 -i 'init_component /home/isabelle/contrib/polyml-test-e7a662f8f9c4'",
66009
4fe8e0b2590a more tests;
wenzelm
parents: 66008
diff changeset
   223
          args = "-a",
66762
9bef97f78b60 updated test version;
wenzelm
parents: 66609
diff changeset
   224
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1"))),
65768
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   225
      List(
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   226
        Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a",
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   227
          detect = Build_Log.Prop.build_start + " > date '2017-03-03'")),
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   228
      List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")),
64351
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   229
      List(
66008
010698325e36 cover more history;
wenzelm
parents: 66007
diff changeset
   230
        Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, shared_home = false,
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   231
          options = "-m32 -M4" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   232
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   233
            " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   234
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   235
          args = "-a",
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   236
          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
66008
010698325e36 cover more history;
wenzelm
parents: 66007
diff changeset
   237
        Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, shared_home = false,
65906
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   238
          options = "-m64 -M4" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   239
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   240
            " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
78fa1771f61d more settings;
wenzelm
parents: 65902
diff changeset
   241
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
65902
c28143ae38cd more settings;
wenzelm
parents: 65887
diff changeset
   242
          args = "-a",
66868
740d22146cb6 more AFP tests;
wenzelm
parents: 66865
diff changeset
   243
          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))),
740d22146cb6 more AFP tests;
wenzelm
parents: 66865
diff changeset
   244
      List(
66869
222a77470c0c proper value;
wenzelm
parents: 66868
diff changeset
   245
        Remote_Build("AFP slow", "lrzcloud1", shared_home = false,
66883
ee874941dfb8 proper integer option for Admin/build_history;
wenzelm
parents: 66880
diff changeset
   246
          options = "-m64 -M6 -U30000 -s10 -t AFP",
66868
740d22146cb6 more AFP tests;
wenzelm
parents: 66865
diff changeset
   247
          args = "-g slow -X very_slow",
740d22146cb6 more AFP tests;
wenzelm
parents: 66865
diff changeset
   248
          afp = true,
740d22146cb6 more AFP tests;
wenzelm
parents: 66865
diff changeset
   249
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   250
    ) :::
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   251
    {
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   252
      for { (host, n) <- List("lxbroy6" -> 1, "lxbroy7" -> 2) }
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   253
      yield {
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   254
        List(Remote_Build("AFP " + n, host = host,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   255
          options = "-m32 -M1x2 -t AFP -P" + n,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   256
          args = "-N -X slow",
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   257
          afp = true,
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   258
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   259
      }
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   260
    }
65732
7864aea16a87 detect database entries;
wenzelm
parents: 65723
diff changeset
   261
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   262
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   263
  private def remote_build_history(
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   264
    rev: String, afp_rev: Option[String], i: Int, r: Remote_Build): Logger_Task =
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   265
  {
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   266
    val task_name = "build_history-" + r.host
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   267
    Logger_Task(task_name, logger =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   268
      {
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   269
        using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
64259
wenzelm
parents: 64257
diff changeset
   270
          ssh =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   271
            {
64348
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   272
              val self_update = !r.shared_home
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   273
              val push_isabelle_home = self_update && Mercurial.is_repository(Path.explode("~~"))
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64346
diff changeset
   274
65929
de3adcf6a276 prefer strict result (in contrast to 0f3b0a929c02);
wenzelm
parents: 65917
diff changeset
   275
              val results =
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   276
                Build_History.remote_build_history(ssh,
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   277
                  isabelle_repos,
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   278
                  isabelle_repos.ext(r.host),
65917
2b7d4678bce6 proper ISABELLE_IDENTIFIER for remote Admin/build_history, e.g. relevant for settings;
wenzelm
parents: 65915
diff changeset
   279
                  isabelle_identifier = "cronjob_build_history",
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   280
                  self_update = self_update,
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   281
                  push_isabelle_home = push_isabelle_home,
66106
b5333fc056da always start with fresh clone (with explicitly given rev): more robust on Windows;
wenzelm
parents: 66009
diff changeset
   282
                  rev = rev,
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   283
                  afp_rev = afp_rev,
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   284
                  options =
65949
wenzelm
parents: 65929
diff changeset
   285
                    " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
65887
cc6fdf8d1dc2 more systematic separation of build_history directories (see also 80c1c1f53e72);
wenzelm
parents: 65871
diff changeset
   286
                    " -f " + r.options,
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   287
                  args = "-o timeout=10800 " + r.args)
64346
5f49765a25ec process results immediately;
wenzelm
parents: 64338
diff changeset
   288
64481
caf62923039b more logging, to see better when files written;
wenzelm
parents: 64480
diff changeset
   289
              for ((log_name, bytes) <- results) {
caf62923039b more logging, to see better when files written;
wenzelm
parents: 64480
diff changeset
   290
                logger.log(Date.now(), log_name)
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   291
                Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
64481
caf62923039b more logging, to see better when files written;
wenzelm
parents: 64480
diff changeset
   292
              }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   293
            })
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   294
      })
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   295
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   296
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   297
  val build_status_profiles: List[Build_Status.Profile] =
65768
b8da621a3297 more precise profiles;
wenzelm
parents: 65764
diff changeset
   298
    (remote_builds_old :: remote_builds).flatten.map(_.profile)
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65746
diff changeset
   299
65746
dead16007097 present build status;
wenzelm
parents: 65736
diff changeset
   300
64192
wenzelm
parents: 64187
diff changeset
   301
wenzelm
parents: 64187
diff changeset
   302
  /** task logging **/
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   303
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   304
  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   305
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64252
diff changeset
   306
  class Log_Service private[Isabelle_Cronjob](progress: Progress, val ssh_context: SSH.Context)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   307
  {
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   308
    current_log.file.delete
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   309
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   310
    private val thread: Consumer_Thread[String] =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   311
      Consumer_Thread.fork("cronjob: logger", daemon = true)(
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   312
        consume = (text: String) =>
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   313
          { // critical
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   314
            File.append(current_log, text + "\n")
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   315
            File.append(cumulative_log, text + "\n")
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   316
            progress.echo(text)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   317
            true
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   318
          })
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   319
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   320
    def shutdown() { thread.shutdown() }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   321
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   322
    val hostname = Isabelle_System.hostname()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   323
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   324
    def log(date: Date, task_name: String, msg: String): Unit =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   325
      if (task_name != "")
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   326
        thread.send(
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   327
          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   328
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   329
    def start_logger(start_date: Date, task_name: String): Logger =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   330
      new Logger(this, start_date, task_name)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   331
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   332
    def run_task(start_date: Date, task: Logger_Task)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   333
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   334
      val logger = start_logger(start_date, task.name)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   335
      val res = Exn.capture { task.body(logger) }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   336
      val end_date = Date.now()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   337
      val err =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   338
        res match {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   339
          case Exn.Res(_) => None
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   340
          case Exn.Exn(exn) =>
64410
89da169f66fa more informative error (see 6e9c22c494c5);
wenzelm
parents: 64409
diff changeset
   341
            System.err.println("Exception trace for " + quote(task.name) + ":")
64397
6e9c22c494c5 more informative error (stderr);
wenzelm
parents: 64351
diff changeset
   342
            exn.printStackTrace()
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   343
            val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception"
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   344
            Some(first_line)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   345
        }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   346
      logger.log_end(end_date, err)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   347
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   348
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   349
    def fork_task(start_date: Date, task: Logger_Task): Task =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   350
      new Task(task.name, run_task(start_date, task))
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   351
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   352
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   353
  class Logger private[Isabelle_Cronjob](
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   354
    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
   355
  {
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64252
diff changeset
   356
    def ssh_context: SSH.Context = log_service.ssh_context
65640
7a26c337e016 maintain build_log database;
wenzelm
parents: 65594
diff changeset
   357
    def options: Options = ssh_context.options
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   358
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   359
    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
   360
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   361
    def log_end(end_date: Date, err: Option[String])
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   362
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   363
      val elapsed_time = end_date.time - start_date.time
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   364
      val msg =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   365
        (if (err.isEmpty) "finished" else "ERROR " + err.get) +
64197
c43dedbb8118 tuned message;
wenzelm
parents: 64195
diff changeset
   366
        (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
   367
      log(end_date, msg)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   368
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   369
64195
wenzelm
parents: 64194
diff changeset
   370
    val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
wenzelm
parents: 64194
diff changeset
   371
wenzelm
parents: 64194
diff changeset
   372
    Isabelle_System.mkdirs(log_dir)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   373
    log(start_date, "started")
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   374
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   375
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   376
  class Task private[Isabelle_Cronjob](name: String, body: => Unit)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   377
  {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   378
    private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   379
    def is_finished: Boolean = future.is_finished
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64157
diff changeset
   380
  }
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   381
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   382
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   383
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   384
  /** cronjob **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   385
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   386
  def cronjob(progress: Progress, exclude_task: Set[String])
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   387
  {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   388
    /* soft lock */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   389
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   390
    val still_running =
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   391
      try { Some(File.read(main_state_file)) }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   392
      catch { case ERROR(_) => None }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   393
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   394
    still_running match {
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   395
      case None | Some("") =>
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   396
      case Some(running) =>
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   397
        error("Isabelle cronjob appears to be still running: " + running)
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   398
    }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   399
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   400
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   401
    /* log service */
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   402
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64252
diff changeset
   403
    val log_service = new Log_Service(progress, SSH.init_context(Options.init()))
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   404
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   405
    def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   406
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   407
    def run_now(task: Logger_Task) { run(Date.now(), task) }
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   408
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   409
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   410
    /* structured tasks */
64184
wenzelm
parents: 64173
diff changeset
   411
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   412
    def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   413
      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   414
        run_now(task))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   415
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   416
    def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   417
      {
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   418
        @tailrec def join(running: List[Task])
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   419
        {
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   420
          running.partition(_.is_finished) match {
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   421
            case (Nil, Nil) =>
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   422
            case (Nil, _ :: _) => Thread.sleep(500); join(running)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   423
            case (_ :: _, remaining) => join(remaining)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   424
          }
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   425
        }
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   426
        val start_date = Date.now()
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   427
        val running =
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   428
          for (task <- tasks if !exclude_task(task.name))
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   429
            yield log_service.fork_task(start_date, task)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   430
        join(running)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   431
      })
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   432
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   433
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   434
    /* main */
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   435
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   436
    val main_start_date = Date.now()
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   437
    File.write(main_state_file, main_start_date + " " + log_service.hostname)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   438
65820
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   439
    val hg = Mercurial.repository(isabelle_repos)
a5d4958d0901 explicit history_base;
wenzelm
parents: 65810
diff changeset
   440
    val rev = hg.id()
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   441
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   442
    run(main_start_date,
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   443
      Logger_Task("isabelle_cronjob", logger =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   444
        run_now(
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
   445
          SEQ(List(build_release, build_history_base,
65783
d3d5cb2d6866 pick isabelle_version based on build_log database;
wenzelm
parents: 65771
diff changeset
   446
            PAR(remote_builds.map(seq =>
65915
49f61e2f5a02 proper index;
wenzelm
parents: 65908
diff changeset
   447
              SEQ(
49f61e2f5a02 proper index;
wenzelm
parents: 65908
diff changeset
   448
                for {
49f61e2f5a02 proper index;
wenzelm
parents: 65908
diff changeset
   449
                  (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
66864
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   450
                  (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, r.history_base_filter(hg))
5cb8ccc46e3e support for AFP versions;
wenzelm
parents: 66861
diff changeset
   451
                } yield remote_build_history(isabelle_rev, afp_rev, i, r)))),
65666
45d0692bb019 incremental download of Jenkins log files, which are also added to database;
wenzelm
parents: 65647
diff changeset
   452
            Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
65770
fb8a7962f2ae clarified modules;
wenzelm
parents: 65768
diff changeset
   453
            Logger_Task("build_log_database",
fb8a7962f2ae clarified modules;
wenzelm
parents: 65768
diff changeset
   454
              logger => Isabelle_Devel.build_log_database(logger.options)),
fb8a7962f2ae clarified modules;
wenzelm
parents: 65768
diff changeset
   455
            Logger_Task("build_status",
65793
96b4799a2e04 more robust update of generated directory;
wenzelm
parents: 65789
diff changeset
   456
              logger => Isabelle_Devel.build_status(logger.options)))))))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   457
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   458
    log_service.shutdown()
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   459
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   460
    main_state_file.file.delete
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   461
  }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   462
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   463
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   464
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   465
  /** command line entry point **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   466
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   467
  def main(args: Array[String])
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   468
  {
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   469
    Command_Line.tool0 {
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   470
      var force = false
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   471
      var verbose = false
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   472
      var exclude_task = Set.empty[String]
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   473
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   474
      val getopts = Getopts("""
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   475
Usage: Admin/cronjob/main [OPTIONS]
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   476
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   477
  Options are:
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   478
    -f           apply force to do anything
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   479
    -v           verbose
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   480
    -x NAME      exclude tasks with this name
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   481
""",
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   482
        "f" -> (_ => force = true),
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   483
        "v" -> (_ => verbose = true),
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   484
        "x:" -> (arg => exclude_task += arg))
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   485
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   486
      val more_args = getopts(args)
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   487
      if (more_args.nonEmpty) getopts.usage()
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   488
64909
8007f10195af tuned signature;
wenzelm
parents: 64544
diff changeset
   489
      val progress = if (verbose) new Console_Progress() else No_Progress
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   490
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   491
      if (force) cronjob(progress, exclude_task)
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   492
      else error("Need to apply force to do anything")
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   493
    }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   494
  }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   495
}