src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Wed Oct 12 19:03:35 2016 +0200 (2016-10-12)
changeset 64170 a0c2cbe2fc8e
parent 64162 03057a8fdd1f
child 64171 568cd5123952
permissions -rw-r--r--
more explicit management of tasks;
separate logger thread with exclusive access to main.log;
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@64170
    10
import scala.annotation.tailrec
wenzelm@64170
    11
import scala.collection.mutable
wenzelm@64170
    12
wenzelm@64170
    13
wenzelm@64148
    14
object Isabelle_Cronjob
wenzelm@64148
    15
{
wenzelm@64153
    16
  /** file-system state: owned by main cronjob **/
wenzelm@64153
    17
wenzelm@64153
    18
  val main_dir = Path.explode("~/cronjob")
wenzelm@64153
    19
  val run_dir = main_dir + Path.explode("run")
wenzelm@64153
    20
  val log_dir = main_dir + Path.explode("log")
wenzelm@64153
    21
wenzelm@64153
    22
  val main_state_file = run_dir + Path.explode("main.state")
wenzelm@64170
    23
  val main_log = log_dir + Path.explode("main.log")  // owned by logger
wenzelm@64153
    24
wenzelm@64153
    25
wenzelm@64154
    26
  /* managed repository clones */
wenzelm@64154
    27
wenzelm@64154
    28
  val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
wenzelm@64154
    29
  val afp_repos = main_dir + Path.explode("AFP-build_history")
wenzelm@64154
    30
wenzelm@64154
    31
  def pull_repos(root: Path): String =
wenzelm@64162
    32
  {
wenzelm@64162
    33
    val hg = Mercurial.repository(root)
wenzelm@64162
    34
    hg.pull(options = "-q")
wenzelm@64162
    35
    hg.identify("tip", options = "-i")
wenzelm@64162
    36
  }
wenzelm@64153
    37
wenzelm@64170
    38
wenzelm@64170
    39
wenzelm@64170
    40
  /** particular tasks **/
wenzelm@64170
    41
wenzelm@64170
    42
  /* identify repository snapshots */
wenzelm@64170
    43
wenzelm@64170
    44
  def isabelle_identify(start_date: Date)
wenzelm@64170
    45
  {
wenzelm@64170
    46
    val isabelle_id = pull_repos(isabelle_repos)
wenzelm@64170
    47
    val afp_id = pull_repos(afp_repos)
wenzelm@64170
    48
wenzelm@64170
    49
    val log_path = log_dir + Build_Log.log_path("isabelle_identify", start_date)
wenzelm@64170
    50
    Isabelle_System.mkdirs(log_path.dir)
wenzelm@64170
    51
    File.write(log_path,
wenzelm@64170
    52
      Library.terminate_lines(
wenzelm@64170
    53
        List("isabelle_identify: " + Build_Log.print_date(start_date),
wenzelm@64170
    54
          "",
wenzelm@64170
    55
          "Isabelle version: " + isabelle_id,
wenzelm@64170
    56
          "AFP version: " + afp_id)))
wenzelm@64170
    57
  }
wenzelm@64170
    58
wenzelm@64170
    59
wenzelm@64170
    60
wenzelm@64153
    61
  /** cronjob **/
wenzelm@64153
    62
wenzelm@64170
    63
  private class Task(val name: String, body: Date => Unit)
wenzelm@64170
    64
  {
wenzelm@64170
    65
    override def toString: String = "cronjob: " + name
wenzelm@64170
    66
wenzelm@64170
    67
    val start_date: Date = Date.now()
wenzelm@64170
    68
wenzelm@64170
    69
    private val future: Future[Unit] = Future.thread(toString) { body(start_date) }
wenzelm@64170
    70
    def is_finished: Boolean = future.is_finished
wenzelm@64170
    71
wenzelm@64170
    72
    def success: Boolean =
wenzelm@64170
    73
      future.join_result match {
wenzelm@64170
    74
        case Exn.Res(_) => true
wenzelm@64170
    75
        case Exn.Exn(_) => false
wenzelm@64170
    76
      }
wenzelm@64170
    77
  }
wenzelm@64170
    78
wenzelm@64153
    79
  def cronjob(progress: Progress)
wenzelm@64153
    80
  {
wenzelm@64170
    81
    /* check */
wenzelm@64153
    82
wenzelm@64153
    83
    val still_running =
wenzelm@64153
    84
      try { Some(File.read(main_state_file)) }
wenzelm@64153
    85
      catch { case ERROR(_) => None }
wenzelm@64153
    86
wenzelm@64153
    87
    still_running match {
wenzelm@64170
    88
      case None | Some("") =>
wenzelm@64153
    89
      case Some(running) =>
wenzelm@64153
    90
        error("Isabelle cronjob appears to be still running: " + running)
wenzelm@64153
    91
    }
wenzelm@64153
    92
wenzelm@64153
    93
wenzelm@64170
    94
    /* logger */
wenzelm@64170
    95
wenzelm@64170
    96
    val hostname = Isabelle_System.hostname()
wenzelm@64154
    97
wenzelm@64170
    98
    val logger: Consumer_Thread[String] =
wenzelm@64170
    99
      Consumer_Thread.fork("cronjob: logger", daemon = true)(
wenzelm@64170
   100
        consume = (text: String) =>
wenzelm@64170
   101
          {
wenzelm@64170
   102
            File.append(main_log, text + "\n")
wenzelm@64170
   103
            progress.echo(text)
wenzelm@64170
   104
            true
wenzelm@64170
   105
          })
wenzelm@64154
   106
wenzelm@64170
   107
    def log(date: Date, task_name: String, msg: String)
wenzelm@64170
   108
    {
wenzelm@64170
   109
      logger.send(
wenzelm@64170
   110
        "[" + Build_Log.print_date(date) + ", " + hostname + ", " + task_name + "]: " + msg)
wenzelm@64170
   111
    }
wenzelm@64170
   112
wenzelm@64170
   113
    def log_start(task: Task) { log(task.start_date, task.name, "started") }
wenzelm@64170
   114
wenzelm@64170
   115
    def log_end(end_date: Date, task: Task)
wenzelm@64170
   116
    {
wenzelm@64170
   117
      val elapsed_time = end_date.time - task.start_date.time
wenzelm@64170
   118
      val msg =
wenzelm@64170
   119
        (if (task.success) "finished" else "FAILED") +
wenzelm@64170
   120
        (if (elapsed_time.seconds < 3.0) "" else ", elapsed time " + elapsed_time.message_hms)
wenzelm@64170
   121
      log(end_date, task.name, msg)
wenzelm@64154
   122
    }
wenzelm@64154
   123
wenzelm@64154
   124
wenzelm@64170
   125
    /* manage tasks */
wenzelm@64153
   126
wenzelm@64170
   127
    def manage_tasks(task_specs: List[(String, Date => Unit)])
wenzelm@64170
   128
    {
wenzelm@64170
   129
      @tailrec def await(running: List[Task])
wenzelm@64170
   130
      {
wenzelm@64170
   131
        running.partition(_.is_finished) match {
wenzelm@64170
   132
          case (Nil, Nil) =>
wenzelm@64170
   133
          case (Nil, _ :: _) => Thread.sleep(500); await(running)
wenzelm@64170
   134
          case (finished, remaining) =>
wenzelm@64170
   135
            val end_date = Date.now()
wenzelm@64170
   136
            finished.foreach(log_end(end_date, _))
wenzelm@64170
   137
            await(remaining)
wenzelm@64170
   138
        }
wenzelm@64170
   139
      }
wenzelm@64170
   140
      await(task_specs.map({ case (name, body) => new Task(name, body) }))
wenzelm@64170
   141
    }
wenzelm@64153
   142
wenzelm@64170
   143
wenzelm@64170
   144
    /* main */
wenzelm@64170
   145
wenzelm@64170
   146
    val main_task = new Task("main", _ => ())
wenzelm@64170
   147
    File.write(main_state_file, main_task.start_date + " " + hostname)
wenzelm@64170
   148
    log_start(main_task)
wenzelm@64153
   149
wenzelm@64170
   150
    manage_tasks(List("isabelle_identify" -> isabelle_identify _))
wenzelm@64170
   151
wenzelm@64170
   152
    log_end(Date.now(), main_task)
wenzelm@64153
   153
    main_state_file.file.delete
wenzelm@64170
   154
wenzelm@64170
   155
    logger.shutdown()
wenzelm@64153
   156
  }
wenzelm@64153
   157
wenzelm@64153
   158
wenzelm@64153
   159
wenzelm@64153
   160
  /** command line entry point **/
wenzelm@64153
   161
wenzelm@64148
   162
  def main(args: Array[String])
wenzelm@64148
   163
  {
wenzelm@64148
   164
    Command_Line.tool0 {
wenzelm@64148
   165
      var force = false
wenzelm@64148
   166
      var verbose = false
wenzelm@64148
   167
wenzelm@64148
   168
      val getopts = Getopts("""
wenzelm@64148
   169
Usage: Admin/cronjob/main [OPTIONS]
wenzelm@64148
   170
wenzelm@64148
   171
  Options are:
wenzelm@64148
   172
    -f           apply force to do anything
wenzelm@64148
   173
    -v           verbose
wenzelm@64148
   174
""",
wenzelm@64148
   175
        "f" -> (_ => force = true),
wenzelm@64148
   176
        "v" -> (_ => verbose = true))
wenzelm@64148
   177
wenzelm@64148
   178
      val more_args = getopts(args)
wenzelm@64148
   179
      if (more_args.nonEmpty) getopts.usage()
wenzelm@64148
   180
wenzelm@64153
   181
      val progress = if (verbose) new Console_Progress() else Ignore_Progress
wenzelm@64148
   182
wenzelm@64153
   183
      if (force) cronjob(progress)
wenzelm@64153
   184
      else error("Need to apply force to do anything")
wenzelm@64148
   185
    }
wenzelm@64148
   186
  }
wenzelm@64148
   187
}