author | wenzelm |
Wed, 12 Oct 2016 11:31:08 +0200 | |
changeset 64162 | 03057a8fdd1f |
parent 64157 | 3e4400f21310 |
child 64170 | a0c2cbe2fc8e |
permissions | -rw-r--r-- |
64148 | 1 |
/* Title: Pure/Admin/isabelle_cronjob.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Main entry point for administrative cronjob at TUM. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
object Isabelle_Cronjob |
|
11 |
{ |
|
64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
12 |
/** file-system state: owned by main cronjob **/ |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
13 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
14 |
val main_dir = Path.explode("~/cronjob") |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
15 |
val run_dir = main_dir + Path.explode("run") |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
16 |
val log_dir = main_dir + Path.explode("log") |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
17 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
18 |
val main_state_file = run_dir + Path.explode("main.state") |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
19 |
val main_log = log_dir + Path.explode("main.log") |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
20 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
21 |
|
64154 | 22 |
/* managed repository clones */ |
23 |
||
24 |
val isabelle_repos = main_dir + Path.explode("isabelle-build_history") |
|
25 |
val afp_repos = main_dir + Path.explode("AFP-build_history") |
|
26 |
||
27 |
def pull_repos(root: Path): String = |
|
64162 | 28 |
{ |
29 |
val hg = Mercurial.repository(root) |
|
30 |
hg.pull(options = "-q") |
|
31 |
hg.identify("tip", options = "-i") |
|
32 |
} |
|
64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
33 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
34 |
/** cronjob **/ |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
35 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
36 |
def cronjob(progress: Progress) |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
37 |
{ |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
38 |
/* log */ |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
39 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
40 |
val hostname = Isabelle_System.hostname() |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
41 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
42 |
def log(date: Date, msg: String) |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
43 |
{ |
64156 | 44 |
val text = "[" + Build_Log.print_date(date) + ", " + hostname + "]: " + msg |
64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
45 |
File.append(main_log, text + "\n") |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
46 |
progress.echo(text) |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
47 |
} |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
48 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
49 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
50 |
/* start */ |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
51 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
52 |
val start_date = Date.now() |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
53 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
54 |
val still_running = |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
55 |
try { Some(File.read(main_state_file)) } |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
56 |
catch { case ERROR(_) => None } |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
57 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
58 |
still_running match { |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
59 |
case Some(running) => |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
60 |
error("Isabelle cronjob appears to be still running: " + running) |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
61 |
case None => |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
62 |
File.write(main_state_file, start_date + " " + hostname) |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
63 |
log(start_date, "start cronjob") |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
64 |
} |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
65 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
66 |
|
64154 | 67 |
/* identify repository snapshots */ |
68 |
||
69 |
{ |
|
70 |
val pull_date = Date.now() |
|
71 |
||
72 |
val isabelle_id = pull_repos(isabelle_repos) |
|
73 |
val afp_id = pull_repos(afp_repos) |
|
74 |
||
75 |
val log_path = log_dir + Build_Log.log_path("isabelle_identify", pull_date) |
|
76 |
Isabelle_System.mkdirs(log_path.dir) |
|
77 |
File.write(log_path, |
|
78 |
Library.terminate_lines( |
|
64155 | 79 |
List("isabelle_identify: " + Build_Log.print_date(pull_date), |
64154 | 80 |
"", |
81 |
"Isabelle version: " + isabelle_id, |
|
82 |
"AFP version: " + afp_id))) |
|
83 |
} |
|
84 |
||
85 |
||
64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
86 |
/* end */ |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
87 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
88 |
val end_date = Date.now() |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
89 |
val elapsed_time = end_date.time - start_date.time |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
90 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
91 |
log(end_date, "end cronjob, elapsed time " + elapsed_time.message_hms) |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
92 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
93 |
main_state_file.file.delete |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
94 |
} |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
95 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
96 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
97 |
|
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
98 |
/** command line entry point **/ |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
99 |
|
64148 | 100 |
def main(args: Array[String]) |
101 |
{ |
|
102 |
Command_Line.tool0 { |
|
103 |
var force = false |
|
104 |
var verbose = false |
|
105 |
||
106 |
val getopts = Getopts(""" |
|
107 |
Usage: Admin/cronjob/main [OPTIONS] |
|
108 |
||
109 |
Options are: |
|
110 |
-f apply force to do anything |
|
111 |
-v verbose |
|
112 |
""", |
|
113 |
"f" -> (_ => force = true), |
|
114 |
"v" -> (_ => verbose = true)) |
|
115 |
||
116 |
val more_args = getopts(args) |
|
117 |
if (more_args.nonEmpty) getopts.usage() |
|
118 |
||
64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
119 |
val progress = if (verbose) new Console_Progress() else Ignore_Progress |
64148 | 120 |
|
64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
121 |
if (force) cronjob(progress) |
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset
|
122 |
else error("Need to apply force to do anything") |
64148 | 123 |
} |
124 |
} |
|
125 |
} |