src/Pure/Admin/jenkins.scala
author wenzelm
Wed, 10 May 2017 17:24:31 +0200
changeset 65798 d459db0f6135
parent 65788 bc00ac4dba25
child 65896 18f5014331a1
permissions -rw-r--r--
actually plot extended profile history;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65650
48ef286b847b clarified modules;
wenzelm
parents: 64545
diff changeset
     1
/*  Title:      Pure/Admin/jenkins.scala
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     3
65650
48ef286b847b clarified modules;
wenzelm
parents: 64545
diff changeset
     4
Support for Jenkins continuous integration service.
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     5
*/
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     6
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     7
package isabelle
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     8
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
     9
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    10
import java.net.URL
65652
349999526df3 more informative log_filename;
wenzelm
parents: 65651
diff changeset
    11
import java.time.ZoneId
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    12
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    13
import scala.util.matching.Regex
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    14
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    15
65650
48ef286b847b clarified modules;
wenzelm
parents: 64545
diff changeset
    16
object Jenkins
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    17
{
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    18
  /* server API */
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    19
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    20
  def root(): String =
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    21
    Isabelle_System.getenv_strict("ISABELLE_JENKINS_ROOT")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    22
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    23
  def invoke(url: String, args: String*): Any =
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    24
  {
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    25
    val req = url + "/api/json?" + args.mkString("&")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    26
    val result = Url.read(req)
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    27
    try { JSON.parse(result) }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    28
    catch { case ERROR(_) => error("Malformed JSON from " + quote(req)) }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    29
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    30
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    31
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    32
  /* build jobs */
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    33
65658
be817b7b8354 tuned signature;
wenzelm
parents: 65657
diff changeset
    34
  def build_job_names(): List[String] =
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    35
    for {
64545
25045094d7bb clarified JSON operations (see isabelle_vscode/a7931dc2a1ab);
wenzelm
parents: 64160
diff changeset
    36
      job <- JSON.array(invoke(root()), "jobs").getOrElse(Nil)
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    37
      _class <- JSON.string(job, "_class")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    38
      if _class == "hudson.model.FreeStyleProject"
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    39
      name <- JSON.string(job, "name")
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    40
    } yield name
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    41
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    42
65660
dfecaf0fc069 proper log_path check;
wenzelm
parents: 65659
diff changeset
    43
  def download_logs(job_names: List[String], dir: Path, progress: Progress = No_Progress)
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    44
  {
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    45
    val store = Sessions.store()
65662
3db6a13fdffd more parallelism;
wenzelm
parents: 65661
diff changeset
    46
    val infos = job_names.flatMap(build_job_infos(_))
3db6a13fdffd more parallelism;
wenzelm
parents: 65661
diff changeset
    47
    Par_List.map((info: Job_Info) => info.download_log(store, dir, progress), infos)
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    48
  }
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    49
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    50
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65743
diff changeset
    51
  /* build log status */
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65674
diff changeset
    52
65788
bc00ac4dba25 more Jenkins test results;
wenzelm
parents: 65787
diff changeset
    53
  val build_log_jobs = List("isabelle-nightly-benchmark", "isabelle-nightly-slow")
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65674
diff changeset
    54
65747
5a3052b2095f tuned signature;
wenzelm
parents: 65743
diff changeset
    55
  val build_status_profiles: List[Build_Status.Profile] =
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65674
diff changeset
    56
    build_log_jobs.map(job_name =>
65798
d459db0f6135 actually plot extended profile history;
wenzelm
parents: 65788
diff changeset
    57
      Build_Status.Profile("jenkins " + job_name, 0,
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65674
diff changeset
    58
        Build_Log.Prop.build_engine + " = " + SQL.string(Build_Log.Jenkins.engine) + " AND " +
65767
222ed8901008 suppress "Pure" with its special threads=1 (Jenkins log does not provide threads in ISABELLE_BUILD_OPTIONS);
wenzelm
parents: 65764
diff changeset
    59
        Build_Log.Data.session_name + " <> " + SQL.string("Pure") + " AND " +
65736
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65674
diff changeset
    60
        Build_Log.Data.log_name + " LIKE " + SQL.string("%" + job_name)))
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65674
diff changeset
    61
2e7230b66a32 performance statistics from build log database;
wenzelm
parents: 65674
diff changeset
    62
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    63
  /* job info */
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    64
64054
1fc9ab31720d clarified modules;
wenzelm
parents: 64045
diff changeset
    65
  sealed case class Job_Info(
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    66
    job_name: String,
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
    67
    identify: Boolean,
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    68
    timestamp: Long,
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    69
    main_log: URL,
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    70
    session_logs: List[(String, String, URL)])
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
    71
  {
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    72
    val date: Date = Date(Time.ms(timestamp), ZoneId.of("Europe/Berlin"))
65656
wenzelm
parents: 65655
diff changeset
    73
wenzelm
parents: 65655
diff changeset
    74
    def log_filename: Path =
wenzelm
parents: 65655
diff changeset
    75
      Build_Log.log_filename(Build_Log.Jenkins.engine, date, List(job_name))
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    76
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    77
    def read_ml_statistics(store: Sessions.Store, session_name: String): List[Properties.T] =
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    78
    {
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    79
      def get_log(ext: String): Option[URL] =
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    80
        session_logs.collectFirst({ case (a, b, url) if a == session_name && b == ext => url })
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    81
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    82
      get_log("db") match {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    83
        case Some(url) =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    84
          Isabelle_System.with_tmp_file(session_name, "db") { database =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    85
            Bytes.write(database, Bytes.read(url))
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    86
            using(SQLite.open_database(database))(db =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    87
              store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    88
          }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    89
        case None =>
65655
1b84d4109215 clarified signature;
wenzelm
parents: 65654
diff changeset
    90
          get_log("gz") match {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    91
            case Some(url) =>
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    92
              val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url))
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    93
              log_file.parse_session_info(ml_statistics = true).ml_statistics
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    94
            case None => Nil
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    95
          }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    96
      }
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
    97
    }
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
    98
65660
dfecaf0fc069 proper log_path check;
wenzelm
parents: 65659
diff changeset
    99
    def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   100
    {
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   101
      val log_dir = dir + Build_Log.log_subdir(date)
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   102
      val log_path = log_dir + (if (identify) log_filename else log_filename.ext("xz"))
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   103
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   104
      if (!log_path.is_file) {
65660
dfecaf0fc069 proper log_path check;
wenzelm
parents: 65659
diff changeset
   105
        progress.echo(log_path.expand.implode)
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   106
        Isabelle_System.mkdirs(log_dir)
65660
dfecaf0fc069 proper log_path check;
wenzelm
parents: 65659
diff changeset
   107
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   108
        if (identify) {
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   109
          val log_file = Build_Log.Log_File(main_log.toString, Url.read(main_log))
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   110
          val isabelle_version = log_file.find_match(Build_Log.Jenkins.Isabelle_Version)
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   111
          val afp_version = log_file.find_match(Build_Log.Jenkins.AFP_Version)
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   112
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   113
          File.write(log_path,
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   114
            Build_Log.Identify.content(date, isabelle_version, afp_version) + "\n" +
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   115
              main_log.toString)
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   116
        }
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   117
        else {
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   118
          val ml_statistics =
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   119
            session_logs.map(_._1).toSet.toList.sorted.flatMap(session_name =>
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   120
              read_ml_statistics(store, session_name).
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   121
                map(props => (Build_Log.SESSION_NAME -> session_name) :: props))
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   122
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   123
          File.write_xz(log_path,
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   124
            terminate_lines(Url.read(main_log) ::
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   125
              ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))),
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   126
            XZ.options(6))
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   127
        }
65657
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   128
      }
2773b6859c55 download Jenkins logs with inlined ml_statistics;
wenzelm
parents: 65656
diff changeset
   129
    }
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   130
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   131
65654
0fbaa9286331 tuned signature;
wenzelm
parents: 65653
diff changeset
   132
  def build_job_infos(job_name: String): List[Job_Info] =
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   133
  {
65653
f433c0e73307 read ml_statistics from session logs: .db or .gz files;
wenzelm
parents: 65652
diff changeset
   134
    val Session_Log = new Regex("""^.*/log/([^/]+)\.(db|gz)$""")
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   135
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   136
    val identify = job_name == "identify"
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   137
    val job = if (identify) "isabelle-nightly-slow" else job_name
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   138
65659
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   139
    val infos =
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   140
      for {
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   141
        build <-
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   142
          JSON.array(
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   143
            invoke(root() + "/job/" + job, "tree=allBuilds[number,timestamp,artifacts[*]]"),
65659
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   144
            "allBuilds").getOrElse(Nil)
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   145
        number <- JSON.int(build, "number")
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   146
        timestamp <- JSON.long(build, "timestamp")
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   147
      } yield {
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   148
        val job_prefix = root() + "/job/" + job + "/" + number
65659
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   149
        val main_log = Url(job_prefix + "/consoleText")
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   150
        val session_logs =
65674
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   151
          if (identify) Nil
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   152
          else {
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   153
            for {
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   154
              artifact <- JSON.array(build, "artifacts").getOrElse(Nil)
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   155
              log_path <- JSON.string(artifact, "relativePath")
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   156
              (name, ext) <- (log_path match { case Session_Log(a, b) => Some((a, b)) case _ => None })
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   157
            } yield (name, ext, Url(job_prefix + "/artifact/" + log_path))
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   158
          }
23897f5d885d approximate repository identify job based on isabelle-nightly-slow;
wenzelm
parents: 65662
diff changeset
   159
        Job_Info(job_name, identify, timestamp, main_log, session_logs)
65659
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   160
      }
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   161
293141fb093d ensure canonical order: latest first;
wenzelm
parents: 65658
diff changeset
   162
    infos.sortBy(info => - info.timestamp)
63646
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   163
  }
74604a9fc4c8 API for Isabelle Jenkins continuous integration services;
wenzelm
parents:
diff changeset
   164
}