src/Pure/Tools/ci_api.scala
author wenzelm
Tue Oct 04 19:26:19 2016 +0200 (2016-10-04)
changeset 64041 fd454d9e97c4
parent 63992 3aa9837d05c7
child 64042 6957bd29a950
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 Build_Info(
    42     job_name: String,
    43     timestamp: Long,
    44     output: URL,
    45     session_logs: List[(String, URL)])
    46   {
    47     def read_output(): String = Url.read(output)
    48     def read_log(name: String, full: Boolean): Build.Session_Log_Info =
    49     {
    50       val text =
    51         session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse ""
    52       Build.parse_session_log(split_lines(text), full)
    53     }
    54   }
    55 
    56   def build_job_builds(job_name: String): List[Build_Info] =
    57   {
    58     val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
    59 
    60     for {
    61       build <- JSON.array(
    62         invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
    63       number <- JSON.int(build, "number")
    64       timestamp <- JSON.long(build, "timestamp")
    65     } yield {
    66       val job_prefix = root() + "/job/" + job_name + "/" + number
    67       val output = Url(job_prefix + "/consoleText")
    68       val session_logs =
    69         for {
    70           artifact <- JSON.array(build, "artifacts")
    71           log_path <- JSON.string(artifact, "relativePath")
    72           session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
    73         } yield (session -> Url(job_prefix + "/artifact/" + log_path))
    74       Build_Info(job_name, timestamp, output, session_logs)
    75     }
    76   }
    77 }