author | wenzelm |
Tue, 04 Oct 2016 21:11:35 +0200 | |
changeset 64045 | c6160d0b0337 |
parent 64042 | 6957bd29a950 |
child 64054 | 1fc9ab31720d |
permissions | -rw-r--r-- |
63992 | 1 |
/* Title: Pure/Tools/ci_api.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 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
4 |
API for Isabelle Jenkins continuous integration services. |
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 |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
11 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
12 |
import scala.util.matching.Regex |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
13 |
|
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 |
object CI_API |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
16 |
{ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
17 |
/* CI service */ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
18 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
19 |
def root(): String = |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
20 |
Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
21 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
22 |
def invoke(url: String, args: String*): Any = |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
23 |
{ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
24 |
val req = url + "/api/json?" + args.mkString("&") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
25 |
val result = Url.read(req) |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
26 |
try { JSON.parse(result) } |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
27 |
catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) } |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
28 |
} |
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 |
/* build jobs */ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
32 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
33 |
def build_jobs(): List[String] = |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
34 |
for { |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
35 |
job <- JSON.array(invoke(root()), "jobs") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
36 |
_class <- JSON.string(job, "_class") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
37 |
if _class == "hudson.model.FreeStyleProject" |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
38 |
name <- JSON.string(job, "name") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
39 |
} yield name |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
40 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
41 |
sealed case class Build_Info( |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
42 |
job_name: String, |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
43 |
timestamp: Long, |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
44 |
output: URL, |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
45 |
session_logs: List[(String, URL)]) |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
46 |
{ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
47 |
def read_output(): String = Url.read(output) |
64045 | 48 |
def read_log(name: String, full: Boolean): Build_Log.Session_Info = |
64041 | 49 |
{ |
50 |
val text = |
|
51 |
session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "" |
|
64045 | 52 |
Build_Log.parse_session_info(name, split_lines(text), full) |
64041 | 53 |
} |
63646
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
54 |
} |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
55 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
56 |
def build_job_builds(job_name: String): List[Build_Info] = |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
57 |
{ |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
58 |
val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
59 |
|
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
60 |
for { |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
61 |
build <- JSON.array( |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
62 |
invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
63 |
number <- JSON.int(build, "number") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
64 |
timestamp <- JSON.long(build, "timestamp") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
65 |
} yield { |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
66 |
val job_prefix = root() + "/job/" + job_name + "/" + number |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
67 |
val output = Url(job_prefix + "/consoleText") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
68 |
val session_logs = |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
69 |
for { |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
70 |
artifact <- JSON.array(build, "artifacts") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
71 |
log_path <- JSON.string(artifact, "relativePath") |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
72 |
session <- (log_path match { case Log_Session(name) => Some(name) case _ => None }) |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
73 |
} yield (session -> Url(job_prefix + "/artifact/" + log_path)) |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
74 |
Build_Info(job_name, timestamp, output, session_logs) |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
75 |
} |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
76 |
} |
74604a9fc4c8
API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff
changeset
|
77 |
} |