36 } |
36 } |
37 } |
37 } |
38 } |
38 } |
39 |
39 |
40 |
40 |
41 /* Config */ |
41 /* Build_Config */ |
42 |
42 |
43 case class Build_Config( |
43 case class Build_Config( |
44 documents: Boolean = true, |
44 documents: Boolean = true, |
45 clean: Boolean = true, |
45 clean: Boolean = true, |
46 include: List[Path] = Nil, |
46 include: List[Path] = Nil, |
47 select: List[Path] = Nil, |
47 select: List[Path] = Nil, |
48 pre_hook: () => Result = () => { Result.ok }, |
48 pre_hook: () => Result = () => Result.ok, |
49 post_hook: Build.Results => Result = { _ => Result.ok }, |
49 post_hook: Build.Results => Result = _ => Result.ok, |
50 selection: Sessions.Selection = Sessions.Selection.empty |
50 selection: Sessions.Selection = Sessions.Selection.empty |
51 ) |
51 ) |
52 |
52 |
53 |
53 |
54 /* Status */ |
54 /* Status */ |
65 object Status { |
65 object Status { |
66 def merge(statuses: List[Status]): Status = |
66 def merge(statuses: List[Status]): Status = |
67 statuses.foldLeft(Ok: Status)(_ merge _) |
67 statuses.foldLeft(Ok: Status)(_ merge _) |
68 |
68 |
69 def from_results(results: Build.Results, session: String): Status = |
69 def from_results(results: Build.Results, session: String): Status = |
70 if (results.cancelled(session)) |
70 if (results.cancelled(session)) Skipped |
71 Skipped |
71 else if (results(session).ok) Ok |
72 else if (results(session).ok) |
72 else Failed |
73 Ok |
|
74 else |
|
75 Failed |
|
76 } |
73 } |
77 |
74 |
78 case object Ok extends Status("ok") |
75 case object Ok extends Status("ok") |
79 case object Skipped extends Status("skipped") |
76 case object Skipped extends Status("skipped") |
80 case object Failed extends Status("failed") |
77 case object Failed extends Status("failed") |
84 val props = new JProperties() |
81 val props = new JProperties() |
85 val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") |
82 val file_name = Isabelle_System.getenv("ISABELLE_CI_PROPERTIES") |
86 |
83 |
87 if (file_name != "") { |
84 if (file_name != "") { |
88 val file = Path.explode(file_name).file |
85 val file = Path.explode(file_name).file |
89 if (file.exists()) |
86 if (file.exists()) props.load(new java.io.FileReader(file)) |
90 props.load(new java.io.FileReader(file)) |
|
91 props |
87 props |
92 } |
88 } |
93 else |
89 else props |
94 props |
|
95 } |
90 } |
96 |
91 |
97 private def compute_timing(results: Build.Results, group: Option[String]): Timing = { |
92 private def compute_timing(results: Build.Results, group: Option[String]): Timing = { |
98 val timings = results.sessions.collect { |
93 val timings = |
99 case session if group.forall(results.info(session).groups.contains(_)) => |
94 results.sessions.collect { |
100 results(session).timing |
95 case session if group.forall(results.info(session).groups.contains(_)) => |
101 } |
96 results(session).timing |
|
97 } |
102 timings.foldLeft(Timing.zero)(_ + _) |
98 timings.foldLeft(Timing.zero)(_ + _) |
103 } |
99 } |
104 |
100 |
105 private def with_documents(options: Options, config: Build_Config): Options = { |
101 private def with_documents(options: Options, config: Build_Config): Options = { |
106 if (config.documents) |
102 if (config.documents) { |
107 options |
103 options |
108 .bool.update("browser_info", true) |
104 .bool.update("browser_info", true) |
109 .string.update("document", "pdf") |
105 .string.update("document", "pdf") |
110 .string.update("document_variants", "document:outline=/proof,/ML") |
106 .string.update("document_variants", "document:outline=/proof,/ML") |
111 else |
107 } |
112 options |
108 else options |
113 } |
109 } |
114 |
110 |
115 def hg_id(path: Path): String = |
111 def hg_id(path: Path): String = |
116 Mercurial.repository(path).id() |
112 Mercurial.repository(path).id() |
117 |
113 |
120 |
116 |
121 def build(profile: Profile, config: Build_Config): Unit = { |
117 def build(profile: Profile, config: Build_Config): Unit = { |
122 val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) |
118 val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME")) |
123 val isabelle_id = hg_id(isabelle_home) |
119 val isabelle_id = hg_id(isabelle_home) |
124 |
120 |
125 val start_time = Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) |
121 val start_time = |
|
122 Instant.now().atZone(ZoneId.systemDefault).format(DateTimeFormatter.RFC_1123_DATE_TIME) |
126 |
123 |
127 print_section("CONFIGURATION") |
124 print_section("CONFIGURATION") |
128 println(Build_Log.Settings.show()) |
125 println(Build_Log.Settings.show()) |
129 val props = load_properties() |
126 val props = load_properties() |
130 System.getProperties.asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props) |
127 System.getProperties.asInstanceOf[JMap[AnyRef, AnyRef]].putAll(props) |
172 |
169 |
173 if (!results.ok) { |
170 if (!results.ok) { |
174 print_section("FAILED SESSIONS") |
171 print_section("FAILED SESSIONS") |
175 |
172 |
176 for (name <- results.sessions) { |
173 for (name <- results.sessions) { |
177 if (results.cancelled(name)) { |
174 if (results.cancelled(name)) println(s"Session $name: CANCELLED") |
178 println(s"Session $name: CANCELLED") |
|
179 } |
|
180 else { |
175 else { |
181 val result = results(name) |
176 val result = results(name) |
182 if (!result.ok) |
177 if (!result.ok) println(s"Session $name: FAILED ${ result.rc }") |
183 println(s"Session $name: FAILED ${ result.rc }") |
|
184 } |
178 } |
185 } |
179 } |
186 } |
180 } |
187 |
181 |
188 val post_result = config.post_hook(results) |
182 val post_result = config.post_hook(results) |