src/Pure/Admin/jenkins.scala
author wenzelm
Mon Mar 25 16:45:08 2019 +0100 (3 months ago)
changeset 69980 f2e3adfd916f
parent 68209 aeffd8f1f079
permissions -rw-r--r--
tuned signature;
wenzelm@65650
     1
/*  Title:      Pure/Admin/jenkins.scala
wenzelm@63646
     2
    Author:     Makarius
wenzelm@63646
     3
wenzelm@65650
     4
Support for Jenkins continuous integration service.
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@65650
    15
object Jenkins
wenzelm@63646
    16
{
wenzelm@65653
    17
  /* server API */
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@65658
    33
  def build_job_names(): List[String] =
wenzelm@63646
    34
    for {
wenzelm@64545
    35
      job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil)
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@65657
    41
wenzelm@68209
    42
  def download_logs(
wenzelm@68209
    43
    options: Options, job_names: List[String], dir: Path, progress: Progress = No_Progress)
wenzelm@65657
    44
  {
wenzelm@68209
    45
    val store = Sessions.store(options)
wenzelm@65662
    46
    val infos = job_names.flatMap(build_job_infos(_))
wenzelm@65662
    47
    Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos)
wenzelm@65657
    48
  }
wenzelm@65657
    49
wenzelm@65657
    50
wenzelm@65747
    51
  /* build log status */
wenzelm@65736
    52
wenzelm@65788
    53
  val build_log_jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
wenzelm@65736
    54
wenzelm@65747
    55
  val build_status_profiles: List[Build_Status.Profile] =
wenzelm@65736
    56
    build_log_jobs.map(job_name =>
wenzelm@66880
    57
      Build_Status.Profile("jenkins " + job_name,
wenzelm@66880
    58
        sql =
wenzelm@66880
    59
          Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
wenzelm@66880
    60
          Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
wenzelm@66880
    61
          Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
wenzelm@66880
    62
          " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
wenzelm@65736
    63
wenzelm@65736
    64
wenzelm@65657
    65
  /* job info */
wenzelm@65657
    66
wenzelm@64054
    67
  sealed case class Job_Info(
wenzelm@63646
    68
    job_name: String,
wenzelm@63646
    69
    timestamp: Long,
wenzelm@65655
    70
    main_log: URL,
wenzelm@65653
    71
    session_logs: List[(String, String, URL)])
wenzelm@63646
    72
  {
wenzelm@69980
    73
    val date: Date = Date(Time.ms(timestamp), Date.timezone_berlin)
wenzelm@65656
    74
wenzelm@65656
    75
    def log_filename: Path =
wenzelm@65656
    76
      Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
wenzelm@65653
    77
wenzelm@65653
    78
    def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] =
wenzelm@65653
    79
    {
wenzelm@65655
    80
      def get_log(ext: String): Option[URL] =
wenzelm@65655
    81
        session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url })
wenzelm@65655
    82
wenzelm@65655
    83
      get_log("db") match {
wenzelm@65653
    84
        case Some(url) =>
wenzelm@65653
    85
          Isabelle_System.with_tmp_file(session_name, "db") { database =>
wenzelm@65653
    86
            Bytes.write(database, Bytes.read(url))
wenzelm@65935
    87
            using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name))
wenzelm@65653
    88
          }
wenzelm@65653
    89
        case None =>
wenzelm@65655
    90
          get_log("gz") match {
wenzelm@65653
    91
            case Some(url) =>
wenzelm@65653
    92
              val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url))
wenzelm@65653
    93
              log_file.parse_session_info(ml_statistics = true).ml_statistics
wenzelm@65653
    94
            case None => Nil
wenzelm@65653
    95
          }
wenzelm@65653
    96
      }
wenzelm@65653
    97
    }
wenzelm@65657
    98
wenzelm@65660
    99
    def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
wenzelm@65657
   100
    {
wenzelm@65657
   101
      val log_dir = dir + Build_Log.log_subdir(date)
wenzelm@67008
   102
      val log_path = log_dir + log_filename.ext("xz")
wenzelm@65657
   103
wenzelm@65657
   104
      if (!log_path.is_file) {
wenzelm@65660
   105
        progress.echo(log_path.expand.implode)
wenzelm@65674
   106
        Isabelle_System.mkdirs(log_dir)
wenzelm@65660
   107
wenzelm@67008
   108
        val ml_statistics =
wenzelm@67008
   109
          session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
wenzelm@67008
   110
            read_ml_statistics(store, session_name).
wenzelm@67008
   111
              map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
wenzelm@65657
   112
wenzelm@67008
   113
        File.write_xz(log_path,
wenzelm@67008
   114
          terminate_lines(Url.read(main_log) ::
wenzelm@67008
   115
            ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
wenzelm@67008
   116
          XZ.options(6))
wenzelm@65657
   117
      }
wenzelm@65657
   118
    }
wenzelm@63646
   119
  }
wenzelm@63646
   120
wenzelm@65654
   121
  def build_job_infos(job_name: String): List[Job_Info] =
wenzelm@63646
   122
  {
wenzelm@65653
   123
    val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
wenzelm@63646
   124
wenzelm@65659
   125
    val infos =
wenzelm@65659
   126
      for {
wenzelm@65659
   127
        build <-
wenzelm@65659
   128
          JSON.array(
wenzelm@67008
   129
            invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
wenzelm@65659
   130
            "allBuilds").getOrElse(Nil)
wenzelm@65659
   131
        number <- JSON.int(build, "number")
wenzelm@65659
   132
        timestamp <- JSON.long(build, "timestamp")
wenzelm@65659
   133
      } yield {
wenzelm@67008
   134
        val job_prefix = root() + "/job/" + job_name + "/" + number
wenzelm@65659
   135
        val main_log = Url(job_prefix + "/consoleText")
wenzelm@65659
   136
        val session_logs =
wenzelm@67008
   137
          for {
wenzelm@67008
   138
            artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
wenzelm@67008
   139
            log_path <- JSON.string(artifact, "relativePath")
wenzelm@67008
   140
            (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
wenzelm@67008
   141
          } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
wenzelm@67008
   142
        Job_Info(job_name, timestamp, main_log, session_logs)
wenzelm@65659
   143
      }
wenzelm@65659
   144
wenzelm@65659
   145
    infos.sortBy(info => - info.timestamp)
wenzelm@63646
   146
  }
wenzelm@63646
   147
}