author | wenzelm |
Fri, 03 Mar 2023 13:50:54 +0100 | |
changeset 77495 | c546e3e1f7f6 |
parent 77486 | 032c76e04475 |
child 77496 | f0d9f9196b9b |
permissions | -rw-r--r-- |
77238 | 1 |
/* Title: Pure/Tools/build_process.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Build process for sessions, with build database, optional heap, and |
|
5 |
optional presentation. |
|
6 |
*/ |
|
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
77246 | 11 |
import scala.math.Ordering |
77257 | 12 |
import scala.annotation.tailrec |
77246 | 13 |
|
14 |
||
77238 | 15 |
object Build_Process { |
77436 | 16 |
/** static context **/ |
77238 | 17 |
|
77246 | 18 |
object Context { |
19 |
def apply( |
|
20 |
store: Sessions.Store, |
|
77453 | 21 |
build_deps: Sessions.Deps, |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
22 |
progress: Progress = new Progress, |
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
23 |
hostname: String = Isabelle_System.hostname(), |
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
24 |
numa_shuffling: Boolean = false, |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
25 |
build_heap: Boolean = false, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
26 |
max_jobs: Int = 1, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
27 |
fresh_build: Boolean = false, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
28 |
no_build: Boolean = false, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
29 |
verbose: Boolean = false, |
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
30 |
session_setup: (String, Session) => Unit = (_, _) => (), |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
31 |
uuid: String = UUID.random().toString |
77246 | 32 |
): Context = { |
77453 | 33 |
val sessions_structure = build_deps.sessions_structure |
77247 | 34 |
val build_graph = sessions_structure.build_graph |
35 |
||
77246 | 36 |
val sessions = |
37 |
Map.from( |
|
77448 | 38 |
for ((name, (info, _)) <- build_graph.iterator) |
77249
f3f1b7ad1d0d
clarified data structure: more direct access to timeout;
wenzelm
parents:
77248
diff
changeset
|
39 |
yield { |
77447
566e6e393126
proper deps from build_graph, not imports_graph (amending 0c704aba71e3);
wenzelm
parents:
77446
diff
changeset
|
40 |
val deps = info.parent.toList |
566e6e393126
proper deps from build_graph, not imports_graph (amending 0c704aba71e3);
wenzelm
parents:
77446
diff
changeset
|
41 |
val ancestors = sessions_structure.build_requirements(deps) |
77458 | 42 |
val sources_shasum = build_deps.sources_shasum(name) |
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
43 |
val session_context = |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
44 |
Build_Job.Session_Context.load( |
77458 | 45 |
name, deps, ancestors, sources_shasum, info.timeout, store, progress = progress) |
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
46 |
name -> session_context |
77249
f3f1b7ad1d0d
clarified data structure: more direct access to timeout;
wenzelm
parents:
77248
diff
changeset
|
47 |
}) |
77247 | 48 |
|
77248 | 49 |
val sessions_time = { |
50 |
val maximals = build_graph.maximals.toSet |
|
51 |
def descendants_time(name: String): Double = { |
|
52 |
if (maximals.contains(name)) sessions(name).old_time.seconds |
|
53 |
else { |
|
54 |
val descendants = build_graph.all_succs(List(name)).toSet |
|
55 |
val g = build_graph.restrict(descendants) |
|
56 |
(0.0 :: g.maximals.flatMap { desc => |
|
57 |
val ps = g.all_preds(List(desc)) |
|
58 |
if (ps.exists(p => !sessions.isDefinedAt(p))) None |
|
59 |
else Some(ps.map(p => sessions(p).old_time.seconds).sum) |
|
60 |
}).max |
|
61 |
} |
|
77247 | 62 |
} |
77248 | 63 |
Map.from( |
64 |
for (name <- sessions.keysIterator) |
|
65 |
yield name -> descendants_time(name)).withDefaultValue(0.0) |
|
77247 | 66 |
} |
67 |
||
77246 | 68 |
val ordering = |
69 |
new Ordering[String] { |
|
70 |
def compare(name1: String, name2: String): Int = |
|
77248 | 71 |
sessions_time(name2) compare sessions_time(name1) match { |
77246 | 72 |
case 0 => |
77249
f3f1b7ad1d0d
clarified data structure: more direct access to timeout;
wenzelm
parents:
77248
diff
changeset
|
73 |
sessions(name2).timeout compare sessions(name1).timeout match { |
77246 | 74 |
case 0 => name1 compare name2 |
75 |
case ord => ord |
|
76 |
} |
|
77 |
case ord => ord |
|
78 |
} |
|
79 |
} |
|
80 |
||
77477 | 81 |
val numa_nodes = Host.numa_nodes(enabled = numa_shuffling) |
77457 | 82 |
new Context(store, build_deps, sessions, ordering, progress, hostname, numa_nodes, |
77317
b8ec3c0455db
clarified modules: NUMA is managed by Build_Process;
wenzelm
parents:
77315
diff
changeset
|
83 |
build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build, |
77457 | 84 |
no_build = no_build, verbose = verbose, session_setup, uuid = uuid) |
77246 | 85 |
} |
86 |
} |
|
87 |
||
88 |
final class Context private( |
|
77257 | 89 |
val store: Sessions.Store, |
77453 | 90 |
val build_deps: Sessions.Deps, |
77446
1d447e4fc549
misc tuning: more direct access to ancestors, without build_graph;
wenzelm
parents:
77444
diff
changeset
|
91 |
val sessions: Map[String, Build_Job.Session_Context], |
77257 | 92 |
val ordering: Ordering[String], |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
93 |
val progress: Progress, |
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
94 |
val hostname: String, |
77317
b8ec3c0455db
clarified modules: NUMA is managed by Build_Process;
wenzelm
parents:
77315
diff
changeset
|
95 |
val numa_nodes: List[Int], |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
96 |
val build_heap: Boolean, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
97 |
val max_jobs: Int, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
98 |
val fresh_build: Boolean, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
99 |
val no_build: Boolean, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
100 |
val verbose: Boolean, |
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
101 |
val session_setup: (String, Session) => Unit, |
77457 | 102 |
val uuid: String |
77246 | 103 |
) { |
77470 | 104 |
def build_options: Options = store.options |
105 |
||
106 |
val log: Logger = |
|
107 |
build_options.string("system_log") match { |
|
108 |
case "" => No_Logger |
|
109 |
case "-" => Logger.make(progress) |
|
110 |
case log_file => Logger.make(Some(Path.explode(log_file))) |
|
111 |
} |
|
112 |
||
77453 | 113 |
def sessions_structure: Sessions.Structure = build_deps.sessions_structure |
77257 | 114 |
|
77462 | 115 |
def sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum |
77458 | 116 |
|
77462 | 117 |
def old_command_timings(name: String): List[Properties.T] = |
118 |
sessions.get(name) match { |
|
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
119 |
case Some(session_context) => |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
120 |
Properties.uncompress(session_context.old_command_timings_blob, cache = store.cache) |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
121 |
case None => Nil |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
122 |
} |
77439
d6bf9ec39d12
avoid premature Properties.uncompress: allow blob to be stored in another database;
wenzelm
parents:
77438
diff
changeset
|
123 |
|
77463 | 124 |
def store_heap(name: String): Boolean = |
77462 | 125 |
build_heap || Sessions.is_pure(name) || |
126 |
sessions.valuesIterator.exists(_.ancestors.contains(name)) |
|
77246 | 127 |
} |
77257 | 128 |
|
129 |
||
77436 | 130 |
|
131 |
/** dynamic state **/ |
|
77257 | 132 |
|
77344 | 133 |
case class Entry(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) { |
77313
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
134 |
def is_ready: Boolean = deps.isEmpty |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
135 |
def resolve(dep: String): Entry = |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
136 |
if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
137 |
} |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
138 |
|
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
139 |
case class Result( |
77461 | 140 |
process_result: Process_Result, |
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
141 |
output_shasum: SHA1.Shasum, |
77475 | 142 |
node_info: Host.Node_Info, |
77461 | 143 |
current: Boolean |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
144 |
) { |
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
145 |
def ok: Boolean = process_result.ok |
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
146 |
} |
77312 | 147 |
|
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
148 |
sealed case class State( |
77372 | 149 |
serial: Long = 0, |
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
150 |
numa_index: Int = 0, |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
151 |
pending: List[Entry] = Nil, |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
152 |
running: Map[String, Build_Job] = Map.empty, |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
153 |
results: Map[String, Build_Process.Result] = Map.empty |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
154 |
) { |
77343 | 155 |
def numa_next(numa_nodes: List[Int]): (Option[Int], State) = |
156 |
if (numa_nodes.isEmpty) (None, this) |
|
157 |
else { |
|
158 |
val available = numa_nodes.zipWithIndex |
|
77372 | 159 |
val used = |
160 |
Set.from(for (job <- running.valuesIterator; i <- job.node_info.numa_node) yield i) |
|
77343 | 161 |
val candidates = available.drop(numa_index) ::: available.take(numa_index) |
162 |
val (n, i) = |
|
163 |
candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse |
|
164 |
candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head |
|
165 |
(Some(n), copy(numa_index = (i + 1) % available.length)) |
|
166 |
} |
|
77337 | 167 |
|
77335 | 168 |
def finished: Boolean = pending.isEmpty |
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
169 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
170 |
def remove_pending(name: String): State = |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
171 |
copy(pending = pending.flatMap( |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
172 |
entry => if (entry.name == name) None else Some(entry.resolve(name)))) |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
173 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
174 |
def is_running(name: String): Boolean = running.isDefinedAt(name) |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
175 |
|
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77477
diff
changeset
|
176 |
def stop_running(): Unit = running.valuesIterator.foreach(_.cancel()) |
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
177 |
|
77398
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
178 |
def finished_running(): List[Build_Job] = |
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
179 |
List.from(running.valuesIterator.filter(_.is_finished)) |
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
180 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
181 |
def add_running(name: String, job: Build_Job): State = |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
182 |
copy(running = running + (name -> job)) |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
183 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
184 |
def remove_running(name: String): State = |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
185 |
copy(running = running - name) |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
186 |
|
77336 | 187 |
def make_result( |
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
188 |
name: String, |
77461 | 189 |
process_result: Process_Result, |
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
190 |
output_shasum: SHA1.Shasum, |
77475 | 191 |
node_info: Host.Node_Info = Host.Node_Info.none, |
77461 | 192 |
current: Boolean = false |
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
193 |
): State = { |
77461 | 194 |
val entry = name -> Build_Process.Result(process_result, output_shasum, node_info, current) |
195 |
copy(results = results + entry) |
|
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
196 |
} |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
197 |
} |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
198 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
199 |
|
77436 | 200 |
|
201 |
/** SQL data model **/ |
|
77372 | 202 |
|
203 |
object Data { |
|
204 |
val database = Path.explode("$ISABELLE_HOME_USER/build.db") |
|
205 |
||
206 |
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table = |
|
207 |
SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body) |
|
208 |
||
209 |
object Generic { |
|
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
210 |
val uuid = SQL.Column.string("uuid") |
77372 | 211 |
val name = SQL.Column.string("name") |
212 |
||
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
213 |
def sql_equal(uuid: String = "", name: String = ""): SQL.Source = |
77372 | 214 |
SQL.and( |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
215 |
if_proper(uuid, Generic.uuid.equal(uuid)), |
77372 | 216 |
if_proper(name, Generic.name.equal(name))) |
217 |
||
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
218 |
def sql_member(uuid: String = "", names: Iterable[String] = Nil): SQL.Source = |
77372 | 219 |
SQL.and( |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
220 |
if_proper(uuid, Generic.uuid.equal(uuid)), |
77375 | 221 |
if_proper(names, Generic.name.member(names))) |
77372 | 222 |
} |
223 |
||
77417 | 224 |
object Base { |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
225 |
val uuid = Generic.uuid.make_primary_key |
77387
cd10b8edfdf5
clarified db content: avoid redundancy of historic ML_IDENTIFIER;
wenzelm
parents:
77385
diff
changeset
|
226 |
val ml_platform = SQL.Column.string("ml_platform") |
77372 | 227 |
val options = SQL.Column.string("options") |
228 |
||
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
229 |
val table = make_table("", List(uuid, ml_platform, options)) |
77372 | 230 |
} |
231 |
||
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
232 |
object Serial { |
77372 | 233 |
val serial = SQL.Column.long("serial") |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
234 |
|
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
235 |
val table = make_table("serial", List(serial)) |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
236 |
} |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
237 |
|
77372 | 238 |
object Pending { |
239 |
val name = Generic.name.make_primary_key |
|
240 |
val deps = SQL.Column.string("deps") |
|
241 |
val info = SQL.Column.string("info") |
|
242 |
||
243 |
val table = make_table("pending", List(name, deps, info)) |
|
244 |
} |
|
245 |
||
246 |
object Running { |
|
247 |
val name = Generic.name.make_primary_key |
|
248 |
val hostname = SQL.Column.string("hostname") |
|
249 |
val numa_node = SQL.Column.int("numa_node") |
|
250 |
||
251 |
val table = make_table("running", List(name, hostname, numa_node)) |
|
252 |
} |
|
253 |
||
254 |
object Results { |
|
255 |
val name = Generic.name.make_primary_key |
|
256 |
val hostname = SQL.Column.string("hostname") |
|
257 |
val numa_node = SQL.Column.string("numa_node") |
|
258 |
val rc = SQL.Column.int("rc") |
|
259 |
val out = SQL.Column.string("out") |
|
260 |
val err = SQL.Column.string("err") |
|
261 |
val timing_elapsed = SQL.Column.long("timing_elapsed") |
|
262 |
val timing_cpu = SQL.Column.long("timing_cpu") |
|
263 |
val timing_gc = SQL.Column.long("timing_gc") |
|
264 |
||
265 |
val table = |
|
266 |
make_table("results", |
|
267 |
List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc)) |
|
268 |
} |
|
269 |
||
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
270 |
def get_serial(db: SQL.Database): Long = |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
271 |
db.using_statement(Serial.table.select())(stmt => |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
272 |
stmt.execute_query().iterator(_.long(Serial.serial)).nextOption.getOrElse(0L)) |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
273 |
|
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
274 |
def set_serial(db: SQL.Database, serial: Long): Unit = |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
275 |
if (get_serial(db) != serial) { |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
276 |
db.using_statement(Serial.table.delete())(_.execute()) |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
277 |
db.using_statement(Serial.table.insert()) { stmt => |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
278 |
stmt.long(1) = serial |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
279 |
stmt.execute() |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
280 |
} |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
281 |
} |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
282 |
|
77372 | 283 |
def read_pending(db: SQL.Database): List[Entry] = |
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
284 |
db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt => |
77372 | 285 |
List.from( |
286 |
stmt.execute_query().iterator { res => |
|
287 |
val name = res.string(Pending.name) |
|
288 |
val deps = res.string(Pending.deps) |
|
289 |
val info = res.string(Pending.info) |
|
290 |
Entry(name, split_lines(deps), info = JSON.Object.parse(info)) |
|
291 |
}) |
|
292 |
} |
|
293 |
||
294 |
def update_pending(db: SQL.Database, pending: List[Entry]): Boolean = { |
|
295 |
val old_pending = read_pending(db) |
|
296 |
val (delete, insert) = Library.symmetric_difference(old_pending, pending) |
|
297 |
||
298 |
if (delete.nonEmpty) { |
|
299 |
db.using_statement( |
|
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
300 |
Pending.table.delete( |
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
301 |
sql = SQL.where(Generic.sql_member(names = delete.map(_.name)))))(_.execute()) |
77372 | 302 |
} |
303 |
||
304 |
for (entry <- insert) { |
|
305 |
db.using_statement(Pending.table.insert()) { stmt => |
|
306 |
stmt.string(1) = entry.name |
|
307 |
stmt.string(2) = cat_lines(entry.deps) |
|
308 |
stmt.string(3) = JSON.Format(entry.info) |
|
309 |
stmt.execute() |
|
310 |
} |
|
311 |
} |
|
312 |
||
313 |
delete.nonEmpty || insert.nonEmpty |
|
314 |
} |
|
315 |
||
316 |
def read_running(db: SQL.Database): List[Build_Job.Abstract] = |
|
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
317 |
db.using_statement(Running.table.select(sql = SQL.order_by(List(Running.name)))) { stmt => |
77372 | 318 |
List.from( |
319 |
stmt.execute_query().iterator { res => |
|
320 |
val name = res.string(Running.name) |
|
321 |
val hostname = res.string(Running.hostname) |
|
322 |
val numa_node = res.get_int(Running.numa_node) |
|
77475 | 323 |
Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node)) |
77372 | 324 |
}) |
325 |
} |
|
326 |
||
327 |
def update_running(db: SQL.Database, running: Map[String, Build_Job]): Boolean = { |
|
328 |
val old_running = read_running(db) |
|
329 |
val abs_running = running.valuesIterator.map(_.make_abstract).toList |
|
330 |
||
331 |
val (delete, insert) = Library.symmetric_difference(old_running, abs_running) |
|
332 |
||
333 |
if (delete.nonEmpty) { |
|
334 |
db.using_statement( |
|
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
335 |
Running.table.delete( |
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
336 |
sql = SQL.where(Generic.sql_member(names = delete.map(_.job_name)))))(_.execute()) |
77372 | 337 |
} |
338 |
||
339 |
for (job <- insert) { |
|
340 |
db.using_statement(Running.table.insert()) { stmt => |
|
341 |
stmt.string(1) = job.job_name |
|
342 |
stmt.string(2) = job.node_info.hostname |
|
343 |
stmt.int(3) = job.node_info.numa_node |
|
344 |
stmt.execute() |
|
345 |
} |
|
346 |
} |
|
347 |
||
348 |
delete.nonEmpty || insert.nonEmpty |
|
349 |
} |
|
350 |
||
351 |
def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] = |
|
352 |
db.using_statement( |
|
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
353 |
Results.table.select(sql = if_proper(names, Results.name.where_member(names)))) { stmt => |
77372 | 354 |
Map.from( |
355 |
stmt.execute_query().iterator { res => |
|
356 |
val name = res.string(Results.name) |
|
357 |
val hostname = res.string(Results.hostname) |
|
358 |
val numa_node = res.get_int(Results.numa_node) |
|
359 |
val rc = res.int(Results.rc) |
|
360 |
val out = res.string(Results.out) |
|
361 |
val err = res.string(Results.err) |
|
77495 | 362 |
val timing = |
363 |
res.timing( |
|
364 |
Results.timing_elapsed, |
|
365 |
Results.timing_cpu, |
|
366 |
Results.timing_gc) |
|
77475 | 367 |
val node_info = Host.Node_Info(hostname, numa_node) |
77372 | 368 |
val process_result = |
369 |
Process_Result(rc, |
|
370 |
out_lines = split_lines(out), |
|
371 |
err_lines = split_lines(err), |
|
77495 | 372 |
timing = timing) |
77372 | 373 |
name -> Build_Job.Result(node_info, process_result) |
374 |
}) |
|
375 |
} |
|
376 |
||
377 |
def read_results_name(db: SQL.Database): Set[String] = |
|
77381
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
378 |
db.using_statement(Results.table.select(List(Results.name)))(stmt => |
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
379 |
Set.from(stmt.execute_query().iterator(_.string(Results.name)))) |
77372 | 380 |
|
381 |
def update_results(db: SQL.Database, results: Map[String, Build_Process.Result]): Boolean = { |
|
382 |
val old_results = read_results_name(db) |
|
77385 | 383 |
val insert = results.iterator.filterNot(p => old_results.contains(p._1)).toList |
77372 | 384 |
|
385 |
for ((name, result) <- insert) { |
|
386 |
val node_info = result.node_info |
|
387 |
val process_result = result.process_result |
|
388 |
db.using_statement(Results.table.insert()) { stmt => |
|
389 |
stmt.string(1) = name |
|
390 |
stmt.string(2) = node_info.hostname |
|
391 |
stmt.int(3) = node_info.numa_node |
|
392 |
stmt.int(4) = process_result.rc |
|
393 |
stmt.string(5) = cat_lines(process_result.out_lines) |
|
394 |
stmt.string(6) = cat_lines(process_result.err_lines) |
|
395 |
stmt.long(7) = process_result.timing.elapsed.ms |
|
396 |
stmt.long(8) = process_result.timing.cpu.ms |
|
397 |
stmt.long(9) = process_result.timing.gc.ms |
|
398 |
stmt.execute() |
|
399 |
} |
|
400 |
} |
|
401 |
||
402 |
insert.nonEmpty |
|
403 |
} |
|
404 |
||
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
405 |
def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = { |
77372 | 406 |
val tables = |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
407 |
List( |
77417 | 408 |
Base.table, |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
409 |
Serial.table, |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
410 |
Pending.table, |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
411 |
Running.table, |
77476 | 412 |
Results.table, |
413 |
Host.Data.Node_Info.table) |
|
77372 | 414 |
|
415 |
for (table <- tables) db.create_table(table) |
|
416 |
||
417 |
val old_pending = Data.read_pending(db) |
|
418 |
if (old_pending.nonEmpty) { |
|
419 |
error("Cannot init build process, because of unfinished " + |
|
420 |
commas_quote(old_pending.map(_.name))) |
|
421 |
} |
|
422 |
||
423 |
for (table <- tables) db.using_statement(table.delete())(_.execute()) |
|
424 |
||
77417 | 425 |
db.using_statement(Base.table.insert()) { stmt => |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
426 |
stmt.string(1) = build_context.uuid |
77417 | 427 |
stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM") |
428 |
stmt.string(3) = build_context.store.options.make_prefs(Options.init(prefs = "")) |
|
429 |
stmt.execute() |
|
430 |
} |
|
77372 | 431 |
} |
432 |
||
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
433 |
def update_database( |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
434 |
db: SQL.Database, |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
435 |
uuid: String, |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
436 |
hostname: String, |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
437 |
state: State |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
438 |
): State = { |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
439 |
val changed = |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
440 |
List( |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
441 |
update_pending(db, state.pending), |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
442 |
update_running(db, state.running), |
77476 | 443 |
update_results(db, state.results), |
444 |
Host.Data.update_numa_index(db, hostname, state.numa_index)) |
|
77372 | 445 |
|
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
446 |
val serial0 = get_serial(db) |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
447 |
val serial = if (changed.exists(identity)) serial0 + 1 else serial0 |
77372 | 448 |
|
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
449 |
set_serial(db, serial) |
77372 | 450 |
state.copy(serial = serial) |
451 |
} |
|
452 |
} |
|
77396 | 453 |
} |
77372 | 454 |
|
455 |
||
77436 | 456 |
|
457 |
/** main process **/ |
|
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
458 |
|
77436 | 459 |
class Build_Process(protected val build_context: Build_Process.Context) |
460 |
extends AutoCloseable { |
|
461 |
/* context */ |
|
462 |
||
77338
0a91c697a18a
tuned signature: avoid warnings in IntelliJ IDEA;
wenzelm
parents:
77337
diff
changeset
|
463 |
protected val store: Sessions.Store = build_context.store |
0a91c697a18a
tuned signature: avoid warnings in IntelliJ IDEA;
wenzelm
parents:
77337
diff
changeset
|
464 |
protected val build_options: Options = store.options |
77453 | 465 |
protected val build_deps: Sessions.Deps = build_context.build_deps |
77338
0a91c697a18a
tuned signature: avoid warnings in IntelliJ IDEA;
wenzelm
parents:
77337
diff
changeset
|
466 |
protected val progress: Progress = build_context.progress |
0a91c697a18a
tuned signature: avoid warnings in IntelliJ IDEA;
wenzelm
parents:
77337
diff
changeset
|
467 |
protected val verbose: Boolean = build_context.verbose |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
468 |
|
77436 | 469 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
470 |
/* global state: internal var vs. external database */ |
77436 | 471 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
472 |
private var _state: Build_Process.State = init_state(Build_Process.State()) |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
473 |
|
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
474 |
private val _database: Option[SQL.Database] = |
77390
ff43a524aa5d
clarified system option: guard for testing, until the database layout has stabilized;
wenzelm
parents:
77387
diff
changeset
|
475 |
if (!build_options.bool("build_database_test")) None |
77372 | 476 |
else if (store.database_server) Some(store.open_database_server()) |
77383
cb75171d8c9f
clarified permissions of build.db, following server.db;
wenzelm
parents:
77381
diff
changeset
|
477 |
else { |
cb75171d8c9f
clarified permissions of build.db, following server.db;
wenzelm
parents:
77381
diff
changeset
|
478 |
val db = SQLite.open_database(Build_Process.Data.database) |
cb75171d8c9f
clarified permissions of build.db, following server.db;
wenzelm
parents:
77381
diff
changeset
|
479 |
try { Isabelle_System.chmod("600", Build_Process.Data.database) } |
cb75171d8c9f
clarified permissions of build.db, following server.db;
wenzelm
parents:
77381
diff
changeset
|
480 |
catch { case exn: Throwable => db.close(); throw exn } |
cb75171d8c9f
clarified permissions of build.db, following server.db;
wenzelm
parents:
77381
diff
changeset
|
481 |
Some(db) |
cb75171d8c9f
clarified permissions of build.db, following server.db;
wenzelm
parents:
77381
diff
changeset
|
482 |
} |
77372 | 483 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
484 |
def close(): Unit = synchronized { _database.foreach(_.close()) } |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
485 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
486 |
private def setup_database(): Unit = |
77438 | 487 |
synchronized { |
488 |
for (db <- _database) { |
|
489 |
db.transaction { Build_Process.Data.init_database(db, build_context) } |
|
490 |
db.rebuild() |
|
77436 | 491 |
} |
492 |
} |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
493 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
494 |
protected def synchronized_database[A](body: => A): A = |
77438 | 495 |
synchronized { |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
496 |
_database match { |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
497 |
case None => body |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
498 |
case Some(db) => db.transaction { body } |
77436 | 499 |
} |
500 |
} |
|
501 |
||
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
502 |
private def sync_database(): Unit = |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
503 |
synchronized_database { |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
504 |
for (db <- _database) { |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
505 |
_state = |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
506 |
Build_Process.Data.update_database( |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
507 |
db, build_context.uuid, build_context.hostname, _state) |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
508 |
} |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
509 |
} |
77436 | 510 |
|
511 |
||
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
512 |
/* policy operations */ |
77333 | 513 |
|
77415
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
514 |
protected def init_state(state: Build_Process.State): Build_Process.State = { |
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
515 |
val old_pending = state.pending.iterator.map(_.name).toSet |
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
516 |
val new_pending = |
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
517 |
List.from( |
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
518 |
for { |
77449 | 519 |
(name, session_context) <- build_context.sessions.iterator |
77415
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
520 |
if !old_pending(name) |
77449 | 521 |
} yield Build_Process.Entry(name, session_context.deps)) |
77415
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
522 |
state.copy(pending = new_pending ::: state.pending) |
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
523 |
} |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
524 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
525 |
protected def next_job(state: Build_Process.State): Option[String] = |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
526 |
if (state.running.size < (build_context.max_jobs max 1)) { |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
527 |
state.pending.filter(entry => entry.is_ready && !state.is_running(entry.name)) |
77313
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
528 |
.sortBy(_.name)(build_context.ordering) |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
529 |
.headOption.map(_.name) |
77296
eeaa2872320b
clarified signature: more explicit synchronized operations;
wenzelm
parents:
77295
diff
changeset
|
530 |
} |
eeaa2872320b
clarified signature: more explicit synchronized operations;
wenzelm
parents:
77295
diff
changeset
|
531 |
else None |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
532 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
533 |
protected def start_session(state: Build_Process.State, session_name: String): Build_Process.State = { |
77468 | 534 |
val ancestor_results = |
535 |
for (a <- build_context.sessions(session_name).ancestors) yield state.results(a) |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
536 |
|
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
537 |
val input_shasum = |
77260 | 538 |
if (ancestor_results.isEmpty) { |
539 |
SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) |
|
540 |
} |
|
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
541 |
else SHA1.flat_shasum(ancestor_results.map(_.output_shasum)) |
77257 | 542 |
|
77463 | 543 |
val store_heap = build_context.store_heap(session_name) |
77469 | 544 |
|
545 |
val (current, output_shasum) = |
|
546 |
store.check_output(session_name, |
|
547 |
sources_shasum = build_context.sources_shasum(session_name), |
|
548 |
input_shasum = input_shasum, |
|
549 |
fresh_build = build_context.fresh_build, |
|
550 |
store_heap = store_heap) |
|
551 |
||
77260 | 552 |
val all_current = current && ancestor_results.forall(_.current) |
77257 | 553 |
|
77260 | 554 |
if (all_current) { |
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
555 |
state |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
556 |
.remove_pending(session_name) |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
557 |
.make_result(session_name, Process_Result.ok, output_shasum, current = true) |
77260 | 558 |
} |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
559 |
else if (build_context.no_build) { |
77260 | 560 |
progress.echo_if(verbose, "Skipping " + session_name + " ...") |
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
561 |
state. |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
562 |
remove_pending(session_name). |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
563 |
make_result(session_name, Process_Result.error, output_shasum) |
77260 | 564 |
} |
77452 | 565 |
else if (!ancestor_results.forall(_.ok) || progress.stopped) { |
566 |
progress.echo(session_name + " CANCELLED") |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
567 |
state |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
568 |
.remove_pending(session_name) |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
569 |
.make_result(session_name, Process_Result.undefined, output_shasum) |
77452 | 570 |
} |
571 |
else { |
|
77463 | 572 |
progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...") |
77260 | 573 |
|
77472 | 574 |
store.init_output(session_name) |
77257 | 575 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
576 |
val (numa_node, state1) = state.numa_next(build_context.numa_nodes) |
77475 | 577 |
val node_info = Host.Node_Info(build_context.hostname, numa_node) |
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
578 |
val job = |
77474 | 579 |
Build_Job.start_session( |
77473 | 580 |
build_context, build_deps.background(session_name), input_shasum, node_info) |
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
581 |
state1.add_running(session_name, job) |
77260 | 582 |
} |
583 |
} |
|
77257 | 584 |
|
77436 | 585 |
|
586 |
/* run */ |
|
77372 | 587 |
|
77310 | 588 |
def run(): Map[String, Process_Result] = { |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
589 |
def finished(): Boolean = synchronized_database { _state.finished } |
77400
f3e5b3fe230e
clarified signature: more explicit "synchronized" regions;
wenzelm
parents:
77398
diff
changeset
|
590 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
591 |
def sleep(): Unit = |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
592 |
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
593 |
build_options.seconds("editor_input_delay").sleep() |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
594 |
} |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
595 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
596 |
def start(): Boolean = synchronized_database { |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
597 |
next_job(_state) match { |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
598 |
case Some(name) => |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
599 |
if (Build_Job.is_session_name(name)) { |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
600 |
_state = start_session(_state, name) |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
601 |
true |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
602 |
} |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
603 |
else error("Unsupported build job name " + quote(name)) |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
604 |
case None => false |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
605 |
} |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
606 |
} |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
607 |
|
77335 | 608 |
if (finished()) { |
609 |
progress.echo_warning("Nothing to build") |
|
610 |
Map.empty[String, Process_Result] |
|
611 |
} |
|
612 |
else { |
|
77372 | 613 |
setup_database() |
77335 | 614 |
while (!finished()) { |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
615 |
if (progress.stopped) synchronized_database { _state.stop_running() } |
77310 | 616 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
617 |
for (job <- synchronized_database { _state.finished_running() }) { |
77398
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
618 |
val job_name = job.job_name |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77477
diff
changeset
|
619 |
val (process_result, output_shasum) = job.join |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
620 |
synchronized_database { |
77396 | 621 |
_state = _state. |
77398
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
622 |
remove_pending(job_name). |
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
623 |
remove_running(job_name). |
77461 | 624 |
make_result(job_name, process_result, output_shasum, node_info = job.node_info) |
77396 | 625 |
} |
626 |
} |
|
77260 | 627 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
628 |
if (!start()) { |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
629 |
sync_database() |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
630 |
sleep() |
77310 | 631 |
} |
632 |
} |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
633 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
634 |
synchronized_database { |
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
635 |
for ((name, result) <- _state.results) yield name -> result.process_result |
77257 | 636 |
} |
637 |
} |
|
638 |
} |
|
77238 | 639 |
} |