src/Pure/Tools/ci_api.scala
author wenzelm
Sat Oct 08 15:45:47 2016 +0200 (2016-10-08)
changeset 64106 b7ff61d50b19
parent 64082 d57c7295f601
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Pure/Tools/ci_api.scala
     2     Author:     Makarius
     3 
     4 API for Isabelle Jenkins continuous integration services.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.net.URL
    11 
    12 import scala.util.matching.Regex
    13 
    14 
    15 object CI_API
    16 {
    17   /* CI service */
    18 
    19   def root(): String =
    20     Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
    21 
    22   def invoke(url: String, args: String*): Any =
    23   {
    24     val req = url + "/api/json?" + args.mkString("&")
    25     val result = Url.read(req)
    26     try { JSON.parse(result) }
    27     catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
    28   }
    29 
    30 
    31   /* build jobs */
    32 
    33   def build_jobs(): List[String] =
    34     for {
    35       job <- JSON.array(invoke(root()), "jobs")
    36       _class <- JSON.string(job, "_class")
    37       if _class == "hudson.model.FreeStyleProject"
    38       name <- JSON.string(job, "name")
    39     } yield name
    40 
    41   sealed case class Job_Info(
    42     job_name: String,
    43     timestamp: Long,
    44     output: URL,
    45     session_logs: List[(String, URL)])
    46   {
    47     def read_main_log(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
    48     def read_session_log(name: String): Build_Log.Log_File =
    49       Build_Log.Log_File(name,
    50         session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
    51   }
    52 
    53   def build_job_builds(job_name: String): List[Job_Info] =
    54   {
    55     val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
    56 
    57     for {
    58       build <- JSON.array(
    59         invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
    60       number <- JSON.int(build, "number")
    61       timestamp <- JSON.long(build, "timestamp")
    62     } yield {
    63       val job_prefix = root() + "/job/" + job_name + "/" + number
    64       val output = Url(job_prefix + "/consoleText")
    65       val session_logs =
    66         for {
    67           artifact <- JSON.array(build, "artifacts")
    68           log_path <- JSON.string(artifact, "relativePath")
    69           session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
    70         } yield (session -> Url(job_prefix + "/artifact/" + log_path))
    71       Job_Info(job_name, timestamp, output, session_logs)
    72     }
    73   }
    74 }