# HG changeset patch # User wenzelm # Date 1493586711 -7200 # Node ID 48ef286b847bb4d4b299e5cfd0803ecfaae27b1f # Parent 0818da4f67bb6234c8c5aa38bc17e72a4c2dbadc clarified modules; diff -r 0818da4f67bb -r 48ef286b847b src/Pure/Admin/build_stats.scala --- 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) diff -r 0818da4f67bb -r 48ef286b847b src/Pure/Admin/ci_api.scala --- 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) - } - } -} diff -r 0818da4f67bb -r 48ef286b847b src/Pure/Admin/jenkins.scala --- /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) + } + } +} diff -r 0818da4f67bb -r 48ef286b847b src/Pure/build-jars --- 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