author | wenzelm |
Sat, 06 May 2017 19:23:33 +0200 | |
changeset 65743 | 4847ca570454 |
parent 65736 | 2e7230b66a32 |
child 65747 | 5a3052b2095f |
permissions | -rw-r--r-- |
65650 | 1 |
/* Title: Pure/Admin/jenkins.scala |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
3 |
|
65650 | 4 |
Support for Jenkins continuous integration service. |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
6 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
8 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
9 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
10 |
import java.net.URL |
65652 | 11 |
import java.time.ZoneId |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
12 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
13 |
import scala.util.matching.Regex |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
14 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
15 |
|
65650 | 16 |
object Jenkins |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
17 |
{ |
65653
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
18 |
/* server API */ |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
19 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
20 |
def root(): String = |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
21 |
Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
22 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
23 |
def invoke(url: String, args: String*): Any = |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
24 |
{ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
25 |
val req = url + "/api/json?" + args.mkString("&") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
26 |
val result = Url.read(req) |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
27 |
try { JSON.parse(result) } |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
28 |
catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) } |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
29 |
} |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
30 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
31 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
32 |
/* build jobs */ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
33 |
|
65658 | 34 |
def build_job_names(): List[String] = |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
35 |
for { |
64545
25045094d7bb
clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents:
64160
diff
changeset
|
36 |
job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil) |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
37 |
_class <- JSON.string(job, "_class") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
38 |
if _class == "hudson.model.FreeStyleProject" |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
39 |
name <- JSON.string(job, "name") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
40 |
} yield name |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
41 |
|
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
42 |
|
65660 | 43 |
def download_logs(job_names: List[String], dir: Path, progress: Progress = No_Progress) |
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
44 |
{ |
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
45 |
val store = Sessions.store() |
65662 | 46 |
val infos = job_names.flatMap(build_job_infos(_)) |
47 |
Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos) |
|
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
48 |
} |
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
49 |
|
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
50 |
|
65736 | 51 |
/* build log profiles */ |
52 |
||
53 |
val build_log_jobs = List("isabelle-nightly-benchmark") |
|
54 |
||
65743 | 55 |
val build_log_profiles: List[Build_Status.Profile] = |
65736 | 56 |
build_log_jobs.map(job_name => |
65743 | 57 |
Build_Status.Profile("jenkins_" + job_name, |
65736 | 58 |
Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " + |
59 |
Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name))) |
|
60 |
||
61 |
||
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
62 |
/* job info */ |
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
63 |
|
64054 | 64 |
sealed case class Job_Info( |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
65 |
job_name: String, |
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
66 |
identify: Boolean, |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
67 |
timestamp: Long, |
65655 | 68 |
main_log: URL, |
65653
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
69 |
session_logs: List[(String, String, URL)]) |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
70 |
{ |
65655 | 71 |
val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin")) |
65656 | 72 |
|
73 |
def log_filename: Path = |
|
74 |
Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name)) |
|
65653
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
75 |
|
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
76 |
def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] = |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
77 |
{ |
65655 | 78 |
def get_log(ext: String): Option[URL] = |
79 |
session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url }) |
|
80 |
||
81 |
get_log("db") match { |
|
65653
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
82 |
case Some(url) => |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
83 |
Isabelle_System.with_tmp_file(session_name, "db") { database => |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
84 |
Bytes.write(database, Bytes.read(url)) |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
85 |
using(SQLite.open_database(database))(db => |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
86 |
store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
87 |
} |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
88 |
case None => |
65655 | 89 |
get_log("gz") match { |
65653
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
90 |
case Some(url) => |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
91 |
val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url)) |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
92 |
log_file.parse_session_info(ml_statistics = true).ml_statistics |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
93 |
case None => Nil |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
94 |
} |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
95 |
} |
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
96 |
} |
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
97 |
|
65660 | 98 |
def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress) |
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
99 |
{ |
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
100 |
val log_dir = dir + Build_Log.log_subdir(date) |
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
101 |
val log_path = log_dir + (if (identify) log_filename else log_filename.ext("xz")) |
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
102 |
|
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
103 |
if (!log_path.is_file) { |
65660 | 104 |
progress.echo(log_path.expand.implode) |
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
105 |
Isabelle_System.mkdirs(log_dir) |
65660 | 106 |
|
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
107 |
if (identify) { |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
108 |
val log_file = Build_Log.Log_File(main_log.toString, Url.read(main_log)) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
109 |
val isabelle_version = log_file.find_match(Build_Log.Jenkins.Isabelle_Version) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
110 |
val afp_version = log_file.find_match(Build_Log.Jenkins.AFP_Version) |
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
111 |
|
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
112 |
File.write(log_path, |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
113 |
Build_Log.Identify.content(date, isabelle_version, afp_version) + "\n" + |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
114 |
main_log.toString) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
115 |
} |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
116 |
else { |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
117 |
val ml_statistics = |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
118 |
session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name => |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
119 |
read_ml_statistics(store, session_name). |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
120 |
map(props => (Build_Log.SESSION_NAME -> session_name) :: props)) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
121 |
|
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
122 |
File.write_xz(log_path, |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
123 |
terminate_lines(Url.read(main_log) :: |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
124 |
ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))), |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
125 |
XZ.options(6)) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
126 |
} |
65657
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
127 |
} |
2773b6859c55
download Jenkins logs with inlined ml_statistics;
wenzelm
parents:
65656
diff
changeset
|
128 |
} |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
129 |
} |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
130 |
|
65654 | 131 |
def build_job_infos(job_name: String): List[Job_Info] = |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
132 |
{ |
65653
f433c0e73307
read ml_statistics from session logs: .db or .gz files;
wenzelm
parents:
65652
diff
changeset
|
133 |
val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""") |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
134 |
|
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
135 |
val identify = job_name == "identify" |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
136 |
val job = if (identify) "isabelle-nightly-slow" else job_name |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
137 |
|
65659 | 138 |
val infos = |
139 |
for { |
|
140 |
build <- |
|
141 |
JSON.array( |
|
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
142 |
invoke(root() + "/job/" + job, "tree=allBuilds[number,timestamp,artifacts[*]]"), |
65659 | 143 |
"allBuilds").getOrElse(Nil) |
144 |
number <- JSON.int(build, "number") |
|
145 |
timestamp <- JSON.long(build, "timestamp") |
|
146 |
} yield { |
|
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
147 |
val job_prefix = root() + "/job/" + job + "/" + number |
65659 | 148 |
val main_log = Url(job_prefix + "/consoleText") |
149 |
val session_logs = |
|
65674
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
150 |
if (identify) Nil |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
151 |
else { |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
152 |
for { |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
153 |
artifact <- JSON.array(build, "artifacts").getOrElse(Nil) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
154 |
log_path <- JSON.string(artifact, "relativePath") |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
155 |
(name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None }) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
156 |
} yield (name, ext, Url(job_prefix + "/artifact/" + log_path)) |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
157 |
} |
23897f5d885d
approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents:
65662
diff
changeset
|
158 |
Job_Info(job_name, identify, timestamp, main_log, session_logs) |
65659 | 159 |
} |
160 |
||
161 |
infos.sortBy(info => - info.timestamp) |
|
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
162 |
} |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
163 |
} |