src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Thu Mar 21 14:17:36 2019 +0100 (2 months ago)
changeset 69937 afbc075fd2da
parent 69931 31ee094dea3d
child 69952 385458b950e1
permissions -rw-r--r--
less ambitious test: lapbroy68 lacks libgmp-dev that is required for ocaml setup of zarith;
wenzelm@64148
     1
/*  Title:      Pure/Admin/isabelle_cronjob.scala
wenzelm@64148
     2
    Author:     Makarius
wenzelm@64148
     3
wenzelm@64148
     4
Main entry point for administrative cronjob at TUM.
wenzelm@64148
     5
*/
wenzelm@64148
     6
wenzelm@64148
     7
package isabelle
wenzelm@64148
     8
wenzelm@64148
     9
wenzelm@67854
    10
import java.nio.file.Files
wenzelm@67854
    11
wenzelm@64170
    12
import scala.annotation.tailrec
wenzelm@64170
    13
import scala.collection.mutable
wenzelm@64170
    14
wenzelm@64170
    15
wenzelm@64148
    16
object Isabelle_Cronjob
wenzelm@64148
    17
{
wenzelm@66897
    18
  /* global resources: owned by main cronjob */
wenzelm@64153
    19
wenzelm@67766
    20
  val backup = "lxbroy10:cronjob"
wenzelm@64153
    21
  val main_dir = Path.explode("~/cronjob")
wenzelm@64194
    22
  val main_state_file = main_dir + Path.explode("run/main.state")
wenzelm@64219
    23
  val current_log = main_dir + Path.explode("run/main.log")  // owned by log service
wenzelm@64219
    24
  val cumulative_log = main_dir + Path.explode("log/main.log")  // owned by log service
wenzelm@64153
    25
wenzelm@68650
    26
  val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle"
wenzelm@64231
    27
  val isabelle_repos = main_dir + Path.explode("isabelle")
wenzelm@64231
    28
  val afp_repos = main_dir + Path.explode("AFP")
wenzelm@64236
    29
wenzelm@66896
    30
  val build_log_dirs =
wenzelm@66896
    31
    List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
wenzelm@66896
    32
wenzelm@64153
    33
wenzelm@64192
    34
wenzelm@67752
    35
  /** logger tasks **/
wenzelm@67752
    36
wenzelm@67752
    37
  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
wenzelm@67752
    38
wenzelm@64192
    39
wenzelm@67766
    40
  /* init and exit */
wenzelm@64192
    41
wenzelm@67753
    42
  def get_rev(): String = Mercurial.repository(isabelle_repos).id()
wenzelm@67753
    43
  def get_afp_rev(): String = Mercurial.repository(afp_repos).id()
wenzelm@67753
    44
wenzelm@67752
    45
  val init =
wenzelm@67751
    46
    Logger_Task("init", logger =>
wenzelm@66859
    47
      {
wenzelm@66859
    48
        Isabelle_Devel.make_index()
wenzelm@65771
    49
wenzelm@67753
    50
        Mercurial.setup_repository(isabelle_repos_source, isabelle_repos)
wenzelm@67753
    51
        Mercurial.setup_repository(AFP.repos_source, afp_repos)
wenzelm@64192
    52
wenzelm@66859
    53
        File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
wenzelm@67753
    54
          Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
wenzelm@67766
    55
wenzelm@67766
    56
        Isabelle_System.bash(
wenzelm@67766
    57
          """rsync -a --include="*/" --include="plain_identify*" --exclude="*" """ +
wenzelm@69199
    58
            Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
wenzelm@67854
    59
wenzelm@67854
    60
        if (!Isabelle_Devel.cronjob_log.is_file)
wenzelm@67854
    61
          Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
wenzelm@67766
    62
      })
wenzelm@67766
    63
wenzelm@67766
    64
  val exit =
wenzelm@67766
    65
    Logger_Task("exit", logger =>
wenzelm@67766
    66
      {
wenzelm@67766
    67
        Isabelle_System.bash(
wenzelm@69199
    68
          "rsync -a " + File.bash_path(main_dir) + "/log/." + " " + Bash.string(backup) + "/log/.")
wenzelm@67769
    69
            .check
wenzelm@67751
    70
      })
wenzelm@67751
    71
wenzelm@67751
    72
wenzelm@67751
    73
  /* build release */
wenzelm@67751
    74
wenzelm@67752
    75
  val build_release =
wenzelm@67751
    76
    Logger_Task("build_release", logger =>
wenzelm@67751
    77
      {
wenzelm@69432
    78
        Isabelle_Devel.release_snapshot(logger.options, rev = get_rev(), afp_rev = get_afp_rev())
wenzelm@66859
    79
      })
wenzelm@64192
    80
wenzelm@64192
    81
wenzelm@64194
    82
  /* integrity test of build_history vs. build_history_base */
wenzelm@64193
    83
wenzelm@67752
    84
  val build_history_base =
wenzelm@64193
    85
    Logger_Task("build_history_base", logger =>
wenzelm@64193
    86
      {
wenzelm@67774
    87
        using(logger.ssh_context.open_session("lxbroy10"))(ssh =>
wenzelm@67774
    88
          {
wenzelm@67774
    89
            val results =
wenzelm@67774
    90
              Build_History.remote_build_history(ssh,
wenzelm@67774
    91
                isabelle_repos,
wenzelm@67774
    92
                isabelle_repos.ext("build_history_base"),
wenzelm@67774
    93
                isabelle_identifier = "cronjob_build_history",
wenzelm@67774
    94
                self_update = true,
wenzelm@67774
    95
                rev = "build_history_base",
wenzelm@67774
    96
                options = "-f",
wenzelm@67774
    97
                args = "HOL")
wenzelm@67774
    98
wenzelm@67774
    99
            for ((log_name, bytes) <- results) {
wenzelm@67774
   100
              Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
wenzelm@67774
   101
            }
wenzelm@67774
   102
          })
wenzelm@64193
   103
      })
wenzelm@64193
   104
wenzelm@64193
   105
wenzelm@64231
   106
  /* remote build_history */
wenzelm@64231
   107
wenzelm@66864
   108
  sealed case class Item(
wenzelm@66864
   109
    known: Boolean,
wenzelm@66864
   110
    isabelle_version: String,
wenzelm@66864
   111
    afp_version: Option[String],
wenzelm@66864
   112
    pull_date: Date)
wenzelm@65783
   113
  {
wenzelm@65783
   114
    def unknown: Boolean = !known
wenzelm@66864
   115
    def versions: (String, Option[String]) = (isabelle_version, afp_version)
wenzelm@66864
   116
wenzelm@66864
   117
    def known_versions(rev: String, afp_rev: Option[String]): Boolean =
wenzelm@66864
   118
      known && rev != "" && isabelle_version == rev &&
wenzelm@66864
   119
      (afp_rev.isEmpty || afp_rev.get != "" && afp_version == afp_rev.get)
wenzelm@65783
   120
  }
wenzelm@65783
   121
wenzelm@66864
   122
  def recent_items(db: SQL.Database,
wenzelm@66864
   123
    days: Int, rev: String, afp_rev: Option[String], sql: SQL.Source): List[Item] =
wenzelm@65807
   124
  {
wenzelm@66880
   125
    val afp = afp_rev.isDefined
wenzelm@65807
   126
    val select =
wenzelm@66864
   127
      Build_Log.Data.select_recent_versions(
wenzelm@66864
   128
        days = days, rev = rev, afp_rev = afp_rev, sql = "WHERE " + sql)
wenzelm@65807
   129
wenzelm@65807
   130
    db.using_statement(select)(stmt =>
wenzelm@65807
   131
      stmt.execute_query().iterator(res =>
wenzelm@65807
   132
      {
wenzelm@65807
   133
        val known = res.bool(Build_Log.Data.known)
wenzelm@65807
   134
        val isabelle_version = res.string(Build_Log.Prop.isabelle_version)
wenzelm@66880
   135
        val afp_version = if (afp) proper_string(res.string(Build_Log.Prop.afp_version)) else None
wenzelm@66880
   136
        val pull_date = res.date(Build_Log.Data.pull_date(afp))
wenzelm@66864
   137
        Item(known, isabelle_version, afp_version, pull_date)
wenzelm@65807
   138
      }).toList)
wenzelm@65807
   139
  }
wenzelm@65807
   140
wenzelm@65807
   141
  def unknown_runs(items: List[Item]): List[List[Item]] =
wenzelm@65807
   142
  {
wenzelm@65807
   143
    val (run, rest) = Library.take_prefix[Item](_.unknown, items.dropWhile(_.known))
wenzelm@65807
   144
    if (run.nonEmpty) run :: unknown_runs(rest) else Nil
wenzelm@65807
   145
  }
wenzelm@65807
   146
wenzelm@64409
   147
  sealed case class Remote_Build(
wenzelm@65764
   148
    description: String,
wenzelm@64231
   149
    host: String,
wenzelm@64231
   150
    user: String = "",
wenzelm@65594
   151
    port: Int = 0,
wenzelm@67746
   152
    ssh_host: String = "",
wenzelm@67772
   153
    ssh_permissive: Boolean = false,
wenzelm@67746
   154
    proxy_host: String = "",
wenzelm@67746
   155
    proxy_user: String = "",
wenzelm@67746
   156
    proxy_port: Int = 0,
wenzelm@67775
   157
    self_update: Boolean = false,
wenzelm@65820
   158
    historic: Boolean = false,
wenzelm@65789
   159
    history: Int = 0,
wenzelm@65820
   160
    history_base: String = "build_history_base",
wenzelm@64231
   161
    options: String = "",
wenzelm@65732
   162
    args: String = "",
wenzelm@66864
   163
    afp: Boolean = false,
wenzelm@69693
   164
    bulky: Boolean = false,
wenzelm@67075
   165
    more_hosts: List[String] = Nil,
wenzelm@67080
   166
    detect: SQL.Source = "",
wenzelm@67080
   167
    active: Boolean = true)
wenzelm@65732
   168
  {
wenzelm@67750
   169
    def ssh_session(context: SSH.Context): SSH.Session =
wenzelm@67750
   170
      context.open_session(host = proper_string(ssh_host) getOrElse host, user = user, port = port,
wenzelm@67772
   171
        proxy_host = proxy_host, proxy_user = proxy_user, proxy_port = proxy_port,
wenzelm@67772
   172
        permissive = ssh_permissive)
wenzelm@67750
   173
wenzelm@65783
   174
    def sql: SQL.Source =
wenzelm@65783
   175
      Build_Log.Prop.build_engine + " = " + SQL.string(Build_History.engine) + " AND " +
wenzelm@67075
   176
      SQL.member(Build_Log.Prop.build_host.ident, host :: more_hosts) +
wenzelm@65783
   177
      (if (detect == "") "" else " AND " + SQL.enclose(detect))
wenzelm@65783
   178
wenzelm@65747
   179
    def profile: Build_Status.Profile =
wenzelm@69693
   180
      Build_Status.Profile(description, history = history, afp = afp, bulky = bulky, sql = sql)
wenzelm@65783
   181
wenzelm@66864
   182
    def pick(
wenzelm@66864
   183
      options: Options,
wenzelm@66864
   184
      rev: String = "",
wenzelm@66865
   185
      filter: Item => Boolean = _ => true): Option[(String, Option[String])] =
wenzelm@65747
   186
    {
wenzelm@67753
   187
      val afp_rev = if (afp) Some(get_afp_rev()) else None
wenzelm@66864
   188
wenzelm@65783
   189
      val store = Build_Log.store(options)
wenzelm@65783
   190
      using(store.open_database())(db =>
wenzelm@65783
   191
      {
wenzelm@66864
   192
        def pick_days(days: Int, gap: Int): Option[(String, Option[String])] =
wenzelm@65810
   193
        {
wenzelm@66865
   194
          val items = recent_items(db, days, rev, afp_rev, sql).filter(filter)
wenzelm@66007
   195
          def runs = unknown_runs(items).filter(run => run.length >= gap)
wenzelm@65783
   196
wenzelm@66864
   197
          if (historic || items.exists(_.known_versions(rev, afp_rev))) {
wenzelm@65810
   198
            val longest_run =
wenzelm@65810
   199
              (List.empty[Item] /: runs)({ case (item1, item2) =>
wenzelm@65810
   200
                if (item1.length >= item2.length) item1 else item2
wenzelm@65810
   201
              })
wenzelm@65810
   202
            if (longest_run.isEmpty) None
wenzelm@66864
   203
            else Some(longest_run(longest_run.length / 2).versions)
wenzelm@65810
   204
          }
wenzelm@66864
   205
          else if (rev != "") Some((rev, afp_rev))
wenzelm@66864
   206
          else runs.flatten.headOption.map(_.versions)
wenzelm@65783
   207
        }
wenzelm@65810
   208
wenzelm@66007
   209
        pick_days(options.int("build_log_history") max history, 2) orElse
wenzelm@66007
   210
        pick_days(200, 5) orElse
wenzelm@66007
   211
        pick_days(2000, 1)
wenzelm@65783
   212
      })
wenzelm@65747
   213
    }
wenzelm@65732
   214
  }
wenzelm@64231
   215
wenzelm@65806
   216
  val remote_builds_old: List[Remote_Build] =
wenzelm@65806
   217
    List(
wenzelm@67608
   218
      Remote_Build("AFP", "lxbroy7",
wenzelm@69693
   219
          args = "-N -X large -X slow",
wenzelm@67608
   220
          afp = true,
wenzelm@67608
   221
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")),
wenzelm@66762
   222
      Remote_Build("Poly/ML 5.7 Linux", "lxbroy8",
wenzelm@66762
   223
        history_base = "37074e22e8be",
wenzelm@66762
   224
        options = "-m32 -B -M1x2,2 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
wenzelm@66762
   225
        args = "-N -g timing",
wenzelm@66762
   226
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7") + " AND " +
wenzelm@66762
   227
          Build_Log.Settings.ML_OPTIONS + " <> " + SQL.string("-H 500")),
wenzelm@66931
   228
      Remote_Build("Poly/ML 5.7.1 Linux", "lxbroy8",
wenzelm@66931
   229
        history_base = "a9d5b59c3e12",
wenzelm@66931
   230
        options = "-m32 -B -M1x2,2 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
wenzelm@66931
   231
        args = "-N -g timing",
wenzelm@66931
   232
        detect =
wenzelm@66931
   233
          Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
wenzelm@66931
   234
          Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
wenzelm@66762
   235
      Remote_Build("Poly/ML 5.7 Mac OS X", "macbroy2",
wenzelm@66762
   236
        history_base = "37074e22e8be",
wenzelm@66762
   237
        options = "-m32 -B -M1x4,4 -t polyml-5.7 -i 'init_component /home/isabelle/contrib/polyml-5.7'",
wenzelm@66762
   238
        args = "-a",
wenzelm@66762
   239
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7")),
wenzelm@66931
   240
      Remote_Build("Poly/ML 5.7.1 Mac OS X", "macbroy2",
wenzelm@66931
   241
        history_base = "a9d5b59c3e12",
wenzelm@66931
   242
        options = "-m32 -B -M1x4,4 -t polyml-5.7.1-pre2 -i 'init_component /home/isabelle/contrib/polyml-test-905dae2ebfda'",
wenzelm@66931
   243
        args = "-a",
wenzelm@66931
   244
        detect =
wenzelm@66931
   245
        Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre1") + " OR " +
wenzelm@66931
   246
        Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7.1-pre2")),
wenzelm@65806
   247
      Remote_Build("Poly/ML test", "lxbroy8",
wenzelm@65843
   248
        options = "-m32 -B -M1x2,2 -t polyml-test -i 'init_component /home/isabelle/contrib/polyml-5.7-20170217'",
wenzelm@65806
   249
        args = "-N -g timing",
wenzelm@65806
   250
        detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-test")),
wenzelm@65806
   251
      Remote_Build("Mac OS X 10.8 Mountain Lion", "macbroy30", options = "-m32 -M2", args = "-a",
wenzelm@65806
   252
        detect = Build_Log.Prop.build_start + " < date '2017-03-03'"))
wenzelm@65806
   253
wenzelm@66898
   254
  val remote_builds1: List[List[Remote_Build]] =
wenzelm@65732
   255
  {
wenzelm@64231
   256
    List(
wenzelm@65764
   257
      List(Remote_Build("Linux A", "lxbroy9",
wenzelm@65732
   258
        options = "-m32 -B -M1x2,2", args = "-N -g timing")),
wenzelm@65820
   259
      List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
wenzelm@65732
   260
        options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
wenzelm@68384
   261
      List(Remote_Build("Linux Benchmarks", "lxbroy5", historic = true, history = 90,
wenzelm@68385
   262
        options = "-m32 -B -M1x2,2 -t Benchmarks" +
wenzelm@68384
   263
            " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
wenzelm@69927
   264
            " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true -e ISABELLE_SMLNJ=sml" +
wenzelm@69927
   265
            " -e ISABELLE_SWIPL=swipl",
wenzelm@68384
   266
          args = "-N -a -d '~~/src/Benchmarks'",
wenzelm@68384
   267
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("Benchmarks"))),
wenzelm@64351
   268
      List(
wenzelm@67103
   269
        Remote_Build("Mac OS X", "macbroy2",
wenzelm@65906
   270
          options = "-m32 -M8" +
wenzelm@65906
   271
            " -e ISABELLE_GHC=ghc -e ISABELLE_MLTON=mlton -e ISABELLE_OCAML=ocaml" +
wenzelm@69927
   272
            " -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
wenzelm@69927
   273
            " -e ISABELLE_SMLNJ=/mnt/nfsbroy/home/smlnj/bin/sml",
wenzelm@65902
   274
          args = "-a",
wenzelm@67080
   275
          detect = Build_Log.Prop.build_tags.undefined,
wenzelm@67089
   276
          history_base = "2c0f24e927dd"),
wenzelm@67103
   277
        Remote_Build("Mac OS X, quick_and_dirty", "macbroy2",
wenzelm@65732
   278
          options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty",
wenzelm@67080
   279
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("quick_and_dirty"),
wenzelm@67089
   280
          history_base = "2c0f24e927dd"),
wenzelm@67103
   281
        Remote_Build("Mac OS X, skip_proofs", "macbroy2",
wenzelm@65732
   282
          options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs",
wenzelm@67080
   283
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("skip_proofs"),
wenzelm@67089
   284
          history_base = "2c0f24e927dd")),
wenzelm@65768
   285
      List(
wenzelm@65768
   286
        Remote_Build("Mac OS X 10.12 Sierra", "macbroy30", options = "-m32 -M2", args = "-a",
wenzelm@65768
   287
          detect = Build_Log.Prop.build_start + " > date '2017-03-03'")),
wenzelm@65768
   288
      List(Remote_Build("Mac OS X 10.10 Yosemite", "macbroy31", options = "-m32 -M2", args = "-a")),
wenzelm@69309
   289
      List(Remote_Build("Mac OS X 10.14 High Sierra", "lapbroy68", self_update = true,
wenzelm@69937
   290
        options = "-m32 -M1,2,4 -e ISABELLE_GHC_SETUP=true",
wenzelm@69309
   291
        args = "-a -d '~~/src/Benchmarks'")),
wenzelm@69245
   292
      List(Remote_Build("Mac OS X 10.14 Mojave", "lapnipkow3", self_update = true,
wenzelm@69937
   293
        options = "-m32 -M1,2 -e ISABELLE_GHC_SETUP=true",
wenzelm@69253
   294
        args = "-a -d '~~/src/Benchmarks'")),
wenzelm@64351
   295
      List(
wenzelm@67775
   296
        Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
wenzelm@65906
   297
          options = "-m32 -M4" +
wenzelm@69931
   298
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
wenzelm@65906
   299
            " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
wenzelm@65906
   300
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
wenzelm@65902
   301
          args = "-a",
wenzelm@65732
   302
          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86-windows")),
wenzelm@67775
   303
        Remote_Build("Windows", "vmnipkow9", historic = true, history = 90, self_update = true,
wenzelm@65906
   304
          options = "-m64 -M4" +
wenzelm@69931
   305
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
wenzelm@65906
   306
            " -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
wenzelm@65906
   307
            " -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
wenzelm@65902
   308
          args = "-a",
lars@68530
   309
          detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))
wenzelm@66864
   310
    ) :::
wenzelm@66864
   311
    {
wenzelm@67607
   312
      for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
wenzelm@66864
   313
      yield {
wenzelm@67075
   314
        List(Remote_Build("AFP", host = hosts.head, more_hosts = hosts.tail,
wenzelm@67568
   315
          options = "-m32 -M1x2 -t AFP -P" + n +
wenzelm@67568
   316
            " -e ISABELLE_GHC=ghc" +
wenzelm@67568
   317
            " -e ISABELLE_MLTON=mlton" +
wenzelm@69927
   318
            " -e ISABELLE_OCAML=ocaml -e ISABELLE_OCAMLC=ocamlc -e ISABELLE_OCAML_SETUP=true" +
wenzelm@67568
   319
            " -e ISABELLE_SMLNJ=/home/smlnj/bin/sml",
wenzelm@69693
   320
          args = "-N -X large -X slow",
wenzelm@66864
   321
          afp = true,
wenzelm@66864
   322
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP")))
wenzelm@66864
   323
      }
wenzelm@66864
   324
    }
wenzelm@65732
   325
  }
wenzelm@64231
   326
wenzelm@66898
   327
  val remote_builds2: List[List[Remote_Build]] =
wenzelm@66898
   328
    List(
wenzelm@66898
   329
      List(
wenzelm@69694
   330
        Remote_Build("AFP bulky", "lrzcloud1", self_update = true,
wenzelm@67868
   331
          proxy_host = "lxbroy10", proxy_user = "i21isatest",
wenzelm@67772
   332
          ssh_host = "10.155.208.96", ssh_permissive = true,
wenzelm@66898
   333
          options = "-m64 -M6 -U30000 -s10 -t AFP",
wenzelm@69693
   334
          args = "-g large -g slow",
wenzelm@66898
   335
          afp = true,
wenzelm@69693
   336
          bulky = true,
wenzelm@66898
   337
          detect = Build_Log.Prop.build_tags + " = " + SQL.string("AFP"))))
wenzelm@66898
   338
wenzelm@67752
   339
  def remote_build_history(rev: String, afp_rev: Option[String], i: Int, r: Remote_Build)
wenzelm@67752
   340
    : Logger_Task =
wenzelm@64294
   341
  {
wenzelm@64294
   342
    val task_name = "build_history-" + r.host
wenzelm@64294
   343
    Logger_Task(task_name, logger =>
wenzelm@64231
   344
      {
wenzelm@67750
   345
        using(r.ssh_session(logger.ssh_context))(ssh =>
wenzelm@67750
   346
          {
wenzelm@67750
   347
            val results =
wenzelm@67750
   348
              Build_History.remote_build_history(ssh,
wenzelm@67750
   349
                isabelle_repos,
wenzelm@67750
   350
                isabelle_repos.ext(r.host),
wenzelm@67750
   351
                isabelle_identifier = "cronjob_build_history",
wenzelm@67775
   352
                self_update = r.self_update,
wenzelm@67750
   353
                rev = rev,
wenzelm@67750
   354
                afp_rev = afp_rev,
wenzelm@67750
   355
                options =
wenzelm@67750
   356
                  " -N " + Bash.string(task_name) + (if (i < 0) "" else "_" + (i + 1).toString) +
wenzelm@69304
   357
                  " -f -h " + Bash.string(r.host) + " " + r.options,
wenzelm@67750
   358
                args = "-o timeout=10800 " + r.args)
wenzelm@64346
   359
wenzelm@67750
   360
            for ((log_name, bytes) <- results) {
wenzelm@67750
   361
              logger.log(Date.now(), log_name)
wenzelm@67750
   362
              Bytes.write(logger.log_dir + Path.explode(log_name), bytes)
wenzelm@67750
   363
            }
wenzelm@67750
   364
          })
wenzelm@64231
   365
      })
wenzelm@64294
   366
  }
wenzelm@64231
   367
wenzelm@65747
   368
  val build_status_profiles: List[Build_Status.Profile] =
wenzelm@66898
   369
    (remote_builds_old :: remote_builds1 ::: remote_builds2).flatten.map(_.profile)
wenzelm@65747
   370
wenzelm@65746
   371
wenzelm@64192
   372
wenzelm@64192
   373
  /** task logging **/
wenzelm@64171
   374
wenzelm@67752
   375
  object Log_Service
wenzelm@67752
   376
  {
wenzelm@67752
   377
    def apply(options: Options, progress: Progress = No_Progress): Log_Service =
wenzelm@67752
   378
      new Log_Service(SSH.init_context(options), progress)
wenzelm@67752
   379
  }
wenzelm@64154
   380
wenzelm@67752
   381
  class Log_Service private(val ssh_context: SSH.Context, progress: Progress)
wenzelm@64171
   382
  {
wenzelm@64219
   383
    current_log.file.delete
wenzelm@64219
   384
wenzelm@64171
   385
    private val thread: Consumer_Thread[String] =
wenzelm@64171
   386
      Consumer_Thread.fork("cronjob: logger", daemon = true)(
wenzelm@64171
   387
        consume = (text: String) =>
wenzelm@64219
   388
          { // critical
wenzelm@64219
   389
            File.append(current_log, text + "\n")
wenzelm@64219
   390
            File.append(cumulative_log, text + "\n")
wenzelm@64171
   391
            progress.echo(text)
wenzelm@64171
   392
            true
wenzelm@64171
   393
          })
wenzelm@64171
   394
wenzelm@64171
   395
    def shutdown() { thread.shutdown() }
wenzelm@64171
   396
wenzelm@64171
   397
    val hostname = Isabelle_System.hostname()
wenzelm@64171
   398
wenzelm@64171
   399
    def log(date: Date, task_name: String, msg: String): Unit =
wenzelm@64193
   400
      if (task_name != "")
wenzelm@64193
   401
        thread.send(
wenzelm@64193
   402
          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
wenzelm@64171
   403
wenzelm@64171
   404
    def start_logger(start_date: Date, task_name: String): Logger =
wenzelm@64171
   405
      new Logger(this, start_date, task_name)
wenzelm@64154
   406
wenzelm@64171
   407
    def run_task(start_date: Date, task: Logger_Task)
wenzelm@64171
   408
    {
wenzelm@64171
   409
      val logger = start_logger(start_date, task.name)
wenzelm@64171
   410
      val res = Exn.capture { task.body(logger) }
wenzelm@64171
   411
      val end_date = Date.now()
wenzelm@64171
   412
      val err =
wenzelm@64171
   413
        res match {
wenzelm@64171
   414
          case Exn.Res(_) => None
wenzelm@64295
   415
          case Exn.Exn(exn) =>
wenzelm@67178
   416
            Output.writeln("Exception trace for " + quote(task.name) + ":")
wenzelm@64397
   417
            exn.printStackTrace()
wenzelm@66923
   418
            val first_line = split_lines(Exn.message(exn)).headOption getOrElse "exception"
wenzelm@64295
   419
            Some(first_line)
wenzelm@64171
   420
        }
wenzelm@64171
   421
      logger.log_end(end_date, err)
wenzelm@64171
   422
    }
wenzelm@64171
   423
wenzelm@64171
   424
    def fork_task(start_date: Date, task: Logger_Task): Task =
wenzelm@64171
   425
      new Task(task.name, run_task(start_date, task))
wenzelm@64171
   426
  }
wenzelm@64171
   427
wenzelm@64171
   428
  class Logger private[Isabelle_Cronjob](
wenzelm@64171
   429
    val log_service: Log_Service, val start_date: Date, val task_name: String)
wenzelm@64162
   430
  {
wenzelm@64257
   431
    def ssh_context: SSH.Context = log_service.ssh_context
wenzelm@65640
   432
    def options: Options = ssh_context.options
wenzelm@64231
   433
wenzelm@64171
   434
    def log(date: Date, msg: String): Unit = log_service.log(date, task_name, msg)
wenzelm@64171
   435
wenzelm@64171
   436
    def log_end(end_date: Date, err: Option[String])
wenzelm@64171
   437
    {
wenzelm@64171
   438
      val elapsed_time = end_date.time - start_date.time
wenzelm@64171
   439
      val msg =
wenzelm@64171
   440
        (if (err.isEmpty) "finished" else "ERROR " + err.get) +
wenzelm@64197
   441
        (if (elapsed_time.seconds < 3.0) "" else " (" + elapsed_time.message_hms + " elapsed time)")
wenzelm@64171
   442
      log(end_date, msg)
wenzelm@64171
   443
    }
wenzelm@64171
   444
wenzelm@64195
   445
    val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
wenzelm@64195
   446
wenzelm@64195
   447
    Isabelle_System.mkdirs(log_dir)
wenzelm@64171
   448
    log(start_date, "started")
wenzelm@64171
   449
  }
wenzelm@64171
   450
wenzelm@64171
   451
  class Task private[Isabelle_Cronjob](name: String, body: => Unit)
wenzelm@64171
   452
  {
wenzelm@64171
   453
    private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
wenzelm@64171
   454
    def is_finished: Boolean = future.is_finished
wenzelm@64162
   455
  }
wenzelm@64153
   456
wenzelm@64170
   457
wenzelm@64170
   458
wenzelm@64153
   459
  /** cronjob **/
wenzelm@64153
   460
wenzelm@64187
   461
  def cronjob(progress: Progress, exclude_task: Set[String])
wenzelm@64153
   462
  {
wenzelm@64171
   463
    /* soft lock */
wenzelm@64153
   464
wenzelm@64153
   465
    val still_running =
wenzelm@64153
   466
      try { Some(File.read(main_state_file)) }
wenzelm@64153
   467
      catch { case ERROR(_) => None }
wenzelm@64153
   468
wenzelm@64153
   469
    still_running match {
wenzelm@64170
   470
      case None | Some("") =>
wenzelm@64153
   471
      case Some(running) =>
wenzelm@64153
   472
        error("Isabelle cronjob appears to be still running: " + running)
wenzelm@64153
   473
    }
wenzelm@64153
   474
wenzelm@64199
   475
wenzelm@64199
   476
    /* log service */
wenzelm@64199
   477
wenzelm@67752
   478
    val log_service = Log_Service(Options.init(), progress = progress)
wenzelm@64154
   479
wenzelm@64199
   480
    def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
wenzelm@64199
   481
wenzelm@64199
   482
    def run_now(task: Logger_Task) { run(Date.now(), task) }
wenzelm@64154
   483
wenzelm@64154
   484
wenzelm@64199
   485
    /* structured tasks */
wenzelm@64184
   486
wenzelm@64350
   487
    def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
wenzelm@64193
   488
      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
wenzelm@64199
   489
        run_now(task))
wenzelm@64153
   490
wenzelm@64350
   491
    def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
wenzelm@64170
   492
      {
wenzelm@64199
   493
        @tailrec def join(running: List[Task])
wenzelm@64199
   494
        {
wenzelm@64199
   495
          running.partition(_.is_finished) match {
wenzelm@64199
   496
            case (Nil, Nil) =>
wenzelm@64199
   497
            case (Nil, _ :: _) => Thread.sleep(500); join(running)
wenzelm@64199
   498
            case (_ :: _, remaining) => join(remaining)
wenzelm@64199
   499
          }
wenzelm@64170
   500
        }
wenzelm@64199
   501
        val start_date = Date.now()
wenzelm@64199
   502
        val running =
wenzelm@64350
   503
          for (task <- tasks if !exclude_task(task.name))
wenzelm@64199
   504
            yield log_service.fork_task(start_date, task)
wenzelm@64199
   505
        join(running)
wenzelm@64199
   506
      })
wenzelm@64193
   507
wenzelm@64170
   508
wenzelm@66897
   509
    /* repository structure */
wenzelm@64199
   510
wenzelm@65820
   511
    val hg = Mercurial.repository(isabelle_repos)
wenzelm@66895
   512
    val hg_graph = hg.graph()
wenzelm@67048
   513
wenzelm@66895
   514
    def history_base_filter(r: Remote_Build): Item => Boolean =
wenzelm@66895
   515
    {
wenzelm@66895
   516
      val base_rev = hg.id(r.history_base)
wenzelm@66895
   517
      val nodes = hg_graph.all_succs(List(base_rev)).toSet
wenzelm@66895
   518
      (item: Item) => nodes(item.isabelle_version)
wenzelm@66895
   519
    }
wenzelm@66895
   520
wenzelm@66897
   521
wenzelm@66897
   522
    /* main */
wenzelm@66897
   523
wenzelm@66897
   524
    val main_start_date = Date.now()
wenzelm@66897
   525
    File.write(main_state_file, main_start_date + " " + log_service.hostname)
wenzelm@66897
   526
wenzelm@64193
   527
    run(main_start_date,
wenzelm@65783
   528
      Logger_Task("isabelle_cronjob", logger =>
wenzelm@64231
   529
        run_now(
wenzelm@67766
   530
          SEQ(List(
wenzelm@67766
   531
            init,
wenzelm@67774
   532
            build_history_base,
wenzelm@67766
   533
            PAR(
wenzelm@67774
   534
              build_release ::
wenzelm@67766
   535
              List(remote_builds1, remote_builds2).map(remote_builds =>
wenzelm@66898
   536
              SEQ(List(
wenzelm@67080
   537
                PAR(remote_builds.map(_.filter(_.active)).map(seq =>
wenzelm@66898
   538
                  SEQ(
wenzelm@66898
   539
                    for {
wenzelm@66898
   540
                      (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
wenzelm@67048
   541
                      (rev, afp_rev) <- r.pick(logger.options, hg.id(), history_base_filter(r))
wenzelm@67070
   542
                    } yield remote_build_history(rev, afp_rev, i, r)))),
wenzelm@67008
   543
                Logger_Task("jenkins_logs", _ =>
wenzelm@68209
   544
                  Jenkins.download_logs(logger.options, Jenkins.build_log_jobs, main_dir)),
wenzelm@66898
   545
                Logger_Task("build_log_database",
wenzelm@66898
   546
                  logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
wenzelm@66898
   547
                Logger_Task("build_status",
wenzelm@67766
   548
                  logger => Isabelle_Devel.build_status(logger.options)))))),
wenzelm@67766
   549
            exit)))))
wenzelm@64153
   550
wenzelm@64171
   551
    log_service.shutdown()
wenzelm@64170
   552
wenzelm@64153
   553
    main_state_file.file.delete
wenzelm@64153
   554
  }
wenzelm@64153
   555
wenzelm@64153
   556
wenzelm@64153
   557
wenzelm@64153
   558
  /** command line entry point **/
wenzelm@64153
   559
wenzelm@64148
   560
  def main(args: Array[String])
wenzelm@64148
   561
  {
wenzelm@64148
   562
    Command_Line.tool0 {
wenzelm@64148
   563
      var force = false
wenzelm@64148
   564
      var verbose = false
wenzelm@64187
   565
      var exclude_task = Set.empty[String]
wenzelm@64148
   566
wenzelm@64148
   567
      val getopts = Getopts("""
wenzelm@64148
   568
Usage: Admin/cronjob/main [OPTIONS]
wenzelm@64148
   569
wenzelm@64148
   570
  Options are:
wenzelm@64148
   571
    -f           apply force to do anything
wenzelm@64148
   572
    -v           verbose
wenzelm@64187
   573
    -x NAME      exclude tasks with this name
wenzelm@64148
   574
""",
wenzelm@64148
   575
        "f" -> (_ => force = true),
wenzelm@64187
   576
        "v" -> (_ => verbose = true),
wenzelm@64187
   577
        "x:" -> (arg => exclude_task += arg))
wenzelm@64148
   578
wenzelm@64148
   579
      val more_args = getopts(args)
wenzelm@64148
   580
      if (more_args.nonEmpty) getopts.usage()
wenzelm@64148
   581
wenzelm@64909
   582
      val progress = if (verbose) new Console_Progress() else No_Progress
wenzelm@64148
   583
wenzelm@64187
   584
      if (force) cronjob(progress, exclude_task)
wenzelm@64153
   585
      else error("Need to apply force to do anything")
wenzelm@64148
   586
    }
wenzelm@64148
   587
  }
wenzelm@64148
   588
}