src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Thu, 13 Oct 2016 21:23:49 +0200
changeset 64197 c43dedbb8118
parent 64195 290b8ba96ecc
child 64198 351b8211aef9
permissions -rw-r--r--
tuned message;
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")
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    20
  val main_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
    21
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    22
  val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    23
  val afp_repos = main_dir + Path.explode("AFP-build_history")
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    24
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
    25
64192
wenzelm
parents: 64187
diff changeset
    26
wenzelm
parents: 64187
diff changeset
    27
  /** particular tasks **/
wenzelm
parents: 64187
diff changeset
    28
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    29
  /* identify Isabelle + AFP repository snapshots */
64192
wenzelm
parents: 64187
diff changeset
    30
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    31
  private def pull_repos(root: Path): String =
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    32
  {
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    33
    val hg = Mercurial.repository(root)
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    34
    hg.pull(options = "-q")
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    35
    hg.identify("tip", options = "-i")
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    36
  }
64192
wenzelm
parents: 64187
diff changeset
    37
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    38
  private val isabelle_identify =
64192
wenzelm
parents: 64187
diff changeset
    39
    Logger_Task("isabelle_identify", logger =>
wenzelm
parents: 64187
diff changeset
    40
      {
wenzelm
parents: 64187
diff changeset
    41
        val isabelle_id = pull_repos(isabelle_repos)
wenzelm
parents: 64187
diff changeset
    42
        val afp_id = pull_repos(afp_repos)
wenzelm
parents: 64187
diff changeset
    43
64195
wenzelm
parents: 64194
diff changeset
    44
        File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
64192
wenzelm
parents: 64187
diff changeset
    45
          terminate_lines(
wenzelm
parents: 64187
diff changeset
    46
            List("isabelle_identify: " + Build_Log.print_date(logger.start_date),
wenzelm
parents: 64187
diff changeset
    47
              "",
wenzelm
parents: 64187
diff changeset
    48
              "Isabelle version: " + isabelle_id,
wenzelm
parents: 64187
diff changeset
    49
              "AFP version: " + afp_id)))
wenzelm
parents: 64187
diff changeset
    50
      })
wenzelm
parents: 64187
diff changeset
    51
wenzelm
parents: 64187
diff changeset
    52
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    53
  /* integrity test of build_history vs. build_history_base */
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    54
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    55
  private val build_history_base =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    56
    Logger_Task("build_history_base", logger =>
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    57
      {
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    58
        for {
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    59
          (result, log_path) <-
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    60
            Build_History.build_history(Mercurial.repository(isabelle_repos),
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    61
              rev = "build_history_base", fresh = true, build_args = List("FOL"))
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    62
        } {
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    63
          result.check
64195
wenzelm
parents: 64194
diff changeset
    64
          File.copy(log_path, logger.log_dir + log_path.base)
64194
b5ada7dcceaa integrity test of build_history vs. build_history_base;
wenzelm
parents: 64193
diff changeset
    65
        }
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    66
      })
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
64192
wenzelm
parents: 64187
diff changeset
    69
