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