src/Pure/Tools/ci_api.scala
author wenzelm
Fri Oct 07 13:58:10 2016 +0200 (2016-10-07)
changeset 64082 d57c7295f601
parent 64062 a7352cbde7d7
child 64106 b7ff61d50b19
permissions -rw-r--r--
clarified 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@64054
    41
  sealed case class Job_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@64062
    47
    def read_output(): Build_Log.Log_File = Build_Log.Log_File(job_name, Url.read(output))
wenzelm@64082
    48
    def read_log_file(name: String): Build_Log.Log_File =
wenzelm@64082
    49
      Build_Log.Log_File(name,
wenzelm@64082
    50
        session_logs.collectFirst({ case (a, b) if a == name => Url.read_gzip(b) }) getOrElse "")
wenzelm@63646
    51
  }
wenzelm@63646
    52
wenzelm@64054
    53
  def build_job_builds(job_name: String): List[Job_Info] =
wenzelm@63646
    54
  {
wenzelm@63646
    55
    val Log_Session = new Regex("""^.*/log/([^/]+)\.gz$""")
wenzelm@63646
    56
wenzelm@63646
    57
    for {
wenzelm@63646
    58
      build <- JSON.array(
wenzelm@63646
    59
        invoke(root() + "/job/" + job_name, "tree=builds[number,timestamp,artifacts[*]]"), "builds")
wenzelm@63646
    60
      number <- JSON.int(build, "number")
wenzelm@63646
    61
      timestamp <- JSON.long(build, "timestamp")
wenzelm@63646
    62
    } yield {
wenzelm@63646
    63
      val job_prefix = root() + "/job/" + job_name + "/" + number
wenzelm@63646
    64
      val output = Url(job_prefix + "/consoleText")
wenzelm@63646
    65
      val session_logs =
wenzelm@63646
    66
        for {
wenzelm@63646
    67
          artifact <- JSON.array(build, "artifacts")
wenzelm@63646
    68
          log_path <- JSON.string(artifact, "relativePath")
wenzelm@63646
    69
          session <- (log_path match { case Log_Session(name) => Some(name) case _ => None })
wenzelm@63646
    70
        } yield (session -> Url(job_prefix + "/artifact/" + log_path))
wenzelm@64054
    71
      Job_Info(job_name, timestamp, output, session_logs)
wenzelm@63646
    72
    }
wenzelm@63646
    73
  }
wenzelm@63646
    74
}