src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Tue Oct 11 21:48:56 2016 +0200 (2016-10-11)
changeset 64153 769791954872
parent 64148 bbf43b7c4d0d
child 64154 e5cf40a54b1e
permissions -rw-r--r--
some timing and logging, similar to old isatest.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@64148
    10
object Isabelle_Cronjob
wenzelm@64148
    11
{
wenzelm@64153
    12
  /** file-system state: owned by main cronjob **/
wenzelm@64153
    13
wenzelm@64153
    14
  val main_dir = Path.explode("~/cronjob")
wenzelm@64153
    15
  val run_dir = main_dir + Path.explode("run")
wenzelm@64153
    16
  val log_dir = main_dir + Path.explode("log")
wenzelm@64153
    17
wenzelm@64153
    18
  val main_state_file = run_dir + Path.explode("main.state")
wenzelm@64153
    19
  val main_log = log_dir + Path.explode("main.log")
wenzelm@64153
    20
wenzelm@64153
    21
wenzelm@64153
    22
wenzelm@64153
    23
  /** cronjob **/
wenzelm@64153
    24
wenzelm@64153
    25
  def cronjob(progress: Progress)
wenzelm@64153
    26
  {
wenzelm@64153
    27
    /* log */
wenzelm@64153
    28
wenzelm@64153
    29
    val hostname = Isabelle_System.hostname()
wenzelm@64153
    30
wenzelm@64153
    31
    def log(date: Date, msg: String)
wenzelm@64153
    32
    {
wenzelm@64153
    33
      val text = "[" + Build_Log.Log_File.Date_Format(date) + " " + hostname + "]: " + msg
wenzelm@64153
    34
      File.append(main_log, text + "\n")
wenzelm@64153
    35
      progress.echo(text)
wenzelm@64153
    36
    }
wenzelm@64153
    37
wenzelm@64153
    38
wenzelm@64153
    39
    /* start */
wenzelm@64153
    40
wenzelm@64153
    41
    val start_date = Date.now()
wenzelm@64153
    42
wenzelm@64153
    43
    val still_running =
wenzelm@64153
    44
      try { Some(File.read(main_state_file)) }
wenzelm@64153
    45
      catch { case ERROR(_) => None }
wenzelm@64153
    46
wenzelm@64153
    47
    still_running match {
wenzelm@64153
    48
      case Some(running) =>
wenzelm@64153
    49
        error("Isabelle cronjob appears to be still running: " + running)
wenzelm@64153
    50
      case None =>
wenzelm@64153
    51
        File.write(main_state_file, start_date + " " + hostname)
wenzelm@64153
    52
        log(start_date, "start cronjob")
wenzelm@64153
    53
    }
wenzelm@64153
    54
wenzelm@64153
    55
wenzelm@64153
    56
    /* end */
wenzelm@64153
    57
wenzelm@64153
    58
    val end_date = Date.now()
wenzelm@64153
    59
    val elapsed_time = end_date.time - start_date.time
wenzelm@64153
    60
wenzelm@64153
    61
    log(end_date, "end cronjob, elapsed time " + elapsed_time.message_hms)
wenzelm@64153
    62
wenzelm@64153
    63
    main_state_file.file.delete
wenzelm@64153
    64
  }
wenzelm@64153
    65
wenzelm@64153
    66
wenzelm@64153
    67
wenzelm@64153
    68
  /** command line entry point **/
wenzelm@64153
    69
wenzelm@64148
    70
  def main(args: Array[String])
wenzelm@64148
    71
  {
wenzelm@64148
    72
    Command_Line.tool0 {
wenzelm@64148
    73
      var force = false
wenzelm@64148
    74
      var verbose = false
wenzelm@64148
    75
wenzelm@64148
    76
      val getopts = Getopts("""
wenzelm@64148
    77
Usage: Admin/cronjob/main [OPTIONS]
wenzelm@64148
    78
wenzelm@64148
    79
  Options are:
wenzelm@64148
    80
    -f           apply force to do anything
wenzelm@64148
    81
    -v           verbose
wenzelm@64148
    82
""",
wenzelm@64148
    83
        "f" -> (_ => force = true),
wenzelm@64148
    84
        "v" -> (_ => verbose = true))
wenzelm@64148
    85
wenzelm@64148
    86
      val more_args = getopts(args)
wenzelm@64148
    87
      if (more_args.nonEmpty) getopts.usage()
wenzelm@64148
    88
wenzelm@64153
    89
      val progress = if (verbose) new Console_Progress() else Ignore_Progress
wenzelm@64148
    90
wenzelm@64153
    91
      if (force) cronjob(progress)
wenzelm@64153
    92
      else error("Need to apply force to do anything")
wenzelm@64148
    93
    }
wenzelm@64148
    94
  }
wenzelm@64148
    95
}