wenzelm
parents: 64187
diff changeset
    70
  /** task logging **/
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    71
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    72
  sealed case class Logger_Task(name: String = "", body: Logger => Unit)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
    73
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    74
  class Log_Service private[Isabelle_Cronjob](progress: Progress)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    75
  {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    76
    private val thread: Consumer_Thread[String] =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    77
      Consumer_Thread.fork("cronjob: logger", daemon = true)(
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    78
        consume = (text: String) =>
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    79
          {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    80
            File.append(main_log, text + "\n")   // critical
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    81
            progress.echo(text)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    82
            true
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    83
          })
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    84
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    85
    def shutdown() { thread.shutdown() }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    86
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    87
    val hostname = Isabelle_System.hostname()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    88
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    89
    def log(date: Date, task_name: String, msg: String): Unit =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    90
      if (task_name != "")
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    91
        thread.send(
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
    92
          "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    93
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    94
    def start_logger(start_date: Date, task_name: String): Logger =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    95
      new Logger(this, start_date, task_name)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
    96
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    97
    def run_task(start_date: Date, task: Logger_Task)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    98
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
    99
      val logger = start_logger(start_date, task.name)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   100
      val res = Exn.capture { task.body(logger) }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   101
      val end_date = Date.now()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   102
      val err =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   103
        res match {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   104
          case Exn.Res(_) => None
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   105
          case Exn.Exn(exn) => Some(Exn.message(exn))
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   106
        }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   107
      logger.log_end(end_date, err)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   108
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   109
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   110
    def fork_task(start_date: Date, task: Logger_Task): Task =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   111
      new Task(task.name, run_task(start_date, task))
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   112
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   113
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   114
  class Logger private[Isabelle_Cronjob](
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   115
    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
   116
  {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   117
    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
   118
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   119
    def log_end(end_date: Date, err: Option[String])
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   120
    {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   121
      val elapsed_time = end_date.time - start_date.time
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   122
      val msg =
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   123
        (if (err.isEmpty) "finished" else "ERROR " + err.get) +
64197
c43dedbb8118 tuned message;
wenzelm
parents: 64195
diff changeset
   124
        (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
   125
      log(end_date, msg)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   126
    }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   127
64195
wenzelm
parents: 64194
diff changeset
   128
    val log_dir: Path = main_dir + Build_Log.log_subdir(start_date)
wenzelm
parents: 64194
diff changeset
   129
wenzelm
parents: 64194
diff changeset
   130
    Isabelle_System.mkdirs(log_dir)
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   131
    log(start_date, "started")
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   132
  }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   133
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   134
  class Task private[Isabelle_Cronjob](name: String, body: => Unit)
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   135
  {
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   136
    private val future: Future[Unit] = Future.thread("cronjob: " + name) { body }
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   137
    def is_finished: Boolean = future.is_finished
64162
03057a8fdd1f simplified: no internal state for Mercurial;
wenzelm
parents: 64157
diff changeset
   138
  }
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   139
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   140
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   141
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   142
  /** cronjob **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   143
64186
49816908ae42 support for separate sub-system options, independent of main Isabelle options;
wenzelm
parents: 64184
diff changeset
   144
  def init_options(): Options = Options.load(Path.explode("~~/Admin/cronjob/cronjob.options"))
49816908ae42 support for separate sub-system options, independent of main Isabelle options;
wenzelm
parents: 64184
diff changeset
   145
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   146
  def cronjob(progress: Progress, exclude_task: Set[String])
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   147
  {
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   148
    /* soft lock */
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   149
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   150
    val still_running =
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   151
      try { Some(File.read(main_state_file)) }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   152
      catch { case ERROR(_) => None }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   154
    still_running match {
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   155
      case None | Some("") =>
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   156
      case Some(running) =>
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   157
        error("Isabelle cronjob appears to be still running: " + running)
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   158
    }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   159
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   160
    val main_start_date = Date.now()
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   161
    val log_service = new Log_Service(progress)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   162
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   163
    File.write(main_state_file, main_start_date + " " + log_service.hostname)
64154
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   164
e5cf40a54b1e identify managed repository clones;
wenzelm
parents: 64153
diff changeset
   165
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   166
    /* run tasks */
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   167
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   168
    def run(start_date: Date, task: Logger_Task): Unit =
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   169
      log_service.run_task(start_date, task)
64184
wenzelm
parents: 64173
diff changeset
   170
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   171
    def run_sequential(tasks: Logger_Task*): Unit =
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   172
      for (task <- tasks.iterator if !exclude_task(task.name) || task.name == "")
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   173
        run(Date.now(), task)
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   174
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   175
    def run_parallel(tasks: Logger_Task*)
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   176
    {
64184
wenzelm
parents: 64173
diff changeset
   177
      @tailrec def join(running: List[Task])
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   178
      {
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   179
        running.partition(_.is_finished) match {
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   180
          case (Nil, Nil) =>
64184
wenzelm
parents: 64173
diff changeset
   181
          case (Nil, _ :: _) => Thread.sleep(500); join(running)
wenzelm
parents: 64173
diff changeset
   182
          case (_ :: _, remaining) => join(remaining)
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   183
        }
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   184
      }
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   185
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   186
      val start_date = Date.now()
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   187
      val running =
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   188
        for (task <- tasks.toList if !exclude_task(task.name))
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   189
          yield log_service.fork_task(start_date, task)
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   190
      join(running)
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   191
    }
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   192
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   193
    def SEQ(tasks: Logger_Task*): Logger_Task =
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   194
      Logger_Task(body = _ => run_sequential(tasks:_*))
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   195
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   196
    def PAR(tasks: Logger_Task*): Logger_Task =
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   197
      Logger_Task(body = _ => run_parallel(tasks:_*))
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   198
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   199
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   200
    /* main */
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   201
64193
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   202
    run(main_start_date,
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   203
      Logger_Task("isabelle_cronjob", _ =>
7a7e370e2523 clarified log_subdir vs. log_filename;
wenzelm
parents: 64192
diff changeset
   204
        run_sequential(isabelle_identify, build_history_base)))
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   205
64171
568cd5123952 clarified task logging via log service;
wenzelm
parents: 64170
diff changeset
   206
    log_service.shutdown()
64170
a0c2cbe2fc8e more explicit management of tasks;
wenzelm
parents: 64162
diff changeset
   207
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   208
    main_state_file.file.delete
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   209
  }
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   210
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   211
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   212
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   213
  /** command line entry point **/
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   214
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   215
  def main(args: Array[String])
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   216
  {
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   217
    Command_Line.tool0 {
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   218
      var force = false
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   219
      var verbose = false
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   220
      var exclude_task = Set.empty[String]
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   221
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   222
      val getopts = Getopts("""
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   223
Usage: Admin/cronjob/main [OPTIONS]
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   224
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   225
  Options are:
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   226
    -f           apply force to do anything
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   227
    -v           verbose
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   228
    -x NAME      exclude tasks with this name
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   229
""",
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   230
        "f" -> (_ => force = true),
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   231
        "v" -> (_ => verbose = true),
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   232
        "x:" -> (arg => exclude_task += arg))
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   233
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   234
      val more_args = getopts(args)
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   235
      if (more_args.nonEmpty) getopts.usage()
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   236
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   237
      val progress = if (verbose) new Console_Progress() else Ignore_Progress
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   238
64187
450e06dabdd9 allow to exclude named tasks;
wenzelm
parents: 64186
diff changeset
   239
      if (force) cronjob(progress, exclude_task)
64153
769791954872 some timing and logging, similar to old isatest.log;
wenzelm
parents: 64148
diff changeset
   240
      else error("Need to apply force to do anything")
64148
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   241
    }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   242
  }
bbf43b7c4d0d basic setup for Isabelle cronjob;
wenzelm
parents:
diff changeset
   243
}