author | wenzelm |
Wed, 12 Oct 2016 11:48:53 +0200 | |
changeset 64165 | 2e1b25d6c108 |
parent 64160 | 1eea419fab65 |
child 64217 | 3dbfd6758735 |
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 |
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
12 |
import java.util.{Properties => JProperties} |
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 { |
63385 | 22 |
Build.build_selection( |
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, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
25 |
clean_build = true, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
26 |
verbose = true, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
27 |
max_jobs = jobs, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
28 |
dirs = include, |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
29 |
select_dirs = select, |
63385 | 30 |
system_mode = true, |
31 |
selection = select_sessions _) |
|
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
32 |
} |
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
33 |
val end_time = Time.now() |
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
34 |
(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
|
35 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
36 |
|
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
37 |
private def load_properties(): JProperties = |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
38 |
{ |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
39 |
val props = new JProperties() |
63418 | 40 |
val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") |
41 |
||
42 |
if (file_name != "") |
|
43 |
{ |
|
44 |
val file = Path.explode(file_name).file |
|
45 |
if (file.exists()) |
|
46 |
props.load(new java.io.FileReader(file)) |
|
47 |
props |
|
48 |
} |
|
49 |
else |
|
50 |
props |
|
63328
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
51 |
} |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
52 |
|
63385 | 53 |
private def compute_timing(results: Build.Results, group: Option[String]): Timing = |
54 |
{ |
|
55 |
val timings = results.sessions.collect { |
|
56 |
case session if group.forall(results.info(session).groups.contains(_)) => |
|
57 |
results(session).timing |
|
58 |
} |
|
59 |
(Timing.zero /: timings)(_ + _) |
|
60 |
} |
|
61 |
||
63894
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
62 |
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
|
63 |
{ |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
64 |
if (documents) |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
65 |
options |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
66 |
.bool.update("browser_info", true) |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
67 |
.string.update("document", "pdf") |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
68 |
.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
|
69 |
else |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
70 |
options |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
71 |
} |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
72 |
|
63385 | 73 |
|
74 |
final def hg_id(path: Path): String = |
|
64165 | 75 |
Mercurial.repository(path).identify(options = "-i") |
63385 | 76 |
|
77 |
final def print_section(title: String): Unit = |
|
63349 | 78 |
println(s"\n=== $title ===\n") |
79 |
||
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
80 |
|
63385 | 81 |
final val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) |
82 |
final val isabelle_id = hg_id(isabelle_home) |
|
63472 | 83 |
final val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) |
63385 | 84 |
|
85 |
||
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
86 |
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
|
87 |
{ |
63349 | 88 |
print_section("CONFIGURATION") |
64081 | 89 |
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
|
90 |
val props = load_properties() |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
91 |
System.getProperties().putAll(props) |
7a8515c58271
read Java system properties from ISABELLE_CI_PROPERTIES
Lars Hupel <lars.hupel@mytum.de>
parents:
63294
diff
changeset
|
92 |
|
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
93 |
val options = |
63894
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
94 |
with_documents(Options.init()) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
95 |
.int.update("parallel_proofs", 2) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
96 |
.int.update("threads", threads) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
97 |
|
63349 | 98 |
print_section("BUILD") |
63472 | 99 |
println(s"Build started at $start_time") |
100 |
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
|
101 |
pre_hook(args) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
102 |
|
63472 | 103 |
print_section("LOG") |
63387
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
104 |
val (results, elapsed_time) = build(options) |
63349 | 105 |
|
106 |
print_section("TIMING") |
|
63385 | 107 |
|
108 |
val groups = results.sessions.map(results.info).flatMap(_.groups) |
|
109 |
for (group <- groups) |
|
110 |
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
|
111 |
|
3395fe5e3893
more accurate total timing
Lars Hupel <lars.hupel@mytum.de>
parents:
63385
diff
changeset
|
112 |
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
|
113 |
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
|
114 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
115 |
if (!results.ok) { |
63349 | 116 |
print_section("FAILED SESSIONS") |
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 |
for (name <- results.sessions) { |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
119 |
if (results.cancelled(name)) { |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
120 |
println(s"Session $name: CANCELLED") |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
121 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
122 |
else { |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
123 |
val result = results(name) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
124 |
if (!result.ok) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
125 |
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
|
126 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
127 |
} |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
128 |
} |
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 |
post_hook(results) |
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 |
System.exit(results.rc) |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
133 |
} |
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 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
136 |
/* profile */ |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
137 |
|
63894
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
138 |
def documents: Boolean = true |
7534eec7cfad
benchmark doesn't need to build documents
Lars Hupel <lars.hupel@mytum.de>
parents:
63685
diff
changeset
|
139 |
|
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
140 |
def threads: Int |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
141 |
def jobs: Int |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
142 |
def include: List[Path] |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
143 |
def select: List[Path] |
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
144 |
|
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
145 |
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
|
146 |
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
|
147 |
|
63401 | 148 |
def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree) |
63288
e0513d6e4916
start moving actual Jenkins build scripts into the repository
Lars Hupel <lars.hupel@mytum.de>
parents:
diff
changeset
|
149 |
} |