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