src/Pure/Admin/jenkins.scala
changeset 67008 eed58245b579
parent 66880 486f4af28db9
child 68209 aeffd8f1f079
equal deleted inserted replaced
67007:978c584609de 67008:eed58245b579
    64 
    64 
    65   /* job info */
    65   /* job info */
    66 
    66 
    67   sealed case class Job_Info(
    67   sealed case class Job_Info(
    68     job_name: String,
    68     job_name: String,
    69     identify: Boolean,
       
    70     timestamp: Long,
    69     timestamp: Long,
    71     main_log: URL,
    70     main_log: URL,
    72     session_logs: List[(String, String, URL)])
    71     session_logs: List[(String, String, URL)])
    73   {
    72   {
    74     val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
    73     val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
    98     }
    97     }
    99 
    98 
   100     def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
    99     def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
   101     {
   100     {
   102       val log_dir = dir + Build_Log.log_subdir(date)
   101       val log_dir = dir + Build_Log.log_subdir(date)
   103       val log_path = log_dir + (if (identify) log_filename else log_filename.ext("xz"))
   102       val log_path = log_dir + log_filename.ext("xz")
   104 
   103 
   105       if (!log_path.is_file) {
   104       if (!log_path.is_file) {
   106         progress.echo(log_path.expand.implode)
   105         progress.echo(log_path.expand.implode)
   107         Isabelle_System.mkdirs(log_dir)
   106         Isabelle_System.mkdirs(log_dir)
   108 
   107 
   109         if (identify) {
   108         val ml_statistics =
   110           val log_file = Build_Log.Log_File(main_log.toString, Url.read(main_log))
   109           session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
   111           val isabelle_version = log_file.find_match(Build_Log.Jenkins.Isabelle_Version)
   110             read_ml_statistics(store, session_name).
   112           val afp_version = log_file.find_match(Build_Log.Jenkins.AFP_Version)
   111               map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
   113 
   112 
   114           File.write(log_path,
   113         File.write_xz(log_path,
   115             Build_Log.Identify.content(date, isabelle_version, afp_version) + "\n" +
   114           terminate_lines(Url.read(main_log) ::
   116               main_log.toString)
   115             ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
   117         }
   116           XZ.options(6))
   118         else {
       
   119           val ml_statistics =
       
   120             session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
       
   121               read_ml_statistics(store, session_name).
       
   122                 map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
       
   123 
       
   124           File.write_xz(log_path,
       
   125             terminate_lines(Url.read(main_log) ::
       
   126               ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
       
   127             XZ.options(6))
       
   128         }
       
   129       }
   117       }
   130     }
   118     }
   131   }
   119   }
   132 
   120 
   133   def build_job_infos(job_name: String): List[Job_Info] =
   121   def build_job_infos(job_name: String): List[Job_Info] =
   134   {
   122   {
   135     val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
   123     val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
   136 
   124 
   137     val identify = job_name == "identify"
       
   138     val job = if (identify) "isabelle-nightly-slow" else job_name
       
   139 
       
   140     val infos =
   125     val infos =
   141       for {
   126       for {
   142         build <-
   127         build <-
   143           JSON.array(
   128           JSON.array(
   144             invoke(root() + "/job/" + job, "tree=allBuilds[number,timestamp,artifacts[*]]"),
   129             invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"),
   145             "allBuilds").getOrElse(Nil)
   130             "allBuilds").getOrElse(Nil)
   146         number <- JSON.int(build, "number")
   131         number <- JSON.int(build, "number")
   147         timestamp <- JSON.long(build, "timestamp")
   132         timestamp <- JSON.long(build, "timestamp")
   148       } yield {
   133       } yield {
   149         val job_prefix = root() + "/job/" + job + "/" + number
   134         val job_prefix = root() + "/job/" + job_name + "/" + number
   150         val main_log = Url(job_prefix + "/consoleText")
   135         val main_log = Url(job_prefix + "/consoleText")
   151         val session_logs =
   136         val session_logs =
   152           if (identify) Nil
   137           for {
   153           else {
   138             artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
   154             for {
   139             log_path <- JSON.string(artifact, "relativePath")
   155               artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
   140             (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
   156               log_path <- JSON.string(artifact, "relativePath")
   141           } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
   157               (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
   142         Job_Info(job_name, timestamp, main_log, session_logs)
   158             } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
       
   159           }
       
   160         Job_Info(job_name, identify, timestamp, main_log, session_logs)
       
   161       }
   143       }
   162 
   144 
   163     infos.sortBy(info => - info.timestamp)
   145     infos.sortBy(info => - info.timestamp)
   164   }
   146   }
   165 }
   147 }