src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Sun, 04 Dec 2016 18:53:22 +0100
changeset 64538 5dd15fc22a53
parent 64506 b3ccfd59097d
child 64544 d23b7c9b9dd4
permissions -rw-r--r--
back to isabelle-dev repository;
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")
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    26
64236
358f9ff08681 discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
wenzelm
parents: 64235
diff changeset
    27
  val isabelle_dev_source = "http://isabelle.in.tum.de/repos/isabelle"
358f9ff08681 discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
wenzelm
parents: 64235
diff changeset
    28
  val isabelle_release_source = "http://bitbucket.org/isabelle_project/isabelle-release"
358f9ff08681 discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
wenzelm
parents: 64235
diff changeset
    29
  val afp_source = "https://bitbucket.org/isa-afp/afp-devel"
358f9ff08681 discontinued somewhat pointless cronjob.options -- compile-time constants are sufficient;
wenzelm
parents: 64235
diff changeset
    30
64218
f318cb6ba511 publish directly on webspace;
wenzelm
parents: 64215
diff changeset
    31
  val release_snapshot = Path.explode("~/html-data/release_snapshot")
64215
123e6dcd3852 cronjob: build release from repository snapshot;
wenzelm
parents: 64199
diff changeset
    32
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    33
64192
wenzelm
parents: 64187
diff changeset
    34
wenzelm
parents: 64187
diff changeset
    35
  /** particular tasks **/
wenzelm
parents: 64187
diff changeset
    36
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    37
  /* identify Isabelle + AFP repository snapshots and build release */
64192
wenzelm
parents: 64187
diff changeset
    38
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    39
  private val build_release =
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    40
    Logger_Task("build_release", logger =>
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    41
      Isabelle_System.with_tmp_dir("isadist")(base_dir =>
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    42
        {
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    43
          val rev = Mercurial.repository(isabelle_repos).id()
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    44
          val afp_rev = Mercurial.setup_repository(afp_source, afp_repos).id()
64192
wenzelm
parents: 64187
diff changeset
    45
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    46
          File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    47
            terminate_lines(
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    48
              List("isabelle_identify: " + Build_Log.print_date(logger.start_date),
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    49
                "",
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    50
                "Isabelle version: " + rev,
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    51
                "AFP version: " + afp_rev)))
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    52
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    53
          val new_snapshot = release_snapshot.ext("new")
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    54
          val old_snapshot = release_snapshot.ext("old")
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    55
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    56
          Isabelle_System.rm_tree(new_snapshot)
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    57
          Isabelle_System.rm_tree(old_snapshot)
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    58
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    59
          Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    60
            parallel_jobs = 4, remote_mac = "macbroy31", website = Some(new_snapshot))
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    61
64482
43f6c28ff496 clarified File.move: target directory like File.copy;
wenzelm
parents: 64481
diff changeset
    62
          if (release_snapshot.is_dir) File.move(release_snapshot, old_snapshot)
43f6c28ff496 clarified File.move: target directory like File.copy;
wenzelm
parents: 64481
diff changeset
    63
          File.move(new_snapshot, release_snapshot)
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    64
          Isabelle_System.rm_tree(old_snapshot)
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
    65
        }))
64192
wenzelm
parents: 64187
diff changeset
    66
