# HG changeset patch # User wenzelm # Date 1476215336 -7200 # Node ID 7697919548721c72957f58dfce590a5be419ae82 # Parent 8f5b23536c56f3ba52c7a3bbd41e242f1925d4f9 some timing and logging, similar to old isatest.log; diff -r 8f5b23536c56 -r 769791954872 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 11 21:44:20 2016 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Tue Oct 11 21:48:56 2016 +0200 @@ -9,6 +9,64 @@ object Isabelle_Cronjob { + /** file-system state: owned by main cronjob **/ + + val main_dir = Path.explode("~/cronjob") + val run_dir = main_dir + Path.explode("run") + val log_dir = main_dir + Path.explode("log") + + val main_state_file = run_dir + Path.explode("main.state") + val main_log = log_dir + Path.explode("main.log") + + + + /** cronjob **/ + + def cronjob(progress: Progress) + { + /* log */ + + val hostname = Isabelle_System.hostname() + + def log(date: Date, msg: String) + { + val text = "[" + Build_Log.Log_File.Date_Format(date) + " " + hostname + "]: " + msg + File.append(main_log, text + "\n") + progress.echo(text) + } + + + /* start */ + + val start_date = Date.now() + + val still_running = + try { Some(File.read(main_state_file)) } + catch { case ERROR(_) => None } + + still_running match { + case Some(running) => + error("Isabelle cronjob appears to be still running: " + running) + case None => + File.write(main_state_file, start_date + " " + hostname) + log(start_date, "start cronjob") + } + + + /* end */ + + val end_date = Date.now() + val elapsed_time = end_date.time - start_date.time + + log(end_date, "end cronjob, elapsed time " + elapsed_time.message_hms) + + main_state_file.file.delete + } + + + + /** command line entry point **/ + def main(args: Array[String]) { Command_Line.tool0 { @@ -28,16 +86,10 @@ val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() - if (verbose) Output.writeln("This is the Isabelle cronjob") + val progress = if (verbose) new Console_Progress() else Ignore_Progress - val rc = - if (force) { - Thread.sleep(Time.seconds(30).ms) - 0 - } - else { Output.warning("Need to apply force to do anything"); 1 } - - if (rc != 0) sys.exit(rc) + if (force) cronjob(progress) + else error("Need to apply force to do anything") } } }