src/Pure/Admin/jenkins.scala
changeset 67008 eed58245b579
parent 66880 486f4af28db9
child 68209 aeffd8f1f079
     1.1 --- a/src/Pure/Admin/jenkins.scala	Sat Nov 04 19:44:28 2017 +0100
     1.2 +++ b/src/Pure/Admin/jenkins.scala	Sat Nov 04 21:06:02 2017 +0100
     1.3 @@ -66,7 +66,6 @@
     1.4  
     1.5    sealed case class Job_Info(
     1.6      job_name: String,
     1.7 -    identify: Boolean,
     1.8      timestamp: Long,
     1.9      main_log: URL,
    1.10      session_logs: List[(String, String, URL)])
    1.11 @@ -100,32 +99,21 @@
    1.12      def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
    1.13      {
    1.14        val log_dir = dir + Build_Log.log_subdir(date)
    1.15 -      val log_path = log_dir + (if (identify) log_filename else log_filename.ext("xz"))
    1.16 +      val log_path = log_dir + log_filename.ext("xz")
    1.17  
    1.18        if (!log_path.is_file) {
    1.19          progress.echo(log_path.expand.implode)
    1.20          Isabelle_System.mkdirs(log_dir)
    1.21  
    1.22 -        if (identify) {
    1.23 -          val log_file = Build_Log.Log_File(main_log.toString, Url.read(main_log))
    1.24 -          val isabelle_version = log_file.find_match(Build_Log.Jenkins.Isabelle_Version)
    1.25 -          val afp_version = log_file.find_match(Build_Log.Jenkins.AFP_Version)
    1.26 +        val ml_statistics =
    1.27 +          session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
    1.28 +            read_ml_statistics(store, session_name).
    1.29 +              map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
    1.30  
    1.31 -          File.write(log_path,
    1.32 -            Build_Log.Identify.content(date, isabelle_version, afp_version) + "\n" +
    1.33 -              main_log.toString)
    1.34 -        }
    1.35 -        else {
    1.36 -          val ml_statistics =
    1.37 -            session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
    1.38 -              read_ml_statistics(store, session_name).
    1.39 -                map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
    1.40 -
    1.41 -          File.write_xz(log_path,
    1.42 -            terminate_lines(Url.read(main_log) ::
    1.43 -              ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
    1.44 -            XZ.options(6))
    1.45 -        }
    1.46 +        File.write_xz(log_path,
    1.47 +          terminate_lines(Url.read(main_log) ::
    1.48 +            ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
    1.49 +          XZ.options(6))
    1.50        }
    1.51      }
    1.52    }
    1.53 @@ -134,30 +122,24 @@
    1.54    {
    1.55      val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
    1.56  
    1.57 -    val identify = job_name == "identify"
    1.58 -    val job = if (identify) "isabelle-nightly-slow" else job_name
    1.59 -
    1.60      val infos =
    1.61        for {
    1.62          build <-
    1.63            JSON.array(
    1.64 -            invoke(root() + "/job/" + job, "tree=allBuilds[number,timestamp,artifacts[*]]"),
    1.65 +            invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
    1.66              "allBuilds").getOrElse(Nil)
    1.67          number <- JSON.int(build, "number")
    1.68          timestamp <- JSON.long(build, "timestamp")
    1.69        } yield {
    1.70 -        val job_prefix = root() + "/job/" + job + "/" + number
    1.71 +        val job_prefix = root() + "/job/" + job_name + "/" + number
    1.72          val main_log = Url(job_prefix + "/consoleText")
    1.73          val session_logs =
    1.74 -          if (identify) Nil
    1.75 -          else {
    1.76 -            for {
    1.77 -              artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
    1.78 -              log_path <- JSON.string(artifact, "relativePath")
    1.79 -              (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
    1.80 -            } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
    1.81 -          }
    1.82 -        Job_Info(job_name, identify, timestamp, main_log, session_logs)
    1.83 +          for {
    1.84 +            artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
    1.85 +            log_path <- JSON.string(artifact, "relativePath")
    1.86 +            (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
    1.87 +          } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
    1.88 +        Job_Info(job_name, timestamp, main_log, session_logs)
    1.89        }
    1.90  
    1.91      infos.sortBy(info => - info.timestamp)