--- a/src/Pure/Admin/build_stats.scala Sun Apr 30 17:37:12 2017 +0200
+++ b/src/Pure/Admin/build_stats.scala Sun Apr 30 23:11:51 2017 +0200
@@ -24,11 +24,11 @@
elapsed_threshold: Time = default_elapsed_threshold,
ml_timing: Option[Boolean] = default_ml_timing): List[String] =
{
- val job_infos = CI_API.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
+ val job_infos = Jenkins.build_job_builds(job).sortBy(_.timestamp).reverse.take(history_length)
if (job_infos.isEmpty) error("No build infos for job " + quote(job))
val all_infos =
- Par_List.map((job_info: CI_API.Job_Info) =>
+ Par_List.map((job_info: Jenkins.Job_Info) =>
(job_info.timestamp / 1000, job_info.read_main_log.parse_build_info()), job_infos)
val all_sessions =
(Set.empty[String] /: all_infos)(
@@ -157,7 +157,7 @@
}))
val jobs = getopts(args)
- val all_jobs = CI_API.build_jobs()
+ val all_jobs = Jenkins.build_jobs()
val bad_jobs = jobs.filterNot(all_jobs.contains(_)).sorted
if (jobs.isEmpty)
--- a/src/Pure/Admin/ci_api.scala Sun Apr 30 17:37:12 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-/* Title: Pure/Admin/ci_api.scala
- Author: Makarius
-
-API for Isabelle Jenkins continuous integration services.
-*/
-
-package isabelle
-
-
-import java.net.URL
-
-import scala.util.matching.Regex
-
-
-object CI_API
-{
- /* CI service */
-
- def root(): String =
- Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
-
- def invoke(url: String, args: String*): Any =
- {
- val req = url + "/api/json?" + args.mkString("&")
- val result = Url.read(req)
- try { JSON.parse(result) }
- catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
- }
-
-
- /* build jobs */
-
- def build_jobs(): List[String] =
- for {
- job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil)
- _class <- JSON.string(job, "_class")
- if _class == "hudson.model.FreeStyleProject"
- name <- JSON.string(job, "name")
- } yield name
-
- sealed case class Job_Info(
- job_name: String,
- timestamp: Long,
- output: URL,
- session_logs: List[(String, URL)])
- {
- def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
- def read_session_log(name: String): Build_Log.Log_File =
- Build_Log.Log_File(name,
- session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
- }
-
- def build_job_builds(job_name: String): List[Job_Info] =
- {
- val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
-
- for {
- build <- JSON.array(
- invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
- .getOrElse(Nil)
- number <- JSON.int(build, "number")
- timestamp <- JSON.long(build, "timestamp")
- } yield {
- val job_prefix = root() + "/job/" + job_name + "/" + number
- val output = Url(job_prefix + "/consoleText")
- val session_logs =
- for {
- artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
- log_path <- JSON.string(artifact, "relativePath")
- session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
- } yield (session -> Url(job_prefix + "/artifact/" + log_path))
- Job_Info(job_name, timestamp, output, session_logs)
- }
- }
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/jenkins.scala Sun Apr 30 23:11:51 2017 +0200
@@ -0,0 +1,75 @@
+/* Title: Pure/Admin/jenkins.scala
+ Author: Makarius
+
+Support for Jenkins continuous integration service.
+*/
+
+package isabelle
+
+
+import java.net.URL
+
+import scala.util.matching.Regex
+
+
+object Jenkins
+{
+ /* CI service */
+
+ def root(): String =
+ Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
+
+ def invoke(url: String, args: String*): Any =
+ {
+ val req = url + "/api/json?" + args.mkString("&")
+ val result = Url.read(req)
+ try { JSON.parse(result) }
+ catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
+ }
+
+
+ /* build jobs */
+
+ def build_jobs(): List[String] =
+ for {
+ job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil)
+ _class <- JSON.string(job, "_class")
+ if _class == "hudson.model.FreeStyleProject"
+ name <- JSON.string(job, "name")
+ } yield name
+
+ sealed case class Job_Info(
+ job_name: String,
+ timestamp: Long,
+ output: URL,
+ session_logs: List[(String, URL)])
+ {
+ def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
+ def read_session_log(name: String): Build_Log.Log_File =
+ Build_Log.Log_File(name,
+ session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
+ }
+
+ def build_job_builds(job_name: String): List[Job_Info] =
+ {
+ val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
+
+ for {
+ build <- JSON.array(
+ invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
+ .getOrElse(Nil)
+ number <- JSON.int(build, "number")
+ timestamp <- JSON.long(build, "timestamp")
+ } yield {
+ val job_prefix = root() + "/job/" + job_name + "/" + number
+ val output = Url(job_prefix + "/consoleText")
+ val session_logs =
+ for {
+ artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
+ log_path <- JSON.string(artifact, "relativePath")
+ session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
+ } yield (session -> Url(job_prefix + "/artifact/" + log_path))
+ Job_Info(job_name, timestamp, output, session_logs)
+ }
+ }
+}
--- a/src/Pure/build-jars Sun Apr 30 17:37:12 2017 +0200
+++ b/src/Pure/build-jars Sun Apr 30 23:11:51 2017 +0200
@@ -19,9 +19,9 @@
Admin/build_release.scala
Admin/build_stats.scala
Admin/check_sources.scala
- Admin/ci_api.scala
Admin/ci_profile.scala
Admin/isabelle_cronjob.scala
+ Admin/jenkins.scala
Admin/news.scala
Admin/other_isabelle.scala
Admin/remote_dmg.scala