src/Pure/Admin/jenkins.scala
author wenzelm
Mon, 01 May 2017 10:05:02 +0200
changeset 65655 1b84d4109215
parent 65654 0fbaa9286331
child 65656 c266f045258b
permissions -rw-r--r--
clarified signature;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65650
48ef286b847b clarified modules;
wenzelm
parents: 64545
diff changeset
     1
/*  Title:      Pure/Admin/jenkins.scala
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     3
65650
48ef286b847b clarified modules;
wenzelm
parents: 64545
diff changeset
     4
Support for Jenkins continuous integration service.
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     5
*/
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     6
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     7
package isabelle
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     8
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     9
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    10
import java.net.URL
65652
349999526df3 more informative log_filename;
wenzelm
parents: 65651
diff changeset
    11
import java.time.ZoneId
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    12
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    13
import scala.util.matching.Regex
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    14
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    15
65650
48ef286b847b clarified modules;
wenzelm
parents: 64545
diff changeset
    16
object Jenkins
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    17
{
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    18
  /* server API */
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    19
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    20
  def root(): String =
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    21
    Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    22
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    23
  def invoke(url: String, args: String*): Any =
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    24
  {
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    25
    val req = url + "/api/json?" + args.mkString("&")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    26
    val result = Url.read(req)
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    27
    try { JSON.parse(result) }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    28
    catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    29
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    30
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    31
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    32
  /* build jobs */
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    33
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    34
  def build_jobs(): List[String] =
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    35
    for {
64545
25045094d7bb clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents: 64160
diff changeset
    36
      job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil)
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    37
      _class <- JSON.string(job, "_class")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    38
      if _class == "hudson.model.FreeStyleProject"
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    39
      name <- JSON.string(job, "name")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    40
    } yield name
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    41
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64045
diff changeset
    42
  sealed case class Job_Info(
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    43
    job_name: String,
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    44
    timestamp: Long,
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    45
    main_log: URL,
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    46
    session_logs: List[(String, String, URL)])
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    47
  {
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    48
    val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    49
    val log_filename: Path = Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    50
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    51
    def read_log_file(): Build_Log.Log_File =
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    52
      Build_Log.Log_File(log_filename.implode, Url.read(main_log))
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    53
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    54
    def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] =
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    55
    {
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    56
      def get_log(ext: String): Option[URL] =
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    57
        session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url })
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    58
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    59
      get_log("db") match {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    60
        case Some(url) =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    61
          Isabelle_System.with_tmp_file(session_name, "db") { database =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    62
            Bytes.write(database, Bytes.read(url))
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    63
            using(SQLite.open_database(database))(db =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    64
              store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    65
          }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    66
        case None =>
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    67
          get_log("gz") match {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    68
            case Some(url) =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    69
              val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url))
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    70
              log_file.parse_session_info(ml_statistics = true).ml_statistics
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    71
            case None => Nil
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    72
          }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    73
      }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    74
    }
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    75
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    76
65654
0fbaa9286331 tuned signature;
wenzelm
parents: 65653
diff changeset
    77
  def build_job_infos(job_name: String): List[Job_Info] =
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    78
  {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    79
    val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    80
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    81
    for {
65651
2b78b7edf072 retrieve more than just 100 builds;
wenzelm
parents: 65650
diff changeset
    82
      build <-
2b78b7edf072 retrieve more than just 100 builds;
wenzelm
parents: 65650
diff changeset
    83
        JSON.array(
2b78b7edf072 retrieve more than just 100 builds;
wenzelm
parents: 65650
diff changeset
    84
          invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
2b78b7edf072 retrieve more than just 100 builds;
wenzelm
parents: 65650
diff changeset
    85
          "allBuilds").getOrElse(Nil)
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    86
      number <- JSON.int(build, "number")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    87
      timestamp <- JSON.long(build, "timestamp")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    88
    } yield {
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    89
      val job_prefix = root() + "/job/" + job_name + "/" + number
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    90
      val main_log = Url(job_prefix + "/consoleText")
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    91
      val session_logs =
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    92
        for {
64545
25045094d7bb clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents: 64160
diff changeset
    93
          artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    94
          log_path <- JSON.string(artifact, "relativePath")
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    95
          (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    96
        } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    97
      Job_Info(job_name, timestamp, main_log, session_logs)
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    98
    }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    99
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   100
}