src/Pure/Admin/isabelle_cronjob.scala
author wenzelm
Tue Oct 11 22:14:26 2016 +0200 (2016-10-11)
changeset 64154 e5cf40a54b1e
parent 64153 769791954872
child 64155 646c4d6a6a02
permissions -rw-r--r--
identify managed repository clones;
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@64154
    22
  /* managed repository clones */
wenzelm@64154
    23
wenzelm@64154
    24
  val isabelle_repos = main_dir + Path.explode("isabelle-build_history")
wenzelm@64154
    25
  val afp_repos = main_dir + Path.explode("AFP-build_history")
wenzelm@64154
    26
wenzelm@64154
    27
  def pull_repos(root: Path): String =
wenzelm@64154
    28
    using(Mercurial.open_repository(root))(hg =>
wenzelm@64154
    29
      {
wenzelm@64154
    30
        hg.pull(options = "-q")
wenzelm@64154
    31
        hg.identify("tip")
wenzelm@64154
    32
      })
wenzelm@64154
    33
wenzelm@64153
    34
wenzelm@64153
    35
  /** cronjob **/
wenzelm@64153
    36
wenzelm@64153
    37
  def cronjob(progress: Progress)
wenzelm@64153
    38
  {
wenzelm@64153
    39
    /* log */
wenzelm@64153
    40
wenzelm@64153
    41
    val hostname = Isabelle_System.hostname()
wenzelm@64153
    42
wenzelm@64153
    43
    def log(date: Date, msg: String)
wenzelm@64153
    44
    {
wenzelm@64153
    45
      val text = "[" + Build_Log.Log_File.Date_Format(date) + " " + hostname + "]: " + msg
wenzelm@64153
    46
      File.append(main_log, text + "\n")
wenzelm@64153
    47
      progress.echo(text)
wenzelm@64153
    48
    }
wenzelm@64153
    49
wenzelm@64153
    50
wenzelm@64153
    51
    /* start */
wenzelm@64153
    52
wenzelm@64153
    53
    val start_date = Date.now()
wenzelm@64153
    54
wenzelm@64153
    55
    val still_running =
wenzelm@64153
    56
      try { Some(File.read(main_state_file)) }
wenzelm@64153
    57
      catch { case ERROR(_) => None }
wenzelm@64153
    58
wenzelm@64153
    59
    still_running match {
wenzelm@64153
    60
      case Some(running) =>
wenzelm@64153
    61
        error("Isabelle cronjob appears to be still running: " + running)
wenzelm@64153
    62
      case None =>
wenzelm@64153
    63
        File.write(main_state_file, start_date + " " + hostname)
wenzelm@64153
    64
        log(start_date, "start cronjob")
wenzelm@64153
    65
    }
wenzelm@64153
    66
wenzelm@64153
    67
wenzelm@64154
    68
    /* identify repository snapshots */
wenzelm@64154
    69
wenzelm@64154
    70
    {
wenzelm@64154
    71
      val pull_date = Date.now()
wenzelm@64154
    72
wenzelm@64154
    73
      val isabelle_id = pull_repos(isabelle_repos)
wenzelm@64154
    74
      val afp_id = pull_repos(afp_repos)
wenzelm@64154
    75
wenzelm@64154
    76
      val log_path = log_dir + Build_Log.log_path("isabelle_identify", pull_date)
wenzelm@64154
    77
      Isabelle_System.mkdirs(log_path.dir)
wenzelm@64154
    78
      File.write(log_path,
wenzelm@64154
    79
        Library.terminate_lines(
wenzelm@64154
    80
          List("isabelle_identify: " + Build_Log.Log_File.Date_Format(pull_date),
wenzelm@64154
    81
            "",
wenzelm@64154
    82
            "Isabelle version: " + isabelle_id,
wenzelm@64154
    83
            "AFP version: " + afp_id)))
wenzelm@64154
    84
    }
wenzelm@64154
    85
wenzelm@64154
    86
wenzelm@64153
    87
    /* end */
wenzelm@64153
    88
wenzelm@64153
    89
    val end_date = Date.now()
wenzelm@64153
    90
    val elapsed_time = end_date.time - start_date.time
wenzelm@64153
    91
wenzelm@64153
    92
    log(end_date, "end cronjob, elapsed time " + elapsed_time.message_hms)
wenzelm@64153
    93
wenzelm@64153
    94
    main_state_file.file.delete
wenzelm@64153
    95
  }
wenzelm@64153
    96
wenzelm@64153
    97
wenzelm@64153
    98
wenzelm@64153
    99
  /** command line entry point **/
wenzelm@64153
   100
wenzelm@64148
   101
  def main(args: Array[String])
wenzelm@64148
   102
  {
wenzelm@64148
   103
    Command_Line.tool0 {
wenzelm@64148
   104
      var force = false
wenzelm@64148
   105
      var verbose = false
wenzelm@64148
   106
wenzelm@64148
   107
      val getopts = Getopts("""
wenzelm@64148
   108
Usage: Admin/cronjob/main [OPTIONS]
wenzelm@64148
   109
wenzelm@64148
   110
  Options are:
wenzelm@64148
   111
    -f           apply force to do anything
wenzelm@64148
   112
    -v           verbose
wenzelm@64148
   113
""",
wenzelm@64148
   114
        "f" -> (_ => force = true),
wenzelm@64148
   115
        "v" -> (_ => verbose = true))
wenzelm@64148
   116
wenzelm@64148
   117
      val more_args = getopts(args)
wenzelm@64148
   118
      if (more_args.nonEmpty) getopts.usage()
wenzelm@64148
   119
wenzelm@64153
   120
      val progress = if (verbose) new Console_Progress() else Ignore_Progress
wenzelm@64148
   121
wenzelm@64153
   122
      if (force) cronjob(progress)
wenzelm@64153
   123
      else error("Need to apply force to do anything")
wenzelm@64148
   124
    }
wenzelm@64148
   125
  }
wenzelm@64148
   126
}