author  wenzelm 
Tue, 11 Oct 2016 22:24:47 +0200  
changeset 64156  01716e3c3e68 
parent 64155  646c4d6a6a02 
child 64157  3e4400f21310 
permissions  rwrr 
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 
/** filesystem 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("isabellebuild_history") 

25 
val afp_repos = main_dir + Path.explode("AFPbuild_history") 

26 

27 
def pull_repos(root: Path): String = 

28 
using(Mercurial.open_repository(root))(hg => 

29 
{ 

30 
hg.pull(options = "q") 

31 
hg.identify("tip") 

32 
}) 

33 

64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

34 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

35 
/** cronjob **/ 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

36 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

37 
def cronjob(progress: Progress) 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

38 
{ 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

39 
/* log */ 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

40 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

41 
val hostname = Isabelle_System.hostname() 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

42 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

43 
def log(date: Date, msg: String) 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

44 
{ 
64156  45 
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

46 
File.append(main_log, text + "\n") 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

47 
progress.echo(text) 
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 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

51 
/* start */ 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

52 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

53 
val start_date = Date.now() 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

54 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

55 
val still_running = 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

56 
try { Some(File.read(main_state_file)) } 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

57 
catch { case ERROR(_) => None } 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

58 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

59 
still_running match { 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

60 
case Some(running) => 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

61 
error("Isabelle cronjob appears to be still running: " + running) 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

62 
case None => 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

63 
File.write(main_state_file, start_date + " " + hostname) 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

64 
log(start_date, "start cronjob") 
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 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

67 

64154  68 
/* identify repository snapshots */ 
69 

70 
{ 

71 
val pull_date = Date.now() 

72 

73 
val isabelle_id = pull_repos(isabelle_repos) 

74 
val afp_id = pull_repos(afp_repos) 

75 

76 
val log_path = log_dir + Build_Log.log_path("isabelle_identify", pull_date) 

77 
Isabelle_System.mkdirs(log_path.dir) 

78 
File.write(log_path, 

79 
Library.terminate_lines( 

64155  80 
List("isabelle_identify: " + Build_Log.print_date(pull_date), 
64154  81 
"", 
82 
"Isabelle version: " + isabelle_id, 

83 
"AFP version: " + afp_id))) 

84 
} 

85 

86 

64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

87 
/* end */ 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

88 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

89 
val end_date = Date.now() 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

90 
val elapsed_time = end_date.time  start_date.time 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

91 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

92 
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

93 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

94 
main_state_file.file.delete 
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 

769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

99 
/** command line entry point **/ 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

100 

64148  101 
def main(args: Array[String]) 
102 
{ 

103 
Command_Line.tool0 { 

104 
var force = false 

105 
var verbose = false 

106 

107 
val getopts = Getopts(""" 

108 
Usage: Admin/cronjob/main [OPTIONS] 

109 

110 
Options are: 

111 
f apply force to do anything 

112 
v verbose 

113 
""", 

114 
"f" > (_ => force = true), 

115 
"v" > (_ => verbose = true)) 

116 

117 
val more_args = getopts(args) 

118 
if (more_args.nonEmpty) getopts.usage() 

119 

64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

120 
val progress = if (verbose) new Console_Progress() else Ignore_Progress 
64148  121 

64153
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

122 
if (force) cronjob(progress) 
769791954872
some timing and logging, similar to old isatest.log;
wenzelm
parents:
64148
diff
changeset

123 
else error("Need to apply force to do anything") 
64148  124 
} 
125 
} 

126 
} 