src/Pure/Admin/jenkins.scala
author wenzelm
Mon, 01 May 2017 11:04:33 +0200
changeset 65659 293141fb093d
parent 65658 be817b7b8354
child 65660 dfecaf0fc069
permissions -rw-r--r--
ensure canonical order: latest first;
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
65658
be817b7b8354 tuned signature;
wenzelm
parents: 65657
diff changeset
    34
  def build_job_names(): List[String] =
63646
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
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    42
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    43
  def download_logs(job_names: List[String], dir: Path)
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    44
  {
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    45
    val store = Sessions.store()
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    46
    for {
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    47
      job_name <- job_names.iterator
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    48
      info <- build_job_infos(job_name).iterator
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    49
    } info.download_log(store, dir)
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    50
  }
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    51
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    52
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    53
  /* job info */
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    54
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64045
diff changeset
    55
  sealed case class Job_Info(
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    56
    job_name: String,
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    57
    timestamp: Long,
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    58
    main_log: URL,
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    59
    session_logs: List[(String, String, URL)])
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    60
  {
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    61
    val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
65656
wenzelm
parents: 65655
diff changeset
    62
wenzelm
parents: 65655
diff changeset
    63
    def log_filename: Path =
wenzelm
parents: 65655
diff changeset
    64
      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
    65
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    66
    def read_log_file(): Build_Log.Log_File =
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    67
      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
    68
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    69
    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
    70
    {
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    71
      def get_log(ext: String): Option[URL] =
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    72
        session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url })
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    73
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    74
      get_log("db") match {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    75
        case Some(url) =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    76
          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
    77
            Bytes.write(database, Bytes.read(url))
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    78
            using(SQLite.open_database(database))(db =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    79
              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
    80
          }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    81
        case None =>
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    82
          get_log("gz") match {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    83
            case Some(url) =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    84
              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
    85
              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
    86
            case None => Nil
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    87
          }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    88
      }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    89
    }
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    90
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    91
    def download_log(store: Sessions.Store, dir: Path)
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    92
    {
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    93
      val log_dir = dir + Build_Log.log_subdir(date)
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    94
      val log_path = log_dir + log_filename
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    95
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    96
      if (!log_path.is_file) {
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    97
        val ml_statistics =
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    98
          session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    99
            read_ml_statistics(store, session_name).
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   100
              map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   101
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   102
        Isabelle_System.mkdirs(log_dir)
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   103
        File.write_xz(log_path.ext("xz"),
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   104
          terminate_lines(Url.read(main_log) ::
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   105
            ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   106
          XZ.options(6))
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   107
      }
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   108
    }
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   109
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   110
65654
0fbaa9286331 tuned signature;
wenzelm
parents: 65653
diff changeset
   111
  def build_job_infos(job_name: String): List[Job_Info] =
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   112
  {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
   113
    val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   114
65659
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   115
    val infos =
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   116
      for {
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   117
        build <-
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   118
          JSON.array(
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   119
            invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   120
            "allBuilds").getOrElse(Nil)
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   121
        number <- JSON.int(build, "number")
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   122
        timestamp <- JSON.long(build, "timestamp")
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   123
      } yield {
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   124
        val job_prefix = root() + "/job/" + job_name + "/" + number
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   125
        val main_log = Url(job_prefix + "/consoleText")
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   126
        val session_logs =
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   127
          for {
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   128
            artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   129
            log_path <- JSON.string(artifact, "relativePath")
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   130
            (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   131
          } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   132
        Job_Info(job_name, timestamp, main_log, session_logs)
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   133
      }
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   134
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   135
    infos.sortBy(info => - info.timestamp)
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   136
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   137
}