author | Lars Hupel <lars.hupel@mytum.de> |
Thu, 04 Oct 2018 14:52:50 +0200 | |
changeset 69120 | 9d3b41732fe0 |
parent 68498 | 6855ebc61b4f |
child 69121 | 842958af0400 |
permissions | -rw-r--r-- |
64160 | 1 |
/* Title: Pure/Admin/ci_profile.scala |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
2 |
Author: Lars Hupel |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
3 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
4 |
Build profile for continuous integration services. |
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 |
|
64055 | 10 |
import java.time.{Instant, ZoneId} |
63472 | 11 |
import java.time.format.DateTimeFormatter |
68013 | 12 |
import java.util.{Properties => JProperties, Map => JMap} |
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
13 |
|
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
14 |
|
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
15 |
abstract class CI_Profile extends Isabelle_Tool.Body |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
16 |
{ |
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
17 |
private def build(options: Options): (Build.Results, Time) = |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
18 |
{ |
64115 | 19 |
val progress = new Console_Progress(verbose = true) |
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
20 |
val start_time = Time.now() |
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
21 |
val results = progress.interrupt_handler { |
65422 | 22 |
Build.build( |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
23 |
options = options, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
24 |
progress = progress, |
64285
d7e0123a752b
Jenkins: configurable clean build
Lars Hupel <lars.hupel@mytum.de>
parents:
64232
diff
changeset
|
25 |
clean_build = clean, |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
26 |
verbose = true, |
68498
6855ebc61b4f
support NUMA shuffling in CI
Lars Hupel <lars.hupel@mytum.de>
parents:
68013
diff
changeset
|
27 |
numa_shuffling = numa, |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
28 |
max_jobs = jobs, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
29 |
dirs = include, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
30 |
select_dirs = select, |
64286
b2f7aa1c6b75
Jenkins: build in system mode again
Lars Hupel <lars.hupel@mytum.de>
parents:
64285
diff
changeset
|
31 |
system_mode = true, |
65419 | 32 |
selection = selection) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
33 |
} |
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
34 |
val end_time = Time.now() |
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
35 |
(results, end_time - start_time) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
36 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
37 |
|
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
38 |
private def load_properties(): JProperties = |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
39 |
{ |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
40 |
val props = new JProperties() |
63418 | 41 |
val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") |
42 |
||
43 |
if (file_name != "") |
|
44 |
{ |
|
45 |
val file = Path.explode(file_name).file |
|
46 |
if (file.exists()) |
|
47 |
props.load(new java.io.FileReader(file)) |
|
48 |
props |
|
49 |
} |
|
50 |
else |
|
51 |
props |
|
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
52 |
} |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
53 |
|
63385 | 54 |
private def compute_timing(results: Build.Results, group: Option[String]): Timing = |
55 |
{ |
|
56 |
val timings = results.sessions.collect { |
|
57 |
case session if group.forall(results.info(session).groups.contains(_)) => |
|
58 |
results(session).timing |
|
59 |
} |
|
60 |
(Timing.zero /: timings)(_ + _) |
|
61 |
} |
|
62 |
||
63894
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
63 |
private def with_documents(options: Options): Options = |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
64 |
{ |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
65 |
if (documents) |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
66 |
options |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
67 |
.bool.update("browser_info", true) |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
68 |
.string.update("document", "pdf") |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
69 |
.string.update("document_variants", "document:outline=/proof,/ML") |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
70 |
else |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
71 |
options |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
72 |
} |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
73 |
|
63385 | 74 |
|
75 |
final def hg_id(path: Path): String = |
|
64232
367d83d6030e
clarified hg.id operation, with explicit tip as default;
wenzelm
parents:
64217
diff
changeset
|
76 |
Mercurial.repository(path).id() |
63385 | 77 |
|
78 |
final def print_section(title: String): Unit = |
|
63349 | 79 |
println(s"\n=== $title ===\n") |
80 |
||
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
81 |
|
63385 | 82 |
final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) |
83 |
final val isabelle_id = hg_id(isabelle_home) |
|
63472 | 84 |
final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) |
63385 | 85 |
|
86 |
||
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
87 |
override final def apply(args: List[String]): Unit = |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
88 |
{ |
63349 | 89 |
print_section("CONFIGURATION") |
64081 | 90 |
println(Build_Log.Settings.show()) |
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
91 |
val props = load_properties() |
68013 | 92 |
System.getProperties().asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props) |
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
93 |
|
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
94 |
val options = |
63894
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
95 |
with_documents(Options.init()) |
65056 | 96 |
.int.update("parallel_proofs", 1) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
97 |
.int.update("threads", threads) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
98 |
|
69120
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
99 |
println(s"jobs = $jobs, threads = $threads, numa = $numa") |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
100 |
|
63349 | 101 |
print_section("BUILD") |
63472 | 102 |
println(s"Build started at $start_time") |
103 |
println(s"Isabelle id $isabelle_id") |
|
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
104 |
pre_hook(args) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
105 |
|
63472 | 106 |
print_section("LOG") |
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
107 |
val (results, elapsed_time) = build(options) |
63349 | 108 |
|
109 |
print_section("TIMING") |
|
63385 | 110 |
|
111 |
val groups = results.sessions.map(results.info).flatMap(_.groups) |
|
112 |
for (group <- groups) |
|
113 |
println(s"Group $group: " + compute_timing(results, Some(group)).message_resources) |
|
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
114 |
|
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
115 |
val total_timing = compute_timing(results, None).copy(elapsed = elapsed_time) |
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
116 |
println("Overall: " + total_timing.message_resources) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
117 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
118 |
if (!results.ok) { |
63349 | 119 |
print_section("FAILED SESSIONS") |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
120 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
121 |
for (name <- results.sessions) { |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
122 |
if (results.cancelled(name)) { |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
123 |
println(s"Session $name: CANCELLED") |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
124 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
125 |
else { |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
126 |
val result = results(name) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
127 |
if (!result.ok) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
128 |
println(s"Session $name: FAILED ${result.rc}") |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
129 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
130 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
131 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
132 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
133 |
post_hook(results) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
134 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
135 |
System.exit(results.rc) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
136 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
137 |
|
69120
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
138 |
/* profile */ |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
139 |
|
69120
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
140 |
def threads: Int = Isabelle_System.hostname() match { |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
141 |
case "hpcisabelle" => 8 |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
142 |
case "lxcisa0" => 4 |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
143 |
case _ => 2 |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
144 |
} |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
145 |
|
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
146 |
def jobs: Int = Isabelle_System.hostname() match { |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
147 |
case "hpcisabelle" => 8 |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
148 |
case "lxcisa0" => 10 |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
149 |
case _ => 2 |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
150 |
} |
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
151 |
|
9d3b41732fe0
Jenkins: detect machine; adjust job parameters accordingly
Lars Hupel <lars.hupel@mytum.de>
parents:
68498
diff
changeset
|
152 |
def numa: Boolean = Isabelle_System.hostname() == "hpcisabelle" |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
153 |
|
63894
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
154 |
def documents: Boolean = true |
64285
d7e0123a752b
Jenkins: configurable clean build
Lars Hupel <lars.hupel@mytum.de>
parents:
64232
diff
changeset
|
155 |
def clean: Boolean = true |
63894
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
156 |
|
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
157 |
def include: List[Path] |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
158 |
def select: List[Path] |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
159 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
160 |
def pre_hook(args: List[String]): Unit |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
161 |
def post_hook(results: Build.Results): Unit |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
162 |
|
65419 | 163 |
def selection: Sessions.Selection |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
164 |
} |