1 /* Title: Pure/Admin/jenkins.scala |
|
2 Author: Makarius |
|
3 |
|
4 Support for Jenkins continuous integration service. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.net.URL |
|
11 |
|
12 import scala.util.matching.Regex |
|
13 |
|
14 |
|
15 object Jenkins { |
|
16 /* server API */ |
|
17 |
|
18 def root(): String = |
|
19 Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT") |
|
20 |
|
21 def invoke(url: String, args: String*): Any = { |
|
22 val req = url + "/api/json?" + args.mkString("&") |
|
23 val result = Url.read(req) |
|
24 try { JSON.parse(result) } |
|
25 catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) } |
|
26 } |
|
27 |
|
28 |
|
29 /* build jobs */ |
|
30 |
|
31 def build_job_names(): List[String] = |
|
32 for { |
|
33 job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil) |
|
34 _class <- JSON.string(job, "_class") |
|
35 if _class == "hudson.model.FreeStyleProject" |
|
36 name <- JSON.string(job, "name") |
|
37 } yield name |
|
38 |
|
39 |
|
40 def download_logs( |
|
41 options: Options, |
|
42 job_names: List[String], |
|
43 dir: Path, |
|
44 progress: Progress = new Progress |
|
45 ): Unit = { |
|
46 val store = Sessions.store(options) |
|
47 val infos = job_names.flatMap(build_job_infos) |
|
48 Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos) |
|
49 } |
|
50 |
|
51 |
|
52 /* build log status */ |
|
53 |
|
54 val build_log_jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow") |
|
55 |
|
56 val build_status_profiles: List[Build_Status.Profile] = |
|
57 build_log_jobs.map(job_name => |
|
58 Build_Status.Profile("jenkins " + job_name, |
|
59 sql = |
|
60 Build_Log.Prop.build_engine.toString + " = " + SQL.string(Build_Log.Jenkins.engine) + |
|
61 " AND " + Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " + |
|
62 Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) + |
|
63 " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name))) |
|
64 |
|
65 |
|
66 /* job info */ |
|
67 |
|
68 sealed case class Job_Info( |
|
69 job_name: String, |
|
70 timestamp: Long, |
|
71 main_log: URL, |
|
72 session_logs: List[(String, String, URL)] |
|
73 ) { |
|
74 val date: Date = Date(Time.ms(timestamp), Date.timezone_berlin) |
|
75 |
|
76 def log_filename: Path = |
|
77 Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name)) |
|
78 |
|
79 def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] = { |
|
80 def get_log(ext: String): Option[URL] = |
|
81 session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url }) |
|
82 |
|
83 get_log("db") match { |
|
84 case Some(url) => |
|
85 Isabelle_System.with_tmp_file(session_name, "db") { database => |
|
86 Bytes.write(database, Bytes.read(url)) |
|
87 using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name)) |
|
88 } |
|
89 case None => |
|
90 get_log("gz") match { |
|
91 case Some(url) => |
|
92 val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url)) |
|
93 log_file.parse_session_info(ml_statistics = true).ml_statistics |
|
94 case None => Nil |
|
95 } |
|
96 } |
|
97 } |
|
98 |
|
99 def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress): Unit = { |
|
100 val log_dir = dir + Build_Log.log_subdir(date) |
|
101 val log_path = log_dir + log_filename.xz |
|
102 |
|
103 if (!log_path.is_file) { |
|
104 progress.echo(File.standard_path(log_path)) |
|
105 Isabelle_System.make_directory(log_dir) |
|
106 |
|
107 val ml_statistics = |
|
108 session_logs.map(_._1).distinct.sorted.flatMap(session_name => |
|
109 read_ml_statistics(store, session_name). |
|
110 map(props => (Build_Log.SESSION_NAME -> session_name) :: props)) |
|
111 |
|
112 File.write_xz(log_path, |
|
113 terminate_lines(Url.read(main_log) :: |
|
114 ml_statistics.map(Protocol.ML_Statistics_Marker.apply)), |
|
115 Compress.Options_XZ(6)) |
|
116 } |
|
117 } |
|
118 } |
|
119 |
|
120 def build_job_infos(job_name: String): List[Job_Info] = { |
|
121 val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""") |
|
122 |
|
123 val infos = |
|
124 for { |
|
125 build <- |
|
126 JSON.array( |
|
127 invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"), |
|
128 "allBuilds").getOrElse(Nil) |
|
129 number <- JSON.int(build, "number") |
|
130 timestamp <- JSON.long(build, "timestamp") |
|
131 } yield { |
|
132 val job_prefix = root() + "/job/" + job_name + "/" + number |
|
133 val main_log = Url(job_prefix + "/consoleText") |
|
134 val session_logs = |
|
135 for { |
|
136 artifact <- JSON.array(build, "artifacts").getOrElse(Nil) |
|
137 log_path <- JSON.string(artifact, "relativePath") |
|
138 (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None }) |
|
139 } yield (name, ext, Url(job_prefix + "/artifact/" + log_path)) |
|
140 Job_Info(job_name, timestamp, main_log, session_logs) |
|
141 } |
|
142 |
|
143 infos.sortBy(info => - info.timestamp) |
|
144 } |
|
145 } |
|