wenzelm
parents: 64187
diff changeset
    67
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    68
  /* integrity test of build_history vs. build_history_base */
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    69
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    70
  private val build_history_base =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    71
    Logger_Task("build_history_base", logger =>
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    72
      {
64251
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    73
        val hg =
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    74
          Mercurial.setup_repository(
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    75
            File.standard_path(isabelle_repos), isabelle_repos_test)
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    76
        for {
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    77
          (result, log_path) <-
64251
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    78
            Build_History.build_history(
528381eb8a7b proper setup of fresh repository;
wenzelm
parents: 64237
diff changeset
    79
              hg, 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
    80
        } {
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    81
          result.check
64482
43f6c28ff496 clarified File.move: target directory like File.copy;
wenzelm
parents: 64481
diff changeset
    82
          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
    83
        }
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    84
      })
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    85
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    86
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    87
  /* remote build_history */
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    88
64409
70c87ca55f2c tuned signature -- more friendly for experimentation;
wenzelm
parents: 64405
diff changeset
    89
  sealed case class Remote_Build(
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    90
    host: String,
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    91
    user: String = "",
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    92
    port: Int = SSH.default_port,
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
    93
    shared_home: Boolean = true,
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    94
    options: String = "",
64351
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
    95
    args: String = "")
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    96
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    97
  private val remote_builds =
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
    98
    List(
64506
b3ccfd59097d more cronjob tasks, using Poly/ML repository version from 13-Nov-2016;
wenzelm
parents: 64482
diff changeset
    99
      List(Remote_Build("lxbroy8",
b3ccfd59097d more cronjob tasks, using Poly/ML repository version from 13-Nov-2016;
wenzelm
parents: 64482
diff changeset
   100
        options = "-m32 -B -M1x2,2 -t polyml-test -e 'init_component /home/isabelle/contrib/polyml-test-7a7b742897e9'",
b3ccfd59097d more cronjob tasks, using Poly/ML repository version from 13-Nov-2016;
wenzelm
parents: 64482
diff changeset
   101
        args = "-N -g timing")),
b3ccfd59097d more cronjob tasks, using Poly/ML repository version from 13-Nov-2016;
wenzelm
parents: 64482
diff changeset
   102
      List(Remote_Build("lxbroy9", options = "-m32 -B -M1x2,2", args = "-N -g timing")),
64476
62c807eb009f proper option for "build", not "build_history" (cf. 5ca4ac099e94);
wenzelm
parents: 64468
diff changeset
   103
      List(Remote_Build("lxbroy10", options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
64351
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   104
      List(
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   105
        Remote_Build("macbroy2", options = "-m32 -M8", args = "-a"),
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   106
        Remote_Build("macbroy2", options = "-m32 -M8 -t quick_and_dirty", args = "-a -o quick_and_dirty"),
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   107
        Remote_Build("macbroy2", options = "-m32 -M8 -t skip_proofs", args = "-a -o skip_proofs")),
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   108
      List(Remote_Build("macbroy30", options = "-m32 -M2", args = "-a")),
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   109
      List(Remote_Build("macbroy31", options = "-m32 -M2", args = "-a")),
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   110
      List(
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   111
        Remote_Build("vmnipkow9", shared_home = false, options = "-m32 -M4", args = "-a"),
e54578e699b5 more tasks;
wenzelm
parents: 64350
diff changeset
   112
        Remote_Build("vmnipkow9", shared_home = false, options = "-m64 -M4", args = "-a")))
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   113
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   114
  private def remote_build_history(rev: String, r: Remote_Build): Logger_Task =
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   115
  {
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   116
    val task_name = "build_history-" + r.host
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   117
    Logger_Task(task_name, logger =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   118
      {
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   119
        using(logger.ssh_context.open_session(host = r.host, user = r.user, port = r.port))(
64259
wenzelm
parents: 64257
diff changeset
   120
          ssh =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   121
            {
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
   122
              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
   123
              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
   124
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   125
              val (results, _) =
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   126
                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
   127
                  isabelle_repos,
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   128
                  isabelle_repos.ext(r.host),
64538
5dd15fc22a53 back to isabelle-dev repository;
wenzelm
parents: 64506
diff changeset
   129
                  isabelle_repos_source = isabelle_dev_source,
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   130
                  self_update = self_update,
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   131
                  push_isabelle_home = push_isabelle_home,
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   132
                  options =
64479
9d643c4e9403 uniform order for options and args;
wenzelm
parents: 64476
diff changeset
   133
                    "-r " + Bash.string(rev) + " -N " + Bash.string(task_name) + " -f " + r.options,
64468
ed8940d6295c back to more elementary result (see 5f49765a25ec): avoid concurrent use of ssh channel;
wenzelm
parents: 64452
diff changeset
   134
                  args = "-o timeout=10800 " + r.args)
64346
5f49765a25ec process results immediately;
wenzelm
parents: 64338
diff changeset
   135
64481
caf62923039b more logging, to see better when files written;
wenzelm
parents: 64480
diff changeset
   136
              for ((log_name, bytes) <- results) {
caf62923039b more logging, to see better when files written;
wenzelm
parents: 64480
diff changeset
   137
                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
   138
                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
   139
              }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   140
            })
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   141
      })
64294
303976a45afe shared_home is default for classic isatest home setup;
wenzelm
parents: 64277
diff changeset
   142
  }
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   143
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   144
64192
wenzelm
parents: 64187
diff changeset
   145
wenzelm
parents: 64187
diff changeset
   146
  /** task logging **/
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   147
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   148
  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   149
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64252
diff changeset
   150
  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
   151
  {
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   152
    current_log.file.delete
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   153
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   154
    private val thread: Consumer_Thread[String] =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   155
      Consumer_Thread.fork("cronjob: logger", daemon = true)(
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   156
        consume = (text: String) =>
64219
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   157
          { // critical
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   158
            File.append(current_log, text + "\n")
c1af670cbe7e clarified logs;
wenzelm
parents: 64218
diff changeset
   159
            File.append(cumulative_log, text + "\n")
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   160
            progress.echo(text)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   161
            true
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   162
          })
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   163
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   164
    def shutdown() { thread.shutdown() }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   165
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   166
    val hostname = Isabelle_System.hostname()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   167
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   168
    def log(date: Date, task_name: String, msg: String): Unit =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   169
      if (task_name != "")
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   170
        thread.send(
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   171
          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   172
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   173
    def start_logger(start_date: Date, task_name: String): Logger =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   174
      new Logger(this, start_date, task_name)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   175
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   176
    def run_task(start_date: Date, task: Logger_Task)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   177
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   178
      val logger = start_logger(start_date, task.name)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   179
      val res = Exn.capture { task.body(logger) }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   180
      val end_date = Date.now()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   181
      val err =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   182
        res match {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   183
          case Exn.Res(_) => None
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   184
          case Exn.Exn(exn) =>
64410
89da169f66fa more informative error (see 6e9c22c494c5);
wenzelm
parents: 64409
diff changeset
   185
            System.err.println("Exception trace for " + quote(task.name) + ":")
64397
6e9c22c494c5 more informative error (stderr);
wenzelm
parents: 64351
diff changeset
   186
            exn.printStackTrace()
64295
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   187
            val first_line = Library.split_lines(Exn.message(exn)).headOption getOrElse "exception"
6aefa7e66888 avoid spamming log file;
wenzelm
parents: 64294
diff changeset
   188
            Some(first_line)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   189
        }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   190
      logger.log_end(end_date, err)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   191
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   192
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   193
    def fork_task(start_date: Date, task: Logger_Task): Task =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   194
      new Task(task.name, run_task(start_date, task))
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   195
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   196
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   197
  class Logger private[Isabelle_Cronjob](
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   198
    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
   199
  {
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64252
diff changeset
   200
    def ssh_context: SSH.Context = log_service.ssh_context
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   201
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   202
    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
   203
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   204
    def log_end(end_date: Date, err: Option[String])
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   205
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   206
      val elapsed_time = end_date.time - start_date.time
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   207
      val msg =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   208
        (if (err.isEmpty) "finished" else "ERROR " + err.get) +
64197
c43dedbb8118 tuned message;
wenzelm
parents: 64195
diff changeset
   209
        (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
   210
      log(end_date, msg)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   211
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   212
64195
wenzelm
parents: 64194
diff changeset
   213
    val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
wenzelm
parents: 64194
diff changeset
   214
wenzelm
parents: 64194
diff changeset
   215
    Isabelle_System.mkdirs(log_dir)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   216
    log(start_date, "started")
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   217
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   218
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   219
  class Task private[Isabelle_Cronjob](name: String, body: => Unit)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   220
  {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   221
    private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   222
    def is_finished: Boolean = future.is_finished
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64157
diff changeset
   223
  }
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   224
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   225
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   226
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   227
  /** cronjob **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   228
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   229
  def cronjob(progress: Progress, exclude_task: Set[String])
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   230
  {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   231
    /* soft lock */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   232
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   233
    val still_running =
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   234
      try { Some(File.read(main_state_file)) }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   235
      catch { case ERROR(_) => None }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   236
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   237
    still_running match {
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   238
      case None | Some("") =>
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   239
      case Some(running) =>
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   240
        error("Isabelle cronjob appears to be still running: " + running)
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   241
    }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   242
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   243
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   244
    /* log service */
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   245
64257
9d51ac055cec tuned signature;
wenzelm
parents: 64252
diff changeset
   246
    val log_service = new Log_Service(progress, SSH.init_context(Options.init()))
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   247
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   248
    def run(start_date: Date, task: Logger_Task) { log_service.run_task(start_date, task) }
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   249
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   250
    def run_now(task: Logger_Task) { run(Date.now(), task) }
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   251
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   252
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   253
    /* structured tasks */
64184
wenzelm
parents: 64173
diff changeset
   254
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   255
    def SEQ(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   256
      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   257
        run_now(task))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   258
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   259
    def PAR(tasks: List[Logger_Task]): Logger_Task = Logger_Task(body = _ =>
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   260
      {
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   261
        @tailrec def join(running: List[Task])
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   262
        {
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   263
          running.partition(_.is_finished) match {
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   264
            case (Nil, Nil) =>
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   265
            case (Nil, _ :: _) => Thread.sleep(500); join(running)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   266
            case (_ :: _, remaining) => join(remaining)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   267
          }
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   268
        }
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   269
        val start_date = Date.now()
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   270
        val running =
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   271
          for (task <- tasks if !exclude_task(task.name))
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   272
            yield log_service.fork_task(start_date, task)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   273
        join(running)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   274
      })
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   275
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   276
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   277
    /* main */
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   278
64199
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   279
    val main_start_date = Date.now()
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   280
    File.write(main_state_file, main_start_date + " " + log_service.hostname)
f38d39c57959 clarified;
wenzelm
parents: 64198
diff changeset
   281
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64231
diff changeset
   282
    val rev = Mercurial.repository(isabelle_repos).id()
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   283
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   284
    run(main_start_date,
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   285
      Logger_Task("isabelle_cronjob", _ =>
64231
dbc8294c75d3 added remote_build_history tasks: parallel on several remote hosts;
wenzelm
parents: 64220
diff changeset
   286
        run_now(
64405
81bac77929d9 just one task to identify Isabelle + AFP repository snapshots and build release;
wenzelm
parents: 64399
diff changeset
   287
          SEQ(List(build_release, build_history_base,
64350
3af8566788e7 remote_builds has PAR-SEQ semantics of old isatest-makedist;
wenzelm
parents: 64348
diff changeset
   288
            PAR(remote_builds.map(seq => SEQ(seq.map(remote_build_history(rev, _))))))))))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   289
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   290
    log_service.shutdown()
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   291
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   292
    main_state_file.file.delete
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   293
  }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   294
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   295
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   296
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   297
  /** command line entry point **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   298
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   299
  def main(args: Array[String])
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   300
  {
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   301
    Command_Line.tool0 {
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   302
      var force = false
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   303
      var verbose = false
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   304
      var exclude_task = Set.empty[String]
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   305
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   306
      val getopts = Getopts("""
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   307
Usage: Admin/cronjob/main [OPTIONS]
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   308
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   309
  Options are:
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   310
    -f           apply force to do anything
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   311
    -v           verbose
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   312
    -x NAME      exclude tasks with this name
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   313
""",
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   314
        "f" -> (_ => force = true),
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   315
        "v" -> (_ => verbose = true),
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   316
        "x:" -> (arg => exclude_task += arg))
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   317
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   318
      val more_args = getopts(args)
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   319
      if (more_args.nonEmpty) getopts.usage()
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   320
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   321
      val progress = if (verbose) new Console_Progress() else Ignore_Progress
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   322
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   323
      if (force) cronjob(progress, exclude_task)
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   324
      else error("Need to apply force to do anything")
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   325
    }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   326
  }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   327
}