author | Fabian Huch <huch@in.tum.de> |
Wed, 12 Jun 2024 17:06:34 +0200 | |
changeset 80411 | a9fce67fb8b2 |
parent 80281 | 17d2f775907a |
permissions | -rw-r--r-- |
77570 | 1 |
/* Title: Pure/Admin/ci_build.scala |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
2 |
Author: Fabian Huch, TU Munich |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
3 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
4 |
Module for automated (continuous integration) builds. |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
5 |
*/ |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
6 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
7 |
package isabelle |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
8 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
9 |
|
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
10 |
import scala.collection.mutable |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
11 |
|
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
12 |
|
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
13 |
object CI_Build { |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
14 |
def section(title: String): String = "\n=== " + title + " ===\n" |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
15 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
16 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
17 |
/* mailing */ |
75628
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75393
diff
changeset
|
18 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
19 |
object Mail_System { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
20 |
def try_open(options: Options): Option[Mail_System] = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
21 |
Exn.capture(new Mail_System(options)) match { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
22 |
case Exn.Res(res) if res.server.defined => Some(res) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
23 |
case _ => None |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
24 |
} |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
25 |
} |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
26 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
27 |
class Mail_System private(options: Options) { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
28 |
val from: Mail.Address = Mail.address(options.string("ci_mail_from")) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
29 |
val to: Mail.Address = Mail.address(options.string("ci_mail_to")) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
30 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
31 |
val server: Mail.Server = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
32 |
new Mail.Server(Mail.address(options.string("ci_mail_sender")), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
33 |
smtp_host = options.string("ci_mail_smtp_host"), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
34 |
smtp_port = options.int("ci_mail_smtp_port"), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
35 |
user = options.string("ci_mail_user"), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
36 |
password = options.string("ci_mail_password")) |
73934
39e0c7fac69e
jenkins: pre/post-hook results
Fabian Huch <huch@in.tum.de>
parents:
73359
diff
changeset
|
37 |
} |
39e0c7fac69e
jenkins: pre/post-hook results
Fabian Huch <huch@in.tum.de>
parents:
73359
diff
changeset
|
38 |
|
75628
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75393
diff
changeset
|
39 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
40 |
/** ci build jobs **/ |
75628
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75393
diff
changeset
|
41 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
42 |
/* hosts */ |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
43 |
|
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
44 |
sealed trait Hosts { |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
45 |
def hosts_spec: String |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
46 |
def max_jobs: Option[Int] |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
47 |
def prefs: List[Options.Spec] |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
48 |
def numa_shuffling: Boolean |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
49 |
def build_cluster: Boolean |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
50 |
} |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
51 |
|
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
52 |
case class Local(host_spec: String, jobs: Int, threads: Int, numa_shuffling: Boolean = true) |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
53 |
extends Hosts { |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
54 |
def hosts_spec: String = host_spec |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
55 |
def max_jobs: Option[Int] = Some(jobs) |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
56 |
def prefs: List[Options.Spec] = List(Options.Spec.eq("threads", threads.toString)) |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
57 |
def build_cluster: Boolean = false |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
58 |
} |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
59 |
|
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
60 |
case class Cluster(hosts_spec: String, numa_shuffling: Boolean = true) extends Hosts { |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
61 |
def max_jobs: Option[Int] = None |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
62 |
def prefs: List[Options.Spec] = Nil |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
63 |
def build_cluster: Boolean = true |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
64 |
} |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
65 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
66 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
67 |
/* build triggers */ |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
68 |
|
80261
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
69 |
sealed trait Trigger |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
70 |
case object On_Commit extends Trigger |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
71 |
|
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
72 |
object Timed { |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
73 |
def nightly(start_time: Time = Time.zero): Timed = |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
74 |
Timed { (before, now) => |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
75 |
val start0 = before.midnight + start_time |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
76 |
val start1 = now.midnight + start_time |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
77 |
(before.time < start0.time && start0.time <= now.time) || |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
78 |
(before.time < start1.time && start1.time <= now.time) |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
79 |
} |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
80 |
} |
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
81 |
|
80261
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
82 |
case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger |
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
83 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
84 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
85 |
/* build hooks */ |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
86 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
87 |
trait Hook { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
88 |
def pre(options: Options, progress: Progress): Unit = () |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
89 |
def post( |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
90 |
options: Options, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
91 |
start_date: Date, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
92 |
url: Option[Url], |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
93 |
results: Build.Results, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
94 |
progress: Progress |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
95 |
): Unit = () |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
96 |
} |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
97 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
98 |
object none extends Hook |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
99 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
100 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
101 |
/* jobs */ |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
102 |
|
80260
ed9b1598d293
manage components of ci builds;
Fabian Huch <huch@in.tum.de>
parents:
80245
diff
changeset
|
103 |
sealed case class Job( |
ed9b1598d293
manage components of ci builds;
Fabian Huch <huch@in.tum.de>
parents:
80245
diff
changeset
|
104 |
name: String, |
ed9b1598d293
manage components of ci builds;
Fabian Huch <huch@in.tum.de>
parents:
80245
diff
changeset
|
105 |
description: String, |
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
106 |
hosts: Hosts, |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
107 |
afp: Boolean = false, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
108 |
selection: Sessions.Selection = Sessions.Selection.empty, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
109 |
presentation: Boolean = false, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
110 |
clean_build: Boolean = false, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
111 |
select_dirs: List[Path] = Nil, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
112 |
build_prefs: List[Options.Spec] = Nil, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
113 |
hook: Hook = none, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
114 |
extra_components: List[String] = Nil, |
80261
e3f472221f8f
add triggers to ci jobs: on commit vs timed;
Fabian Huch <huch@in.tum.de>
parents:
80260
diff
changeset
|
115 |
trigger: Trigger = On_Commit |
80260
ed9b1598d293
manage components of ci builds;
Fabian Huch <huch@in.tum.de>
parents:
80245
diff
changeset
|
116 |
) { |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
117 |
override def toString: String = name |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
118 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
119 |
def afp_root: Option[Path] = if (!afp) None else Some(AFP.BASE) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
120 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
121 |
def prefs: List[Options.Spec] = build_prefs ++ hosts.prefs ++ document_prefs |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
122 |
def document_prefs: List[Options.Spec] = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
123 |
if (!presentation) Nil |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
124 |
else List( |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
125 |
Options.Spec.eq("browser_info", "true"), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
126 |
Options.Spec.eq("document", "pdf"), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
127 |
Options.Spec.eq("document_variants", "document:outline=/proof,/ML")) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
128 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
129 |
def components: List[String] = (if (!afp) Nil else List("AFP")) ::: extra_components |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
130 |
} |
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
131 |
|
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
132 |
private lazy val known_jobs: List[Job] = |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
133 |
Isabelle_System.make_services(classOf[Isabelle_CI_Jobs]).flatMap(_.jobs) |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
134 |
|
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
135 |
def show_jobs: String = |
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
136 |
cat_lines(known_jobs.sortBy(_.name).map(job => job.name + " - " + job.description)) |
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
137 |
|
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
138 |
def the_job(name: String): Job = known_jobs.find(job => job.name == name) getOrElse |
76225 | 139 |
error("Unknown job " + quote(name)) |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
140 |
|
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
141 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
142 |
/* concrete jobs */ |
75628
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75393
diff
changeset
|
143 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
144 |
val timing = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
145 |
Job("benchmark", |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
146 |
description = "runs benchmark and timing sessions", |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
147 |
Local("benchmark", jobs = 1, threads = 6, numa_shuffling = false), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
148 |
selection = Sessions.Selection(session_groups = List("timing")), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
149 |
clean_build = true, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
150 |
select_dirs = List(Path.explode("~~/src/Benchmarks")), |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
151 |
trigger = Timed.nightly()) |
75628
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75393
diff
changeset
|
152 |
|
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75393
diff
changeset
|
153 |
|
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
154 |
/* ci build */ |
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
155 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
156 |
def ci_build( |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
157 |
options: Options, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
158 |
job: Job, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
159 |
build_hosts: List[Build_Cluster.Host] = Nil, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
160 |
url: Option[Url] = None, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
161 |
progress: Progress = new Progress |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
162 |
): Unit = { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
163 |
val start_date = Date.now() |
63385 | 164 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
165 |
def return_code(f: => Unit): Int = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
166 |
Exn.capture(f) match { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
167 |
case Exn.Res(_) => Process_Result.RC.ok |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
168 |
case Exn.Exn(e) => |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
169 |
progress.echo_error_message(e.getMessage) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
170 |
Process_Result.RC.error |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
171 |
} |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
172 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
173 |
val mail_result = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
174 |
return_code { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
175 |
Mail_System.try_open(options).getOrElse(error("No mail configuration")).server.check() |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
176 |
} |
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
177 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
178 |
val pre_result = return_code { job.hook.pre(options, progress) } |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
179 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
180 |
progress.echo(section("BUILD")) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
181 |
val results = progress.interrupt_handler { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
182 |
Build.build( |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
183 |
options ++ job.prefs, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
184 |
build_hosts = build_hosts, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
185 |
selection = job.selection, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
186 |
progress = progress, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
187 |
clean_build = job.clean_build, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
188 |
afp_root = job.afp_root, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
189 |
select_dirs = job.select_dirs, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
190 |
numa_shuffling = job.hosts.numa_shuffling, |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
191 |
max_jobs = job.hosts.max_jobs) |
75628
6a5e4f17f285
switched to statically compiled ci profile;
Fabian Huch <huch@in.tum.de>
parents:
75393
diff
changeset
|
192 |
} |
63349 | 193 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
194 |
val post_result = return_code { job.hook.post(options, start_date, url, results, progress) } |
63385 | 195 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
196 |
val rc = List(mail_result, pre_result, results.rc, post_result).max |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
197 |
if (rc != Process_Result.RC.ok) { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
198 |
progress.echo(section("FAILED")) |
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
199 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
200 |
if (mail_result != Process_Result.RC.ok) progress.echo("Mail: FAILED") |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
201 |
else { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
202 |
val mail_system = Mail_System.try_open(options).get |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
203 |
val content = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
204 |
"The job " + job.name + " failed. " + if_proper(url, " View the build at: " + url.get) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
205 |
val mail = Mail("Build failed", List(mail_system.to), content, Some(mail_system.from)) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
206 |
mail_system.server.send(mail) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
207 |
} |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
208 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
209 |
if (pre_result != Process_Result.RC.ok) progress.echo("Pre-hook: FAILED") |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
210 |
for (name <- results.sessions) { |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
211 |
if (results.cancelled(name)) progress.echo("Session " + name + ": CANCELLED") |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
212 |
else { |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
213 |
val result = results(name) |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
214 |
if (!result.ok) progress.echo("Session " + name + ": FAILED " + result.rc) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
215 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
216 |
} |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
217 |
if (post_result != Process_Result.RC.ok) progress.echo("Post-hook: FAILED") |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
218 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
219 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
220 |
sys.exit(rc) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
221 |
} |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
222 |
|
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
223 |
|
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
224 |
/* Isabelle tool wrapper */ |
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
225 |
|
78821
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
226 |
val isabelle_tool = Isabelle_Tool("ci_build", "builds Isabelle jobs in ci environments", |
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
227 |
Scala_Project.here, |
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
228 |
{ args => |
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
229 |
var options = Options.init() |
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
230 |
val build_hosts = new mutable.ListBuffer[Build_Cluster.Host] |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
231 |
var url: Option[Url] = None |
78821
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
232 |
|
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
233 |
val getopts = Getopts(""" |
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
234 |
Usage: isabelle ci_build [OPTIONS] JOB |
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
235 |
|
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
236 |
Options are: |
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
237 |
-H HOSTS host specifications of the form NAMES:PARAMETERS (separated by commas) |
78821
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
238 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
239 |
-u URL build url |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
240 |
|
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
241 |
Runs Isabelle builds in ci environment. For cluster builds, build hosts must |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
242 |
be passed explicitly (no registry). |
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
243 |
|
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
244 |
The following build jobs are available: |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
245 |
|
78821
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
246 |
""" + Library.indent_lines(4, show_jobs) + "\n", |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
247 |
"H:" -> (arg => build_hosts ++= Build_Cluster.Host.parse(Registry.load(Nil), arg)), |
80281
17d2f775907a
add cluster/hosts configurations to build manager: allows running jobs in parallel on distinct hardware;
Fabian Huch <huch@in.tum.de>
parents:
80261
diff
changeset
|
248 |
"o:" -> (arg => options = options + arg), |
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
249 |
"u:" -> (arg => url = Some(Url(arg)))) |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
250 |
|
78821
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
251 |
val more_args = getopts(args) |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
252 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
253 |
val job = |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
254 |
more_args match { |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
255 |
case job :: Nil => the_job(job) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
256 |
case _ => getopts.usage() |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
257 |
} |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
258 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
259 |
val progress = new Console_Progress(verbose = true) |
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
260 |
|
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
261 |
ci_build(options, job, url = url, build_hosts = build_hosts.toList, progress = progress) |
78821
4c5aadf1cb48
prefer Isabelle options for CI mail settings over ci.properties;
Fabian Huch <huch@in.tum.de>
parents:
77570
diff
changeset
|
262 |
}) |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
263 |
} |
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
264 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
265 |
class Isabelle_CI_Jobs(val jobs: CI_Build.Job*) extends Isabelle_System.Service |
76222
3c4e373922ca
restructured ci profile into modular ci build system;
Fabian Huch <huch@in.tum.de>
parents:
75633
diff
changeset
|
266 |
|
80411
a9fce67fb8b2
overhauled ci_build: clarified, removed unused, removed implicit Jenkins assumptions;
Fabian Huch <huch@in.tum.de>
parents:
80281
diff
changeset
|
267 |
class CI_Jobs extends Isabelle_CI_Jobs(CI_Build.timing) |