# HG changeset patch # User wenzelm # Date 1493671539 -7200 # Node ID 23897f5d885df99ab6e5d3b7202a81055ee67d13 # Parent 9cd66d9c38633128925a9d03f8152c857d679aef approximate repository identify job based on isabelle-nightly-slow; more Jenkins changeset patterns found in the wild; diff -r 9cd66d9c3863 -r 23897f5d885d src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Mon May 01 20:29:44 2017 +0200 +++ b/src/Pure/Admin/build_log.scala Mon May 01 22:45:39 2017 +0200 @@ -311,7 +311,17 @@ object Identify { val log_prefix = "isabelle_identify_" - val engine = "identify" + + def engine(log_file: Log_File): String = + if (log_file.name.startsWith(Jenkins.log_prefix)) "jenkins_identify" + else "identify" + + def content(date: Date, isabelle_version: Option[String], afp_version: Option[String]): String = + terminate_lines( + List("isabelle_identify: " + Build_Log.print_date(date), "") ::: + isabelle_version.map("Isabelle version: " + _).toList ::: + afp_version.map("AFP version: " + _).toList) + val Start = new Regex("""^isabelle_identify: (.+)$""") val No_End = new Regex("""$.""") val Isabelle_Version = new Regex("""^Isabelle version: (\S+)$""") @@ -348,8 +358,10 @@ val Start = new Regex("""^(?:Started by an SCM change|Started from command line by admin|).*$""") val Start_Date = new Regex("""^Build started at (.+)$""") val No_End = new Regex("""$.""") - val Isabelle_Version = new Regex("""^Isabelle id (\S+)$""") - val AFP_Version = new Regex("""^AFP id (\S+)$""") + val Isabelle_Version = + new Regex("""^(?:Build for Isabelle id |Isabelle id |ISABELLE_CI_REPO_ID=")(\w+).*$""") + val AFP_Version = + new Regex("""^(?:Build for AFP id |AFP id |ISABELLE_CI_AFP_ID=")(\w+).*$""") val CONFIGURATION = "=== CONFIGURATION ===" val BUILD = "=== BUILD ===" } @@ -391,7 +403,7 @@ log_file.get_all_settings) case Identify.Start(log_file.Strict_Date(start)) :: _ => - parse(Identify.engine, "", start, Identify.No_End, + parse(Identify.engine(log_file), "", start, Identify.No_End, Identify.Isabelle_Version, Identify.AFP_Version) case Isatest.Start(log_file.Strict_Date(start), host) :: _ => diff -r 9cd66d9c3863 -r 23897f5d885d src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Mon May 01 20:29:44 2017 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Mon May 01 22:45:39 2017 +0200 @@ -48,11 +48,7 @@ val afp_rev = Mercurial.setup_repository(afp_source, afp_repos).id() File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date), - terminate_lines( - List("isabelle_identify: " + Build_Log.print_date(logger.start_date), - "", - "Isabelle version: " + rev, - "AFP version: " + afp_rev))) + Build_Log.Identify.content(logger.start_date, Some(rev), Some(afp_rev))) val new_snapshot = release_snapshot.ext("new") val old_snapshot = release_snapshot.ext("old") diff -r 9cd66d9c3863 -r 23897f5d885d src/Pure/Admin/jenkins.scala --- a/src/Pure/Admin/jenkins.scala Mon May 01 20:29:44 2017 +0200 +++ b/src/Pure/Admin/jenkins.scala Mon May 01 22:45:39 2017 +0200 @@ -52,6 +52,7 @@ sealed case class Job_Info( job_name: String, + identify: Boolean, timestamp: Long, main_log: URL, session_logs: List[(String, String, URL)]) @@ -86,21 +87,32 @@ def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress) { val log_dir = dir + Build_Log.log_subdir(date) - val log_path = log_dir + log_filename.ext("xz") + val log_path = log_dir + (if (identify) log_filename else log_filename.ext("xz")) if (!log_path.is_file) { progress.echo(log_path.expand.implode) + Isabelle_System.mkdirs(log_dir) - val ml_statistics = - session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name => - read_ml_statistics(store, session_name). - map(props => (Build_Log.SESSION_NAME -> session_name) :: props)) + if (identify) { + val log_file = Build_Log.Log_File(main_log.toString, Url.read(main_log)) + val isabelle_version = log_file.find_match(Build_Log.Jenkins.Isabelle_Version) + val afp_version = log_file.find_match(Build_Log.Jenkins.AFP_Version) - Isabelle_System.mkdirs(log_dir) - File.write_xz(log_path, - terminate_lines(Url.read(main_log) :: - ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))), - XZ.options(6)) + File.write(log_path, + Build_Log.Identify.content(date, isabelle_version, afp_version) + "\n" + + main_log.toString) + } + else { + val ml_statistics = + session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name => + read_ml_statistics(store, session_name). + map(props => (Build_Log.SESSION_NAME -> session_name) :: props)) + + File.write_xz(log_path, + terminate_lines(Url.read(main_log) :: + ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))), + XZ.options(6)) + } } } } @@ -109,24 +121,30 @@ { val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""") + val identify = job_name == "identify" + val job = if (identify) "isabelle-nightly-slow" else job_name + val infos = for { build <- JSON.array( - invoke(root() + "/job/" + job_name, "tree=allBuilds[number,timestamp,artifacts[*]]"), + invoke(root() + "/job/" + job, "tree=allBuilds[number,timestamp,artifacts[*]]"), "allBuilds").getOrElse(Nil) number <- JSON.int(build, "number") timestamp <- JSON.long(build, "timestamp") } yield { - val job_prefix = root() + "/job/" + job_name + "/" + number + val job_prefix = root() + "/job/" + job + "/" + number val main_log = Url(job_prefix + "/consoleText") val session_logs = - for { - artifact <- JSON.array(build, "artifacts").getOrElse(Nil) - log_path <- JSON.string(artifact, "relativePath") - (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None }) - } yield (name, ext, Url(job_prefix + "/artifact/" + log_path)) - Job_Info(job_name, timestamp, main_log, session_logs) + if (identify) Nil + else { + for { + artifact <- JSON.array(build, "artifacts").getOrElse(Nil) + log_path <- JSON.string(artifact, "relativePath") + (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None }) + } yield (name, ext, Url(job_prefix + "/artifact/" + log_path)) + } + Job_Info(job_name, identify, timestamp, main_log, session_logs) } infos.sortBy(info => - info.timestamp)