superseded by plain_identify;
authorwenzelm
Sat Nov 04 21:06:02 2017 +0100 (18 months ago)
changeset 67008eed58245b579
parent 67007 978c584609de
child 67009 b68592732783
superseded by plain_identify;
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/jenkins.scala
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 19:44:28 2017 +0100
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Sat Nov 04 21:06:02 2017 +0100
     1.3 @@ -24,8 +24,6 @@
     1.4    val isabelle_repos_test = main_dir + Path.explode("isabelle-test")
     1.5    val afp_repos = main_dir + Path.explode("AFP")
     1.6  
     1.7 -  val jenkins_jobs = "identify" :: Jenkins.build_log_jobs
     1.8 -
     1.9    val build_log_dirs =
    1.10      List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
    1.11  
    1.12 @@ -467,7 +465,8 @@
    1.13                        (r, i) <- (if (seq.length <= 1) seq.map((_, -1)) else seq.zipWithIndex)
    1.14                        (isabelle_rev, afp_rev) <- r.pick(logger.options, rev, history_base_filter(r))
    1.15                      } yield remote_build_history(isabelle_rev, afp_rev, i, r)))),
    1.16 -                Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
    1.17 +                Logger_Task("jenkins_logs", _ =>
    1.18 +                  Jenkins.download_logs(Jenkins.build_log_jobs, main_dir)),
    1.19                  Logger_Task("build_log_database",
    1.20                    logger => Isabelle_Devel.build_log_database(logger.options, build_log_dirs)),
    1.21                  Logger_Task("build_status",
     2.1 --- a/src/Pure/Admin/jenkins.scala	Sat Nov 04 19:44:28 2017 +0100
     2.2 +++ b/src/Pure/Admin/jenkins.scala	Sat Nov 04 21:06:02 2017 +0100
     2.3 @@ -66,7 +66,6 @@
     2.4  
     2.5    sealed case class Job_Info(
     2.6      job_name: String,
     2.7 -    identify: Boolean,
     2.8      timestamp: Long,
     2.9      main_log: URL,
    2.10      session_logs: List[(String, String, URL)])
    2.11 @@ -100,32 +99,21 @@
    2.12      def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
    2.13      {
    2.14        val log_dir = dir + Build_Log.log_subdir(date)
    2.15 -      val log_path = log_dir + (if (identify) log_filename else log_filename.ext("xz"))
    2.16 +      val log_path = log_dir + log_filename.ext("xz")
    2.17  
    2.18        if (!log_path.is_file) {
    2.19          progress.echo(log_path.expand.implode)
    2.20          Isabelle_System.mkdirs(log_dir)
    2.21  
    2.22 -        if (identify) {
    2.23 -          val log_file = Build_Log.Log_File(main_log.toString, Url.read(main_log))
    2.24 -          val isabelle_version = log_file.find_match(Build_Log.Jenkins.Isabelle_Version)
    2.25 -          val afp_version = log_file.find_match(Build_Log.Jenkins.AFP_Version)
    2.26 +        val ml_statistics =
    2.27 +          session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
    2.28 +            read_ml_statistics(store, session_name).
    2.29 +              map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
    2.30  
    2.31 -          File.write(log_path,
    2.32 -            Build_Log.Identify.content(date, isabelle_version, afp_version) + "\n" +
    2.33 -              main_log.toString)
    2.34 -        }
    2.35 -        else {
    2.36 -          val ml_statistics =
    2.37 -            session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
    2.38 -              read_ml_statistics(store, session_name).
    2.39 -                map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
    2.40 -
    2.41 -          File.write_xz(log_path,
    2.42 -            terminate_lines(Url.read(main_log) ::
    2.43 -              ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
    2.44 -            XZ.options(6))
    2.45 -        }
    2.46 +        File.write_xz(log_path,
    2.47 +          terminate_lines(Url.read(main_log) ::
    2.48 +            ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
    2.49 +          XZ.options(6))
    2.50        }
    2.51      }
    2.52    }
    2.53 @@ -134,30 +122,24 @@
    2.54    {
    2.55      val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
    2.56  
    2.57 -    val identify = job_name == "identify"
    2.58 -    val job = if (identify) "isabelle-nightly-slow" else job_name
    2.59 -
    2.60      val infos =
    2.61        for {
    2.62          build <-
    2.63            JSON.array(
    2.64 -            invoke(root() + "/job/" + job, "tree=allBuilds[number,timestamp,artifacts[*]]"),
    2.65 +            invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
    2.66              "allBuilds").getOrElse(Nil)
    2.67          number <- JSON.int(build, "number")
    2.68          timestamp <- JSON.long(build, "timestamp")
    2.69        } yield {
    2.70 -        val job_prefix = root() + "/job/" + job + "/" + number
    2.71 +        val job_prefix = root() + "/job/" + job_name + "/" + number
    2.72          val main_log = Url(job_prefix + "/consoleText")
    2.73          val session_logs =
    2.74 -          if (identify) Nil
    2.75 -          else {
    2.76 -            for {
    2.77 -              artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
    2.78 -              log_path <- JSON.string(artifact, "relativePath")
    2.79 -              (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
    2.80 -            } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
    2.81 -          }
    2.82 -        Job_Info(job_name, identify, timestamp, main_log, session_logs)
    2.83 +          for {
    2.84 +            artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
    2.85 +            log_path <- JSON.string(artifact, "relativePath")
    2.86 +            (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
    2.87 +          } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
    2.88 +        Job_Info(job_name, timestamp, main_log, session_logs)
    2.89        }
    2.90  
    2.91      infos.sortBy(info => - info.timestamp)