wenzelm@65650: /*  Title:      Pure/Admin/jenkins.scala
wenzelm@63646:     Author:     Makarius
wenzelm@63646: 
wenzelm@65650: Support for Jenkins continuous integration service.
wenzelm@63646: */
wenzelm@63646: 
wenzelm@63646: package isabelle
wenzelm@63646: 
wenzelm@63646: 
wenzelm@63646: import java.net.URL
wenzelm@63646: 
wenzelm@63646: import scala.util.matching.Regex
wenzelm@63646: 
wenzelm@63646: 
wenzelm@65650: object Jenkins
wenzelm@63646: {
wenzelm@65653:   /* server API */
wenzelm@63646: 
wenzelm@63646:   def root(): String =
wenzelm@63646:     Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
wenzelm@63646: 
wenzelm@63646:   def invoke(url: String, args: String*): Any =
wenzelm@63646:   {
wenzelm@63646:     val req = url + "/api/json?" + args.mkString("&")
wenzelm@63646:     val result = Url.read(req)
wenzelm@63646:     try { JSON.parse(result) }
wenzelm@63646:     catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
wenzelm@63646:   }
wenzelm@63646: 
wenzelm@63646: 
wenzelm@63646:   /* build jobs */
wenzelm@63646: 
wenzelm@65658:   def build_job_names(): List[String] =
wenzelm@63646:     for {
wenzelm@64545:       job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil)
wenzelm@63646:       _class <- JSON.string(job, "_class")
wenzelm@63646:       if _class == "hudson.model.FreeStyleProject"
wenzelm@63646:       name <- JSON.string(job, "name")
wenzelm@63646:     } yield name
wenzelm@63646: 
wenzelm@65657: 
wenzelm@68209:   def download_logs(
wenzelm@68209:     options: Options, job_names: List[String], dir: Path, progress: Progress = No_Progress)
wenzelm@65657:   {
wenzelm@68209:     val store = Sessions.store(options)
wenzelm@65662:     val infos = job_names.flatMap(build_job_infos(_))
wenzelm@65662:     Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos)
wenzelm@65657:   }
wenzelm@65657: 
wenzelm@65657: 
wenzelm@65747:   /* build log status */
wenzelm@65736: 
wenzelm@65788:   val build_log_jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
wenzelm@65736: 
wenzelm@65747:   val build_status_profiles: List[Build_Status.Profile] =
wenzelm@65736:     build_log_jobs.map(job_name =>
wenzelm@66880:       Build_Status.Profile("jenkins " + job_name,
wenzelm@66880:         sql =
wenzelm@66880:           Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
wenzelm@66880:           Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
wenzelm@66880:           Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
wenzelm@66880:           " AND " + Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
wenzelm@65736: 
wenzelm@65736: 
wenzelm@65657:   /* job info */
wenzelm@65657: 
wenzelm@64054:   sealed case class Job_Info(
wenzelm@63646:     job_name: String,
wenzelm@63646:     timestamp: Long,
wenzelm@65655:     main_log: URL,
wenzelm@65653:     session_logs: List[(String, String, URL)])
wenzelm@63646:   {
wenzelm@69980:     val date: Date = Date(Time.ms(timestamp), Date.timezone_berlin)
wenzelm@65656: 
wenzelm@65656:     def log_filename: Path =
wenzelm@65656:       Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
wenzelm@65653: 
wenzelm@65653:     def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] =
wenzelm@65653:     {
wenzelm@65655:       def get_log(ext: String): Option[URL] =
wenzelm@65655:         session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url })
wenzelm@65655: 
wenzelm@65655:       get_log("db") match {
wenzelm@65653:         case Some(url) =>
wenzelm@65653:           Isabelle_System.with_tmp_file(session_name, "db") { database =>
wenzelm@65653:             Bytes.write(database, Bytes.read(url))
wenzelm@65935:             using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name))
wenzelm@65653:           }
wenzelm@65653:         case None =>
wenzelm@65655:           get_log("gz") match {
wenzelm@65653:             case Some(url) =>
wenzelm@65653:               val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url))
wenzelm@65653:               log_file.parse_session_info(ml_statistics = true).ml_statistics
wenzelm@65653:             case None => Nil
wenzelm@65653:           }
wenzelm@65653:       }
wenzelm@65653:     }
wenzelm@65657: 
wenzelm@65660:     def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
wenzelm@65657:     {
wenzelm@65657:       val log_dir = dir + Build_Log.log_subdir(date)
wenzelm@67008:       val log_path = log_dir + log_filename.ext("xz")
wenzelm@65657: 
wenzelm@65657:       if (!log_path.is_file) {
wenzelm@65660:         progress.echo(log_path.expand.implode)
wenzelm@65674:         Isabelle_System.mkdirs(log_dir)
wenzelm@65660: 
wenzelm@67008:         val ml_statistics =
wenzelm@67008:           session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
wenzelm@67008:             read_ml_statistics(store, session_name).
wenzelm@67008:               map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
wenzelm@65657: 
wenzelm@67008:         File.write_xz(log_path,
wenzelm@67008:           terminate_lines(Url.read(main_log) ::
wenzelm@67008:             ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
wenzelm@67008:           XZ.options(6))
wenzelm@65657:       }
wenzelm@65657:     }
wenzelm@63646:   }
wenzelm@63646: 
wenzelm@65654:   def build_job_infos(job_name: String): List[Job_Info] =
wenzelm@63646:   {
wenzelm@65653:     val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
wenzelm@63646: 
wenzelm@65659:     val infos =
wenzelm@65659:       for {
wenzelm@65659:         build <-
wenzelm@65659:           JSON.array(
wenzelm@67008:             invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
wenzelm@65659:             "allBuilds").getOrElse(Nil)
wenzelm@65659:         number <- JSON.int(build, "number")
wenzelm@65659:         timestamp <- JSON.long(build, "timestamp")
wenzelm@65659:       } yield {
wenzelm@67008:         val job_prefix = root() + "/job/" + job_name + "/" + number
wenzelm@65659:         val main_log = Url(job_prefix + "/consoleText")
wenzelm@65659:         val session_logs =
wenzelm@67008:           for {
wenzelm@67008:             artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
wenzelm@67008:             log_path <- JSON.string(artifact, "relativePath")
wenzelm@67008:             (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
wenzelm@67008:           } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
wenzelm@67008:         Job_Info(job_name, timestamp, main_log, session_logs)
wenzelm@65659:       }
wenzelm@65659: 
wenzelm@65659:     infos.sortBy(info => - info.timestamp)
wenzelm@63646:   }
wenzelm@63646: }