src/Pure/Admin/isabelle_cronjob.scala
changeset 64153 769791954872
parent 64148 bbf43b7c4d0d
child 64154 e5cf40a54b1e
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 20:20:32 2016 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 21:48:56 2016 +0200
     1.3 @@ -9,6 +9,64 @@
     1.4  
     1.5  object Isabelle_Cronjob
     1.6  {
     1.7 +  /** file-system state: owned by main cronjob **/
     1.8 +
     1.9 +  val main_dir = Path.explode("~/cronjob")
    1.10 +  val run_dir = main_dir + Path.explode("run")
    1.11 +  val log_dir = main_dir + Path.explode("log")
    1.12 +
    1.13 +  val main_state_file = run_dir + Path.explode("main.state")
    1.14 +  val main_log = log_dir + Path.explode("main.log")
    1.15 +
    1.16 +
    1.17 +
    1.18 +  /** cronjob **/
    1.19 +
    1.20 +  def cronjob(progress: Progress)
    1.21 +  {
    1.22 +    /* log */
    1.23 +
    1.24 +    val hostname = Isabelle_System.hostname()
    1.25 +
    1.26 +    def log(date: Date, msg: String)
    1.27 +    {
    1.28 +      val text = "[" + Build_Log.Log_File.Date_Format(date) + " " + hostname + "]: " + msg
    1.29 +      File.append(main_log, text + "\n")
    1.30 +      progress.echo(text)
    1.31 +    }
    1.32 +
    1.33 +
    1.34 +    /* start */
    1.35 +
    1.36 +    val start_date = Date.now()
    1.37 +
    1.38 +    val still_running =
    1.39 +      try { Some(File.read(main_state_file)) }
    1.40 +      catch { case ERROR(_) => None }
    1.41 +
    1.42 +    still_running match {
    1.43 +      case Some(running) =>
    1.44 +        error("Isabelle cronjob appears to be still running: " + running)
    1.45 +      case None =>
    1.46 +        File.write(main_state_file, start_date + " " + hostname)
    1.47 +        log(start_date, "start cronjob")
    1.48 +    }
    1.49 +
    1.50 +
    1.51 +    /* end */
    1.52 +
    1.53 +    val end_date = Date.now()
    1.54 +    val elapsed_time = end_date.time - start_date.time
    1.55 +
    1.56 +    log(end_date, "end cronjob, elapsed time " + elapsed_time.message_hms)
    1.57 +
    1.58 +    main_state_file.file.delete
    1.59 +  }
    1.60 +
    1.61 +
    1.62 +
    1.63 +  /** command line entry point **/
    1.64 +
    1.65    def main(args: Array[String])
    1.66    {
    1.67      Command_Line.tool0 {
    1.68 @@ -28,16 +86,10 @@
    1.69        val more_args = getopts(args)
    1.70        if (more_args.nonEmpty) getopts.usage()
    1.71  
    1.72 -      if (verbose) Output.writeln("This is the Isabelle cronjob")
    1.73 +      val progress = if (verbose) new Console_Progress() else Ignore_Progress
    1.74  
    1.75 -      val rc =
    1.76 -        if (force) {
    1.77 -          Thread.sleep(Time.seconds(30).ms)
    1.78 -          0
    1.79 -        }
    1.80 -        else { Output.warning("Need to apply force to do anything"); 1 }
    1.81 -
    1.82 -      if (rc != 0) sys.exit(rc)
    1.83 +      if (force) cronjob(progress)
    1.84 +      else error("Need to apply force to do anything")
    1.85      }
    1.86    }
    1.87  }