author | wenzelm |
Sun, 05 Mar 2023 18:18:09 +0100 | |
changeset 77522 | a1d30297cd61 |
parent 77521 | 5642de4d225d |
child 77525 | de6fb423fd4b |
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 |
||
77505 | 11 |
import scala.collection.immutable.SortedMap |
77246 | 12 |
import scala.math.Ordering |
77257 | 13 |
import scala.annotation.tailrec |
77246 | 14 |
|
15 |
||
77238 | 16 |
object Build_Process { |
77436 | 17 |
/** static context **/ |
77238 | 18 |
|
77246 | 19 |
object Context { |
20 |
def apply( |
|
21 |
store: Sessions.Store, |
|
77453 | 22 |
build_deps: Sessions.Deps, |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
23 |
progress: Progress = new Progress, |
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
24 |
hostname: String = Isabelle_System.hostname(), |
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
25 |
numa_shuffling: Boolean = false, |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
26 |
build_heap: Boolean = false, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
27 |
max_jobs: Int = 1, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
28 |
fresh_build: Boolean = false, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
29 |
no_build: 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( |
77496 | 45 |
uuid, name, deps, ancestors, sources_shasum, info.timeout, store, |
46 |
progress = progress) |
|
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
47 |
name -> session_context |
77249
f3f1b7ad1d0d
clarified data structure: more direct access to timeout;
wenzelm
parents:
77248
diff
changeset
|
48 |
}) |
77247 | 49 |
|
77248 | 50 |
val sessions_time = { |
51 |
val maximals = build_graph.maximals.toSet |
|
52 |
def descendants_time(name: String): Double = { |
|
53 |
if (maximals.contains(name)) sessions(name).old_time.seconds |
|
54 |
else { |
|
55 |
val descendants = build_graph.all_succs(List(name)).toSet |
|
56 |
val g = build_graph.restrict(descendants) |
|
57 |
(0.0 :: g.maximals.flatMap { desc => |
|
58 |
val ps = g.all_preds(List(desc)) |
|
59 |
if (ps.exists(p => !sessions.isDefinedAt(p))) None |
|
60 |
else Some(ps.map(p => sessions(p).old_time.seconds).sum) |
|
61 |
}).max |
|
62 |
} |
|
77247 | 63 |
} |
77248 | 64 |
Map.from( |
65 |
for (name <- sessions.keysIterator) |
|
66 |
yield name -> descendants_time(name)).withDefaultValue(0.0) |
|
77247 | 67 |
} |
68 |
||
77246 | 69 |
val ordering = |
70 |
new Ordering[String] { |
|
71 |
def compare(name1: String, name2: String): Int = |
|
77248 | 72 |
sessions_time(name2) compare sessions_time(name1) match { |
77246 | 73 |
case 0 => |
77249
f3f1b7ad1d0d
clarified data structure: more direct access to timeout;
wenzelm
parents:
77248
diff
changeset
|
74 |
sessions(name2).timeout compare sessions(name1).timeout match { |
77246 | 75 |
case 0 => name1 compare name2 |
76 |
case ord => ord |
|
77 |
} |
|
78 |
case ord => ord |
|
79 |
} |
|
80 |
} |
|
81 |
||
77477 | 82 |
val numa_nodes = Host.numa_nodes(enabled = numa_shuffling) |
77505 | 83 |
new Context(store, build_deps, sessions, ordering, hostname, numa_nodes, |
77317
b8ec3c0455db
clarified modules: NUMA is managed by Build_Process;
wenzelm
parents:
77315
diff
changeset
|
84 |
build_heap = build_heap, max_jobs = max_jobs, fresh_build = fresh_build, |
77521
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77514
diff
changeset
|
85 |
no_build = no_build, session_setup, uuid = uuid) |
77246 | 86 |
} |
87 |
} |
|
88 |
||
77496 | 89 |
// static context of one particular instance, identified by uuid |
77246 | 90 |
final class Context private( |
77257 | 91 |
val store: Sessions.Store, |
77453 | 92 |
val build_deps: Sessions.Deps, |
77496 | 93 |
val sessions: State.Sessions, |
77257 | 94 |
val ordering: Ordering[String], |
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
95 |
val hostname: String, |
77317
b8ec3c0455db
clarified modules: NUMA is managed by Build_Process;
wenzelm
parents:
77315
diff
changeset
|
96 |
val numa_nodes: List[Int], |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
97 |
val build_heap: Boolean, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
98 |
val max_jobs: Int, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
99 |
val fresh_build: Boolean, |
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
100 |
val no_build: 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 |
||
77453 | 106 |
def sessions_structure: Sessions.Structure = build_deps.sessions_structure |
77257 | 107 |
|
77462 | 108 |
def sources_shasum(name: String): SHA1.Shasum = sessions(name).sources_shasum |
77458 | 109 |
|
77462 | 110 |
def old_command_timings(name: String): List[Properties.T] = |
111 |
sessions.get(name) match { |
|
77444
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
112 |
case Some(session_context) => |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
113 |
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
|
114 |
case None => Nil |
0c704aba71e3
clarified signature: reduce explicit access to static Sessions.Structure;
wenzelm
parents:
77443
diff
changeset
|
115 |
} |
77439
d6bf9ec39d12
avoid premature Properties.uncompress: allow blob to be stored in another database;
wenzelm
parents:
77438
diff
changeset
|
116 |
|
77514 | 117 |
def open_database(): Option[SQL.Database] = |
118 |
if (!build_options.bool("build_database_test")) None |
|
119 |
else if (store.database_server) Some(store.open_database_server()) |
|
120 |
else { |
|
121 |
val db = SQLite.open_database(Build_Process.Data.database) |
|
122 |
try { Isabelle_System.chmod("600", Build_Process.Data.database) } |
|
123 |
catch { case exn: Throwable => db.close(); throw exn } |
|
124 |
Some(db) |
|
125 |
} |
|
126 |
||
77463 | 127 |
def store_heap(name: String): Boolean = |
77462 | 128 |
build_heap || Sessions.is_pure(name) || |
129 |
sessions.valuesIterator.exists(_.ancestors.contains(name)) |
|
77246 | 130 |
} |
77257 | 131 |
|
132 |
||
77436 | 133 |
|
134 |
/** dynamic state **/ |
|
77257 | 135 |
|
77505 | 136 |
type Progress_Messages = SortedMap[Long, Progress.Message] |
137 |
||
77344 | 138 |
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
|
139 |
def is_ready: Boolean = deps.isEmpty |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
140 |
def resolve(dep: String): Entry = |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
141 |
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
|
142 |
} |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
143 |
|
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
144 |
case class Result( |
77461 | 145 |
process_result: Process_Result, |
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
146 |
output_shasum: SHA1.Shasum, |
77475 | 147 |
node_info: Host.Node_Info, |
77461 | 148 |
current: Boolean |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
149 |
) { |
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
150 |
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
|
151 |
} |
77312 | 152 |
|
77496 | 153 |
object State { |
154 |
type Sessions = Map[String, Build_Job.Session_Context] |
|
155 |
type Pending = List[Entry] |
|
156 |
type Running = Map[String, Build_Job] |
|
157 |
type Results = Map[String, Result] |
|
77513 | 158 |
|
159 |
def inc_serial(serial: Long): Long = { |
|
160 |
require(serial < java.lang.Long.MAX_VALUE, "serial overflow") |
|
161 |
serial + 1 |
|
162 |
} |
|
77496 | 163 |
} |
164 |
||
165 |
// dynamic state of various instances, distinguished by uuid |
|
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
166 |
sealed case class State( |
77372 | 167 |
serial: Long = 0, |
77505 | 168 |
progress_seen: 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
|
169 |
numa_index: Int = 0, |
77496 | 170 |
sessions: State.Sessions = Map.empty, // static build targets |
171 |
pending: State.Pending = Nil, // dynamic build "queue" |
|
172 |
running: State.Running = Map.empty, // presently running jobs |
|
173 |
results: State.Results = Map.empty // finished results |
|
77334
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
174 |
) { |
77513 | 175 |
require(serial >= 0, "serial underflow") |
176 |
def inc_serial: State = copy(serial = State.inc_serial(serial)) |
|
177 |
def set_serial(i: Long): State = { |
|
178 |
require(serial <= i, "non-monotonic change of serial") |
|
179 |
copy(serial = i) |
|
180 |
} |
|
181 |
||
77522
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
182 |
def progress_serial(message_serial: Long = serial): State = |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
183 |
if (message_serial > progress_seen) copy(progress_seen = message_serial) |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
184 |
else error("Bad serial " + message_serial + " for progress output (already seen)") |
77505 | 185 |
|
77343 | 186 |
def numa_next(numa_nodes: List[Int]): (Option[Int], State) = |
187 |
if (numa_nodes.isEmpty) (None, this) |
|
188 |
else { |
|
189 |
val available = numa_nodes.zipWithIndex |
|
77372 | 190 |
val used = |
191 |
Set.from(for (job <- running.valuesIterator; i <- job.node_info.numa_node) yield i) |
|
77343 | 192 |
val candidates = available.drop(numa_index) ::: available.take(numa_index) |
193 |
val (n, i) = |
|
194 |
candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse |
|
195 |
candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head |
|
196 |
(Some(n), copy(numa_index = (i + 1) % available.length)) |
|
197 |
} |
|
77337 | 198 |
|
77335 | 199 |
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
|
200 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
201 |
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
|
202 |
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
|
203 |
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
|
204 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
205 |
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
|
206 |
|
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77477
diff
changeset
|
207 |
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
|
208 |
|
77398
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
209 |
def finished_running(): List[Build_Job] = |
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
210 |
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
|
211 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
212 |
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
|
213 |
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
|
214 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
215 |
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
|
216 |
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
|
217 |
|
77336 | 218 |
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
|
219 |
name: String, |
77461 | 220 |
process_result: Process_Result, |
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
221 |
output_shasum: SHA1.Shasum, |
77475 | 222 |
node_info: Host.Node_Info = Host.Node_Info.none, |
77461 | 223 |
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
|
224 |
): State = { |
77461 | 225 |
val entry = name -> Build_Process.Result(process_result, output_shasum, node_info, current) |
226 |
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
|
227 |
} |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
228 |
} |
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
229 |
|
0231e62956a6
clarified state: more explicit type as plain value, which is also easier to sync with external db;
wenzelm
parents:
77333
diff
changeset
|
230 |
|
77436 | 231 |
|
232 |
/** SQL data model **/ |
|
77372 | 233 |
|
234 |
object Data { |
|
235 |
val database = Path.explode("$ISABELLE_HOME_USER/build.db") |
|
236 |
||
237 |
def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table = |
|
238 |
SQL.Table("isabelle_build" + if_proper(name, "_" + name), columns, body = body) |
|
239 |
||
240 |
object Generic { |
|
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
241 |
val uuid = SQL.Column.string("uuid") |
77372 | 242 |
val name = SQL.Column.string("name") |
243 |
||
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
244 |
def sql_equal(uuid: String = "", name: String = ""): SQL.Source = |
77372 | 245 |
SQL.and( |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
246 |
if_proper(uuid, Generic.uuid.equal(uuid)), |
77372 | 247 |
if_proper(name, Generic.name.equal(name))) |
248 |
||
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
249 |
def sql_member(uuid: String = "", names: Iterable[String] = Nil): SQL.Source = |
77372 | 250 |
SQL.and( |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
251 |
if_proper(uuid, Generic.uuid.equal(uuid)), |
77375 | 252 |
if_proper(names, Generic.name.member(names))) |
77372 | 253 |
} |
254 |
||
77417 | 255 |
object Base { |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
256 |
val uuid = Generic.uuid.make_primary_key |
77387
cd10b8edfdf5
clarified db content: avoid redundancy of historic ML_IDENTIFIER;
wenzelm
parents:
77385
diff
changeset
|
257 |
val ml_platform = SQL.Column.string("ml_platform") |
77372 | 258 |
val options = SQL.Column.string("options") |
259 |
||
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
260 |
val table = make_table("", List(uuid, ml_platform, options)) |
77372 | 261 |
} |
262 |
||
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
263 |
object Serial { |
77372 | 264 |
val serial = SQL.Column.long("serial") |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
265 |
|
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
266 |
val table = make_table("serial", List(serial)) |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
267 |
} |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
268 |
|
77505 | 269 |
object Progress { |
270 |
val serial = SQL.Column.long("serial").make_primary_key |
|
271 |
val kind = SQL.Column.int("kind") |
|
272 |
val text = SQL.Column.string("text") |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
273 |
val verbose = SQL.Column.bool("verbose") |
77505 | 274 |
val uuid = Generic.uuid |
275 |
||
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
276 |
val table = make_table("progress", List(serial, kind, text, verbose, uuid)) |
77505 | 277 |
} |
278 |
||
77496 | 279 |
object Sessions { |
280 |
val name = Generic.name.make_primary_key |
|
281 |
val deps = SQL.Column.string("deps") |
|
282 |
val ancestors = SQL.Column.string("ancestors") |
|
283 |
val sources = SQL.Column.string("sources") |
|
284 |
val timeout = SQL.Column.long("timeout") |
|
285 |
val old_time = SQL.Column.long("old_time") |
|
286 |
val old_command_timings = SQL.Column.bytes("old_command_timings") |
|
287 |
val uuid = Generic.uuid |
|
288 |
||
289 |
val table = make_table("sessions", |
|
290 |
List(name, deps, ancestors, sources, timeout, old_time, old_command_timings, uuid)) |
|
291 |
} |
|
292 |
||
77372 | 293 |
object Pending { |
294 |
val name = Generic.name.make_primary_key |
|
295 |
val deps = SQL.Column.string("deps") |
|
296 |
val info = SQL.Column.string("info") |
|
297 |
||
298 |
val table = make_table("pending", List(name, deps, info)) |
|
299 |
} |
|
300 |
||
301 |
object Running { |
|
302 |
val name = Generic.name.make_primary_key |
|
303 |
val hostname = SQL.Column.string("hostname") |
|
304 |
val numa_node = SQL.Column.int("numa_node") |
|
305 |
||
306 |
val table = make_table("running", List(name, hostname, numa_node)) |
|
307 |
} |
|
308 |
||
309 |
object Results { |
|
310 |
val name = Generic.name.make_primary_key |
|
311 |
val hostname = SQL.Column.string("hostname") |
|
312 |
val numa_node = SQL.Column.string("numa_node") |
|
313 |
val rc = SQL.Column.int("rc") |
|
314 |
val out = SQL.Column.string("out") |
|
315 |
val err = SQL.Column.string("err") |
|
316 |
val timing_elapsed = SQL.Column.long("timing_elapsed") |
|
317 |
val timing_cpu = SQL.Column.long("timing_cpu") |
|
318 |
val timing_gc = SQL.Column.long("timing_gc") |
|
319 |
||
320 |
val table = |
|
321 |
make_table("results", |
|
322 |
List(name, hostname, numa_node, rc, out, err, timing_elapsed, timing_cpu, timing_gc)) |
|
323 |
} |
|
324 |
||
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
325 |
def get_serial(db: SQL.Database): Long = |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
326 |
db.using_statement(Serial.table.select())(stmt => |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
327 |
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
|
328 |
|
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
329 |
def set_serial(db: SQL.Database, serial: Long): Unit = |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
330 |
if (get_serial(db) != serial) { |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
331 |
db.using_statement(Serial.table.delete())(_.execute()) |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
332 |
db.using_statement(Serial.table.insert()) { stmt => |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
333 |
stmt.long(1) = serial |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
334 |
stmt.execute() |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
335 |
} |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
336 |
} |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
337 |
|
77505 | 338 |
def read_progress(db: SQL.Database, seen: Long = 0, uuid: String = ""): Progress_Messages = |
339 |
db.using_statement( |
|
340 |
Progress.table.select( |
|
341 |
sql = |
|
342 |
SQL.where( |
|
343 |
SQL.and( |
|
344 |
if (seen <= 0) "" else Progress.serial.ident + " > " + seen, |
|
345 |
Generic.sql_equal(uuid = uuid)))) |
|
346 |
) { stmt => |
|
347 |
SortedMap.from(stmt.execute_query().iterator { res => |
|
348 |
val serial = res.long(Progress.serial) |
|
349 |
val kind = isabelle.Progress.Kind(res.int(Progress.kind)) |
|
350 |
val text = res.string(Progress.text) |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
351 |
val verbose = res.bool(Progress.verbose) |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
352 |
serial -> isabelle.Progress.Message(kind, text, verbose = verbose) |
77505 | 353 |
}) |
354 |
} |
|
355 |
||
356 |
def write_progress( |
|
357 |
db: SQL.Database, |
|
358 |
message_serial: Long, |
|
359 |
message: isabelle.Progress.Message, |
|
360 |
uuid: String |
|
361 |
): Unit = { |
|
362 |
db.using_statement(Progress.table.insert()) { stmt => |
|
363 |
stmt.long(1) = message_serial |
|
364 |
stmt.int(2) = message.kind.id |
|
365 |
stmt.string(3) = message.text |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
366 |
stmt.bool(4) = message.verbose |
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
367 |
stmt.string(5) = uuid |
77505 | 368 |
stmt.execute() |
369 |
} |
|
370 |
} |
|
371 |
||
77496 | 372 |
def read_sessions_domain(db: SQL.Database): Set[String] = |
373 |
db.using_statement(Sessions.table.select(List(Sessions.name)))(stmt => |
|
374 |
Set.from(stmt.execute_query().iterator(_.string(Sessions.name)))) |
|
375 |
||
376 |
def read_sessions(db: SQL.Database, names: Iterable[String] = Nil): State.Sessions = |
|
377 |
db.using_statement( |
|
378 |
Sessions.table.select(sql = if_proper(names, Sessions.name.where_member(names))) |
|
379 |
) { stmt => |
|
380 |
Map.from(stmt.execute_query().iterator { res => |
|
381 |
val name = res.string(Sessions.name) |
|
382 |
val deps = split_lines(res.string(Sessions.deps)) |
|
383 |
val ancestors = split_lines(res.string(Sessions.ancestors)) |
|
384 |
val sources_shasum = SHA1.fake_shasum(res.string(Sessions.sources)) |
|
385 |
val timeout = Time.ms(res.long(Sessions.timeout)) |
|
386 |
val old_time = Time.ms(res.long(Sessions.old_time)) |
|
387 |
val old_command_timings_blob = res.bytes(Sessions.old_command_timings) |
|
388 |
val uuid = res.string(Sessions.uuid) |
|
389 |
name -> Build_Job.Session_Context(name, deps, ancestors, sources_shasum, |
|
390 |
timeout, old_time, old_command_timings_blob, uuid) |
|
391 |
}) |
|
392 |
} |
|
393 |
||
394 |
def update_sessions(db:SQL.Database, sessions: State.Sessions): Boolean = { |
|
395 |
val old_sessions = read_sessions_domain(db) |
|
396 |
val insert = sessions.iterator.filterNot(p => old_sessions.contains(p._1)).toList |
|
397 |
||
398 |
for ((name, session) <- insert) { |
|
399 |
db.using_statement(Sessions.table.insert()) { stmt => |
|
400 |
stmt.string(1) = name |
|
401 |
stmt.string(2) = cat_lines(session.deps) |
|
402 |
stmt.string(3) = cat_lines(session.ancestors) |
|
403 |
stmt.string(4) = session.sources_shasum.toString |
|
404 |
stmt.long(5) = session.timeout.ms |
|
405 |
stmt.long(6) = session.old_time.ms |
|
406 |
stmt.bytes(7) = session.old_command_timings_blob |
|
407 |
stmt.string(8) = session.uuid |
|
408 |
stmt.execute() |
|
409 |
} |
|
410 |
} |
|
411 |
||
412 |
insert.nonEmpty |
|
413 |
} |
|
414 |
||
77372 | 415 |
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
|
416 |
db.using_statement(Pending.table.select(sql = SQL.order_by(List(Pending.name)))) { stmt => |
77372 | 417 |
List.from( |
418 |
stmt.execute_query().iterator { res => |
|
419 |
val name = res.string(Pending.name) |
|
420 |
val deps = res.string(Pending.deps) |
|
421 |
val info = res.string(Pending.info) |
|
422 |
Entry(name, split_lines(deps), info = JSON.Object.parse(info)) |
|
423 |
}) |
|
424 |
} |
|
425 |
||
77496 | 426 |
def update_pending(db: SQL.Database, pending: State.Pending): Boolean = { |
77372 | 427 |
val old_pending = read_pending(db) |
428 |
val (delete, insert) = Library.symmetric_difference(old_pending, pending) |
|
429 |
||
430 |
if (delete.nonEmpty) { |
|
431 |
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
|
432 |
Pending.table.delete( |
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
433 |
sql = SQL.where(Generic.sql_member(names = delete.map(_.name)))))(_.execute()) |
77372 | 434 |
} |
435 |
||
436 |
for (entry <- insert) { |
|
437 |
db.using_statement(Pending.table.insert()) { stmt => |
|
438 |
stmt.string(1) = entry.name |
|
439 |
stmt.string(2) = cat_lines(entry.deps) |
|
440 |
stmt.string(3) = JSON.Format(entry.info) |
|
441 |
stmt.execute() |
|
442 |
} |
|
443 |
} |
|
444 |
||
445 |
delete.nonEmpty || insert.nonEmpty |
|
446 |
} |
|
447 |
||
448 |
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
|
449 |
db.using_statement(Running.table.select(sql = SQL.order_by(List(Running.name)))) { stmt => |
77372 | 450 |
List.from( |
451 |
stmt.execute_query().iterator { res => |
|
452 |
val name = res.string(Running.name) |
|
453 |
val hostname = res.string(Running.hostname) |
|
454 |
val numa_node = res.get_int(Running.numa_node) |
|
77475 | 455 |
Build_Job.Abstract(name, Host.Node_Info(hostname, numa_node)) |
77372 | 456 |
}) |
457 |
} |
|
458 |
||
77496 | 459 |
def update_running(db: SQL.Database, running: State.Running): Boolean = { |
77372 | 460 |
val old_running = read_running(db) |
461 |
val abs_running = running.valuesIterator.map(_.make_abstract).toList |
|
462 |
||
463 |
val (delete, insert) = Library.symmetric_difference(old_running, abs_running) |
|
464 |
||
465 |
if (delete.nonEmpty) { |
|
466 |
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
|
467 |
Running.table.delete( |
a86e346b20d8
misc tuning and clarification: more uniform use of optional "sql" in SQL.Table.delete/select;
wenzelm
parents:
77380
diff
changeset
|
468 |
sql = SQL.where(Generic.sql_member(names = delete.map(_.job_name)))))(_.execute()) |
77372 | 469 |
} |
470 |
||
471 |
for (job <- insert) { |
|
472 |
db.using_statement(Running.table.insert()) { stmt => |
|
473 |
stmt.string(1) = job.job_name |
|
474 |
stmt.string(2) = job.node_info.hostname |
|
475 |
stmt.int(3) = job.node_info.numa_node |
|
476 |
stmt.execute() |
|
477 |
} |
|
478 |
} |
|
479 |
||
480 |
delete.nonEmpty || insert.nonEmpty |
|
481 |
} |
|
482 |
||
77496 | 483 |
def read_results_domain(db: SQL.Database): Set[String] = |
484 |
db.using_statement(Results.table.select(List(Results.name)))(stmt => |
|
485 |
Set.from(stmt.execute_query().iterator(_.string(Results.name)))) |
|
486 |
||
77372 | 487 |
def read_results(db: SQL.Database, names: List[String] = Nil): Map[String, Build_Job.Result] = |
488 |
db.using_statement( |
|
77496 | 489 |
Results.table.select(sql = if_proper(names, Results.name.where_member(names))) |
490 |
) { stmt => |
|
491 |
Map.from(stmt.execute_query().iterator { res => |
|
77372 | 492 |
val name = res.string(Results.name) |
493 |
val hostname = res.string(Results.hostname) |
|
494 |
val numa_node = res.get_int(Results.numa_node) |
|
495 |
val rc = res.int(Results.rc) |
|
496 |
val out = res.string(Results.out) |
|
497 |
val err = res.string(Results.err) |
|
77495 | 498 |
val timing = |
499 |
res.timing( |
|
500 |
Results.timing_elapsed, |
|
501 |
Results.timing_cpu, |
|
502 |
Results.timing_gc) |
|
77475 | 503 |
val node_info = Host.Node_Info(hostname, numa_node) |
77372 | 504 |
val process_result = |
505 |
Process_Result(rc, |
|
506 |
out_lines = split_lines(out), |
|
507 |
err_lines = split_lines(err), |
|
77495 | 508 |
timing = timing) |
77372 | 509 |
name -> Build_Job.Result(node_info, process_result) |
510 |
}) |
|
77496 | 511 |
} |
77372 | 512 |
|
77496 | 513 |
def update_results(db: SQL.Database, results: State.Results): Boolean = { |
514 |
val old_results = read_results_domain(db) |
|
77385 | 515 |
val insert = results.iterator.filterNot(p => old_results.contains(p._1)).toList |
77372 | 516 |
|
517 |
for ((name, result) <- insert) { |
|
518 |
val node_info = result.node_info |
|
519 |
val process_result = result.process_result |
|
520 |
db.using_statement(Results.table.insert()) { stmt => |
|
521 |
stmt.string(1) = name |
|
522 |
stmt.string(2) = node_info.hostname |
|
523 |
stmt.int(3) = node_info.numa_node |
|
524 |
stmt.int(4) = process_result.rc |
|
525 |
stmt.string(5) = cat_lines(process_result.out_lines) |
|
526 |
stmt.string(6) = cat_lines(process_result.err_lines) |
|
527 |
stmt.long(7) = process_result.timing.elapsed.ms |
|
528 |
stmt.long(8) = process_result.timing.cpu.ms |
|
529 |
stmt.long(9) = process_result.timing.gc.ms |
|
530 |
stmt.execute() |
|
531 |
} |
|
532 |
} |
|
533 |
||
534 |
insert.nonEmpty |
|
535 |
} |
|
536 |
||
77378
f047804f4860
clarified Build_Process.Context: cover all static information;
wenzelm
parents:
77375
diff
changeset
|
537 |
def init_database(db: SQL.Database, build_context: Build_Process.Context): Unit = { |
77372 | 538 |
val tables = |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
539 |
List( |
77417 | 540 |
Base.table, |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
541 |
Serial.table, |
77505 | 542 |
Progress.table, |
77496 | 543 |
Sessions.table, |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
544 |
Pending.table, |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
545 |
Running.table, |
77476 | 546 |
Results.table, |
547 |
Host.Data.Node_Info.table) |
|
77372 | 548 |
|
549 |
for (table <- tables) db.create_table(table) |
|
550 |
||
551 |
val old_pending = Data.read_pending(db) |
|
552 |
if (old_pending.nonEmpty) { |
|
553 |
error("Cannot init build process, because of unfinished " + |
|
554 |
commas_quote(old_pending.map(_.name))) |
|
555 |
} |
|
556 |
||
557 |
for (table <- tables) db.using_statement(table.delete())(_.execute()) |
|
558 |
||
77417 | 559 |
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
|
560 |
stmt.string(1) = build_context.uuid |
77417 | 561 |
stmt.string(2) = Isabelle_System.getenv("ML_PLATFORM") |
562 |
stmt.string(3) = build_context.store.options.make_prefs(Options.init(prefs = "")) |
|
563 |
stmt.execute() |
|
564 |
} |
|
77372 | 565 |
} |
566 |
||
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
567 |
def update_database( |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
568 |
db: SQL.Database, |
77456
4fec9413f14b
identify Build_Process.Context.instance with Sessions.Build_Info (see also ff164add75cd);
wenzelm
parents:
77455
diff
changeset
|
569 |
uuid: String, |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
570 |
hostname: String, |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
571 |
state: State |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
572 |
): State = { |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
573 |
val changed = |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
574 |
List( |
77496 | 575 |
update_sessions(db, state.sessions), |
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
576 |
update_pending(db, state.pending), |
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
577 |
update_running(db, state.running), |
77476 | 578 |
update_results(db, state.results), |
579 |
Host.Data.update_numa_index(db, hostname, state.numa_index)) |
|
77372 | 580 |
|
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
581 |
val serial0 = get_serial(db) |
77513 | 582 |
val serial = if (changed.exists(identity)) State.inc_serial(serial0) else serial0 |
77372 | 583 |
|
77416
d88c12f22ab0
clarified scope of "serial" and "numa_index" within database;
wenzelm
parents:
77415
diff
changeset
|
584 |
set_serial(db, serial) |
77513 | 585 |
state.set_serial(serial) |
77372 | 586 |
} |
587 |
} |
|
77396 | 588 |
} |
77372 | 589 |
|
590 |
||
77436 | 591 |
|
592 |
/** main process **/ |
|
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
593 |
|
77505 | 594 |
class Build_Process( |
595 |
protected val build_context: Build_Process.Context, |
|
596 |
protected val build_progress: Progress |
|
597 |
) |
|
77436 | 598 |
extends AutoCloseable { |
599 |
/* context */ |
|
600 |
||
77338
0a91c697a18a
tuned signature: avoid warnings in IntelliJ IDEA;
wenzelm
parents:
77337
diff
changeset
|
601 |
protected val store: Sessions.Store = build_context.store |
0a91c697a18a
tuned signature: avoid warnings in IntelliJ IDEA;
wenzelm
parents:
77337
diff
changeset
|
602 |
protected val build_options: Options = store.options |
77453 | 603 |
protected val build_deps: Sessions.Deps = build_context.build_deps |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
604 |
|
77436 | 605 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
606 |
/* global state: internal var vs. external database */ |
77436 | 607 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
608 |
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
|
609 |
|
77514 | 610 |
private val _database: Option[SQL.Database] = build_context.open_database() |
77372 | 611 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
612 |
def close(): Unit = synchronized { _database.foreach(_.close()) } |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
613 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
614 |
private def setup_database(): Unit = |
77438 | 615 |
synchronized { |
616 |
for (db <- _database) { |
|
617 |
db.transaction { Build_Process.Data.init_database(db, build_context) } |
|
618 |
db.rebuild() |
|
77436 | 619 |
} |
620 |
} |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
621 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
622 |
protected def synchronized_database[A](body: => A): A = |
77438 | 623 |
synchronized { |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
624 |
_database match { |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
625 |
case None => body |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
626 |
case Some(db) => db.transaction { body } |
77436 | 627 |
} |
628 |
} |
|
629 |
||
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
630 |
private def sync_database(): Unit = |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
631 |
synchronized_database { |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
632 |
for (db <- _database) { |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
633 |
_state = |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
634 |
Build_Process.Data.update_database( |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
635 |
db, build_context.uuid, build_context.hostname, _state) |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
636 |
} |
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
637 |
} |
77436 | 638 |
|
639 |
||
77505 | 640 |
/* progress backed by database */ |
641 |
||
77522
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
642 |
private def progress_output(message: Progress.Message, body: => Unit): Unit = { |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
643 |
synchronized_database { |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
644 |
val state1 = _state.inc_serial.progress_serial() |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
645 |
for (db <- _database) { |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
646 |
Build_Process.Data.write_progress(db, state1.serial, message, build_context.uuid) |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
647 |
Build_Process.Data.set_serial(db, state1.serial) |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
648 |
} |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
649 |
body |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
650 |
_state = state1 |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
651 |
} |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
652 |
} |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
653 |
|
77505 | 654 |
object progress extends Progress { |
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
655 |
override def verbose: Boolean = build_progress.verbose |
77505 | 656 |
|
77509
3bc49507bae5
clarified treatment of "verbose" messages, e.g. Progress.theory();
wenzelm
parents:
77505
diff
changeset
|
657 |
override def output(message: Progress.Message): Unit = |
77522
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
658 |
progress_output(message, if (do_output(message)) build_progress.output(message)) |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
659 |
|
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
660 |
override def theory(theory: Progress.Theory): Unit = |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
661 |
progress_output(theory.message, build_progress.theory(theory)) |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
662 |
|
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
663 |
override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = |
a1d30297cd61
more complete coverage of non-final Progress methods, notably for Server.Connection_Progress;
wenzelm
parents:
77521
diff
changeset
|
664 |
build_progress.nodes_status(nodes_status) |
77505 | 665 |
|
666 |
override def stop(): Unit = build_progress.stop() |
|
667 |
override def stopped: Boolean = build_progress.stopped |
|
668 |
} |
|
669 |
||
77511 | 670 |
val log: Logger = Logger.make_system_log(progress, build_options) |
77505 | 671 |
|
672 |
||
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
673 |
/* policy operations */ |
77333 | 674 |
|
77415
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
675 |
protected def init_state(state: Build_Process.State): Build_Process.State = { |
77496 | 676 |
val sessions1 = |
677 |
build_context.sessions.foldLeft(state.sessions) { case (map, (name, session)) => |
|
678 |
if (state.sessions.isDefinedAt(name)) map |
|
679 |
else map + (name -> session) |
|
680 |
} |
|
681 |
||
77415
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
682 |
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
|
683 |
val new_pending = |
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
684 |
List.from( |
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
685 |
for { |
77449 | 686 |
(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
|
687 |
if !old_pending(name) |
77449 | 688 |
} yield Build_Process.Entry(name, session_context.deps)) |
77496 | 689 |
val pending1 = new_pending ::: state.pending |
690 |
||
691 |
state.copy(sessions = sessions1, pending = pending1) |
|
77415
6b928419f109
clarified signature: allow more general init, e.g. from existing database;
wenzelm
parents:
77414
diff
changeset
|
692 |
} |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
693 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
694 |
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
|
695 |
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
|
696 |
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
|
697 |
.sortBy(_.name)(build_context.ordering) |
f8aa1647d156
more elementary data structures, to fit better to SQL database;
wenzelm
parents:
77312
diff
changeset
|
698 |
.headOption.map(_.name) |
77296
eeaa2872320b
clarified signature: more explicit synchronized operations;
wenzelm
parents:
77295
diff
changeset
|
699 |
} |
eeaa2872320b
clarified signature: more explicit synchronized operations;
wenzelm
parents:
77295
diff
changeset
|
700 |
else None |
77259
61fc2afe4c8b
clarified signature: prefer stateful object-oriented style, to make it fit better into physical world;
wenzelm
parents:
77258
diff
changeset
|
701 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
702 |
protected def start_session(state: Build_Process.State, session_name: String): Build_Process.State = { |
77468 | 703 |
val ancestor_results = |
704 |
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
|
705 |
|
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
706 |
val input_shasum = |
77260 | 707 |
if (ancestor_results.isEmpty) { |
708 |
SHA1.shasum_meta_info(SHA1.digest(Path.explode("$POLYML_EXE"))) |
|
709 |
} |
|
77460
ccca589d7027
tuned signature: support general Build_Job instances;
wenzelm
parents:
77459
diff
changeset
|
710 |
else SHA1.flat_shasum(ancestor_results.map(_.output_shasum)) |
77257 | 711 |
|
77463 | 712 |
val store_heap = build_context.store_heap(session_name) |
77469 | 713 |
|
714 |
val (current, output_shasum) = |
|
715 |
store.check_output(session_name, |
|
716 |
sources_shasum = build_context.sources_shasum(session_name), |
|
717 |
input_shasum = input_shasum, |
|
718 |
fresh_build = build_context.fresh_build, |
|
719 |
store_heap = store_heap) |
|
720 |
||
77260 | 721 |
val all_current = current && ancestor_results.forall(_.current) |
77257 | 722 |
|
77260 | 723 |
if (all_current) { |
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
724 |
state |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
725 |
.remove_pending(session_name) |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
726 |
.make_result(session_name, Process_Result.ok, output_shasum, current = true) |
77260 | 727 |
} |
77315
f34559b24277
clarified signature: move all parameters into Build_Process.Context;
wenzelm
parents:
77314
diff
changeset
|
728 |
else if (build_context.no_build) { |
77521
5642de4d225d
clarified signature: manage "verbose" flag via "progress";
wenzelm
parents:
77514
diff
changeset
|
729 |
progress.echo("Skipping " + session_name + " ...", verbose = true) |
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
730 |
state. |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
731 |
remove_pending(session_name). |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
732 |
make_result(session_name, Process_Result.error, output_shasum) |
77260 | 733 |
} |
77452 | 734 |
else if (!ancestor_results.forall(_.ok) || progress.stopped) { |
735 |
progress.echo(session_name + " CANCELLED") |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
736 |
state |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
737 |
.remove_pending(session_name) |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
738 |
.make_result(session_name, Process_Result.undefined, output_shasum) |
77452 | 739 |
} |
740 |
else { |
|
77463 | 741 |
progress.echo((if (store_heap) "Building " else "Running ") + session_name + " ...") |
77260 | 742 |
|
77472 | 743 |
store.init_output(session_name) |
77257 | 744 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
745 |
val (numa_node, state1) = state.numa_next(build_context.numa_nodes) |
77475 | 746 |
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
|
747 |
val job = |
77505 | 748 |
Build_Job.start_session(build_context, progress, log, |
749 |
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
|
750 |
state1.add_running(session_name, job) |
77260 | 751 |
} |
752 |
} |
|
77257 | 753 |
|
77436 | 754 |
|
755 |
/* run */ |
|
77372 | 756 |
|
77310 | 757 |
def run(): Map[String, Process_Result] = { |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
758 |
def finished(): Boolean = synchronized_database { _state.finished } |
77400
f3e5b3fe230e
clarified signature: more explicit "synchronized" regions;
wenzelm
parents:
77398
diff
changeset
|
759 |
|
77437
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
760 |
def sleep(): Unit = |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
761 |
Isabelle_Thread.interrupt_handler(_ => progress.stop()) { |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
762 |
build_options.seconds("editor_input_delay").sleep() |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
763 |
} |
dcbf96acae27
clarified signature: do not expose global state to object-oriented variants;
wenzelm
parents:
77436
diff
changeset
|
764 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
765 |
def start(): Boolean = synchronized_database { |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
766 |
next_job(_state) match { |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
767 |
case Some(name) => |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
768 |
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
|
769 |
_state = start_session(_state, name) |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
770 |
true |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
771 |
} |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
772 |
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
|
773 |
case None => false |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
774 |
} |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
775 |
} |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
776 |
|
77335 | 777 |
if (finished()) { |
778 |
progress.echo_warning("Nothing to build") |
|
779 |
Map.empty[String, Process_Result] |
|
780 |
} |
|
781 |
else { |
|
77372 | 782 |
setup_database() |
77335 | 783 |
while (!finished()) { |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
784 |
if (progress.stopped) synchronized_database { _state.stop_running() } |
77310 | 785 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
786 |
for (job <- synchronized_database { _state.finished_running() }) { |
77398
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
787 |
val job_name = job.job_name |
77486
032c76e04475
clarified execution context: main work happens within Future.thread;
wenzelm
parents:
77477
diff
changeset
|
788 |
val (process_result, output_shasum) = job.join |
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
789 |
synchronized_database { |
77396 | 790 |
_state = _state. |
77398
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
791 |
remove_pending(job_name). |
19e9cafaafc5
clarified signature: works for general Build_Job;
wenzelm
parents:
77396
diff
changeset
|
792 |
remove_running(job_name). |
77461 | 793 |
make_result(job_name, process_result, output_shasum, node_info = job.node_info) |
77396 | 794 |
} |
795 |
} |
|
77260 | 796 |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
797 |
if (!start()) { |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
798 |
sync_database() |
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
799 |
sleep() |
77310 | 800 |
} |
801 |
} |
|
77467
e27bc7957297
more robust: proper synchronization of transition from next_job to start_session;
wenzelm
parents:
77466
diff
changeset
|
802 |
|
77466
94dcf2c3895a
more thorough synchronized_database for internal *and* external state;
wenzelm
parents:
77465
diff
changeset
|
803 |
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
|
804 |
for ((name, result) <- _state.results) yield name -> result.process_result |
77257 | 805 |
} |
806 |
} |
|
807 |
} |
|
77238 | 808 |
} |