author | wenzelm |
Mon, 19 Feb 2024 11:39:15 +0100 | |
changeset 79677 | 49370f0f7911 |
parent 79676 | 0cac7e3634d0 |
child 79682 | 1fa1b32b0379 |
permissions | -rw-r--r-- |
79502 | 1 |
/* Title: Pure/Build/store.scala |
78178 | 2 |
Author: Makarius |
3 |
||
4 |
Persistent store for session content: within file-system and/or SQL database. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import java.sql.SQLException |
|
11 |
||
12 |
||
13 |
object Store { |
|
79676
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
14 |
def apply( |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
15 |
options: Options, |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
16 |
build_cluster: Boolean = false, |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
17 |
cache: Term.Cache = Term.Cache.make() |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
18 |
): Store = new Store(options, build_cluster, cache) |
78178 | 19 |
|
20 |
||
79662 | 21 |
/* session */ |
22 |
||
79674 | 23 |
final class Session private[Store]( |
24 |
val name: String, |
|
25 |
val heap: Option[Path], |
|
26 |
val log_db: Option[Path], |
|
27 |
dirs: List[Path] |
|
28 |
) { |
|
79662 | 29 |
def defined: Boolean = heap.isDefined || log_db.isDefined |
30 |
||
79674 | 31 |
def the_heap: Path = |
32 |
heap getOrElse |
|
33 |
error("Missing heap image for session " + quote(name) + " -- expected in:\n" + |
|
34 |
cat_lines(dirs.map(dir => " " + File.standard_path(dir)))) |
|
35 |
||
79663
4a299bdb5d61
clarified signature: more comprehensive operations;
wenzelm
parents:
79662
diff
changeset
|
36 |
def heap_digest(): Option[SHA1.Digest] = |
4a299bdb5d61
clarified signature: more comprehensive operations;
wenzelm
parents:
79662
diff
changeset
|
37 |
heap.flatMap(ML_Heap.read_file_digest) |
4a299bdb5d61
clarified signature: more comprehensive operations;
wenzelm
parents:
79662
diff
changeset
|
38 |
|
79662 | 39 |
override def toString: String = name |
40 |
} |
|
41 |
||
42 |
||
43 |
||
78179 | 44 |
/* session build info */ |
45 |
||
46 |
sealed case class Build_Info( |
|
47 |
sources: SHA1.Shasum, |
|
48 |
input_heaps: SHA1.Shasum, |
|
49 |
output_heap: SHA1.Shasum, |
|
50 |
return_code: Int, |
|
51 |
uuid: String |
|
52 |
) { |
|
53 |
def ok: Boolean = return_code == 0 |
|
54 |
} |
|
55 |
||
56 |
||
57 |
/* session sources */ |
|
78178 | 58 |
|
59 |
sealed case class Source_File( |
|
60 |
name: String, |
|
61 |
digest: SHA1.Digest, |
|
62 |
compressed: Boolean, |
|
63 |
body: Bytes, |
|
64 |
cache: Compress.Cache |
|
65 |
) { |
|
66 |
override def toString: String = name |
|
67 |
||
68 |
def bytes: Bytes = if (compressed) body.uncompress(cache = cache) else body |
|
69 |
} |
|
70 |
||
71 |
object Sources { |
|
72 |
def load(session_base: Sessions.Base, cache: Compress.Cache = Compress.Cache.none): Sources = |
|
73 |
new Sources( |
|
74 |
session_base.session_sources.foldLeft(Map.empty) { |
|
75 |
case (sources, (path, digest)) => |
|
76 |
def err(): Nothing = error("Incoherent digest for source file: " + path) |
|
77 |
val name = File.symbolic_path(path) |
|
78 |
sources.get(name) match { |
|
79 |
case Some(source_file) => |
|
80 |
if (source_file.digest == digest) sources else err() |
|
81 |
case None => |
|
82 |
val bytes = Bytes.read(path) |
|
83 |
if (bytes.sha1_digest == digest) { |
|
84 |
val (compressed, body) = |
|
85 |
bytes.maybe_compress(Compress.Options_Zstd(), cache = cache) |
|
86 |
val file = Source_File(name, digest, compressed, body, cache) |
|
87 |
sources + (name -> file) |
|
88 |
} |
|
89 |
else err() |
|
90 |
} |
|
91 |
}) |
|
92 |
} |
|
93 |
||
94 |
class Sources private(rep: Map[String, Source_File]) extends Iterable[Source_File] { |
|
95 |
override def toString: String = rep.values.toList.sortBy(_.name).mkString("Sources(", ", ", ")") |
|
96 |
override def iterator: Iterator[Source_File] = rep.valuesIterator |
|
97 |
||
98 |
def get(name: String): Option[Source_File] = rep.get(name) |
|
99 |
def apply(name: String): Source_File = |
|
100 |
get(name).getOrElse(error("Missing session sources entry " + quote(name))) |
|
101 |
} |
|
102 |
||
103 |
||
78179 | 104 |
/* SQL data model */ |
78178 | 105 |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
106 |
object private_data extends SQL.Data() { |
78260
0a7f7abbe4f0
more robust transaction_lock: avoid overlapping data spaces;
wenzelm
parents:
78227
diff
changeset
|
107 |
override lazy val tables = SQL.Tables(Session_Info.table, Sources.table) |
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
108 |
|
78179 | 109 |
object Session_Info { |
110 |
val session_name = SQL.Column.string("session_name").make_primary_key |
|
111 |
||
112 |
// Build_Log.Session_Info |
|
113 |
val session_timing = SQL.Column.bytes("session_timing") |
|
114 |
val command_timings = SQL.Column.bytes("command_timings") |
|
115 |
val theory_timings = SQL.Column.bytes("theory_timings") |
|
116 |
val ml_statistics = SQL.Column.bytes("ml_statistics") |
|
117 |
val task_statistics = SQL.Column.bytes("task_statistics") |
|
118 |
val errors = SQL.Column.bytes("errors") |
|
119 |
val build_log_columns = |
|
120 |
List(session_name, session_timing, command_timings, theory_timings, |
|
121 |
ml_statistics, task_statistics, errors) |
|
78178 | 122 |
|
78179 | 123 |
// Build_Info |
124 |
val sources = SQL.Column.string("sources") |
|
125 |
val input_heaps = SQL.Column.string("input_heaps") |
|
126 |
val output_heap = SQL.Column.string("output_heap") |
|
127 |
val return_code = SQL.Column.int("return_code") |
|
128 |
val uuid = SQL.Column.string("uuid") |
|
129 |
val build_columns = List(sources, input_heaps, output_heap, return_code, uuid) |
|
130 |
||
131 |
val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) |
|
132 |
} |
|
133 |
||
134 |
object Sources { |
|
135 |
val session_name = SQL.Column.string("session_name").make_primary_key |
|
136 |
val name = SQL.Column.string("name").make_primary_key |
|
137 |
val digest = SQL.Column.string("digest") |
|
138 |
val compressed = SQL.Column.bool("compressed") |
|
139 |
val body = SQL.Column.bytes("body") |
|
78178 | 140 |
|
78179 | 141 |
val table = |
142 |
SQL.Table("isabelle_sources", List(session_name, name, digest, compressed, body)) |
|
143 |
||
144 |
def where_equal(session_name: String, name: String = ""): SQL.Source = |
|
145 |
SQL.where_and( |
|
146 |
Sources.session_name.equal(session_name), |
|
147 |
if_proper(name, Sources.name.equal(name))) |
|
148 |
} |
|
149 |
||
78265 | 150 |
def read_bytes(db: SQL.Database, name: String, column: SQL.Column): Bytes = |
151 |
db.execute_query_statementO[Bytes]( |
|
152 |
Session_Info.table.select(List(column), sql = Session_Info.session_name.where_equal(name)), |
|
153 |
res => res.bytes(column) |
|
154 |
).getOrElse(Bytes.empty) |
|
155 |
||
156 |
def read_properties( |
|
157 |
db: SQL.Database, name: String, column: SQL.Column, cache: Term.Cache |
|
158 |
): List[Properties.T] = Properties.uncompress(read_bytes(db, name, column), cache = cache) |
|
159 |
||
160 |
def read_session_timing(db: SQL.Database, name: String, cache: Term.Cache): Properties.T = |
|
161 |
Properties.decode(read_bytes(db, name, Session_Info.session_timing), cache = cache) |
|
162 |
||
163 |
def read_command_timings(db: SQL.Database, name: String): Bytes = |
|
164 |
read_bytes(db, name, Session_Info.command_timings) |
|
165 |
||
166 |
def read_theory_timings(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] = |
|
167 |
read_properties(db, name, Session_Info.theory_timings, cache) |
|
168 |
||
169 |
def read_ml_statistics(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] = |
|
170 |
read_properties(db, name, Session_Info.ml_statistics, cache) |
|
171 |
||
172 |
def read_task_statistics(db: SQL.Database, name: String, cache: Term.Cache): List[Properties.T] = |
|
173 |
read_properties(db, name, Session_Info.task_statistics, cache) |
|
174 |
||
175 |
def read_errors(db: SQL.Database, name: String, cache: Term.Cache): List[String] = |
|
176 |
Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache) |
|
177 |
||
78377 | 178 |
def read_build(db: SQL.Database, name: String): Option[Store.Build_Info] = |
179 |
db.execute_query_statementO[Store.Build_Info]( |
|
180 |
Session_Info.table.select(sql = Session_Info.session_name.where_equal(name)), |
|
181 |
{ res => |
|
182 |
val uuid = |
|
183 |
try { Option(res.string(Session_Info.uuid)).getOrElse("") } |
|
184 |
catch { case _: SQLException => "" } |
|
185 |
Store.Build_Info( |
|
186 |
SHA1.fake_shasum(res.string(Session_Info.sources)), |
|
187 |
SHA1.fake_shasum(res.string(Session_Info.input_heaps)), |
|
188 |
SHA1.fake_shasum(res.string(Session_Info.output_heap)), |
|
189 |
res.int(Session_Info.return_code), |
|
190 |
uuid) |
|
191 |
}) |
|
78265 | 192 |
|
78181 | 193 |
def write_session_info( |
194 |
db: SQL.Database, |
|
195 |
cache: Compress.Cache, |
|
196 |
session_name: String, |
|
197 |
build_log: Build_Log.Session_Info, |
|
198 |
build: Build_Info |
|
199 |
): Unit = { |
|
78262 | 200 |
db.execute_statement(Session_Info.table.insert(), body = |
78181 | 201 |
{ stmt => |
202 |
stmt.string(1) = session_name |
|
203 |
stmt.bytes(2) = Properties.encode(build_log.session_timing) |
|
204 |
stmt.bytes(3) = Properties.compress(build_log.command_timings, cache = cache) |
|
205 |
stmt.bytes(4) = Properties.compress(build_log.theory_timings, cache = cache) |
|
206 |
stmt.bytes(5) = Properties.compress(build_log.ml_statistics, cache = cache) |
|
207 |
stmt.bytes(6) = Properties.compress(build_log.task_statistics, cache = cache) |
|
208 |
stmt.bytes(7) = Build_Log.compress_errors(build_log.errors, cache = cache) |
|
209 |
stmt.string(8) = build.sources.toString |
|
210 |
stmt.string(9) = build.input_heaps.toString |
|
211 |
stmt.string(10) = build.output_heap.toString |
|
212 |
stmt.int(11) = build.return_code |
|
213 |
stmt.string(12) = build.uuid |
|
214 |
}) |
|
215 |
} |
|
216 |
||
78555 | 217 |
def write_sources( |
218 |
db: SQL.Database, |
|
219 |
session_name: String, |
|
220 |
source_files: Iterable[Source_File] |
|
221 |
): Unit = { |
|
222 |
db.execute_batch_statement(Sources.table.insert(), batch = |
|
223 |
for (source_file <- source_files) yield { (stmt: SQL.Statement) => |
|
224 |
stmt.string(1) = session_name |
|
225 |
stmt.string(2) = source_file.name |
|
226 |
stmt.string(3) = source_file.digest.toString |
|
227 |
stmt.bool(4) = source_file.compressed |
|
228 |
stmt.bytes(5) = source_file.body |
|
229 |
}) |
|
230 |
} |
|
78178 | 231 |
|
78179 | 232 |
def read_sources( |
233 |
db: SQL.Database, |
|
234 |
session_name: String, |
|
78265 | 235 |
name: String, |
236 |
cache: Compress.Cache |
|
78179 | 237 |
): List[Source_File] = { |
238 |
db.execute_query_statement( |
|
239 |
Sources.table.select( |
|
240 |
sql = Sources.where_equal(session_name, name = name) + SQL.order_by(List(Sources.name))), |
|
241 |
List.from[Source_File], |
|
242 |
{ res => |
|
243 |
val res_name = res.string(Sources.name) |
|
244 |
val digest = SHA1.fake_digest(res.string(Sources.digest)) |
|
245 |
val compressed = res.bool(Sources.compressed) |
|
246 |
val body = res.bytes(Sources.body) |
|
78180 | 247 |
Source_File(res_name, digest, compressed, body, cache) |
78179 | 248 |
} |
249 |
) |
|
250 |
} |
|
78178 | 251 |
} |
252 |
} |
|
253 |
||
79676
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
254 |
class Store private( |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
255 |
val options: Options, |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
256 |
val build_cluster: Boolean, |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
257 |
val cache: Term.Cache |
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
258 |
) { |
78178 | 259 |
store => |
260 |
||
261 |
override def toString: String = "Store(output_dir = " + output_dir.absolute + ")" |
|
262 |
||
263 |
||
264 |
/* directories */ |
|
265 |
||
266 |
val system_output_dir: Path = Path.explode("$ISABELLE_HEAPS_SYSTEM/$ML_IDENTIFIER") |
|
267 |
val user_output_dir: Path = Path.explode("$ISABELLE_HEAPS/$ML_IDENTIFIER") |
|
268 |
||
269 |
def system_heaps: Boolean = options.bool("system_heaps") |
|
270 |
||
271 |
val output_dir: Path = |
|
272 |
if (system_heaps) system_output_dir else user_output_dir |
|
273 |
||
274 |
val input_dirs: List[Path] = |
|
275 |
if (system_heaps) List(system_output_dir) |
|
276 |
else List(user_output_dir, system_output_dir) |
|
277 |
||
278 |
def presentation_dir: Path = |
|
279 |
if (system_heaps) Path.explode("$ISABELLE_BROWSER_INFO_SYSTEM") |
|
280 |
else Path.explode("$ISABELLE_BROWSER_INFO") |
|
281 |
||
282 |
||
283 |
/* file names */ |
|
284 |
||
285 |
def heap(name: String): Path = Path.basic(name) |
|
286 |
def log(name: String): Path = Path.basic("log") + Path.basic(name) |
|
79661
2a9d8c74eb3c
clarified signature: emphasize physical db files;
wenzelm
parents:
79502
diff
changeset
|
287 |
def log_db(name: String): Path = log(name).db |
78178 | 288 |
def log_gz(name: String): Path = log(name).gz |
289 |
||
290 |
def output_heap(name: String): Path = output_dir + heap(name) |
|
291 |
def output_log(name: String): Path = output_dir + log(name) |
|
79661
2a9d8c74eb3c
clarified signature: emphasize physical db files;
wenzelm
parents:
79502
diff
changeset
|
292 |
def output_log_db(name: String): Path = output_dir + log_db(name) |
78178 | 293 |
def output_log_gz(name: String): Path = output_dir + log_gz(name) |
294 |
||
295 |
||
79662 | 296 |
/* session */ |
297 |
||
79663
4a299bdb5d61
clarified signature: more comprehensive operations;
wenzelm
parents:
79662
diff
changeset
|
298 |
def get_session(name: String): Store.Session = { |
79664 | 299 |
val heap = input_dirs.view.map(_ + store.heap(name)).find(_.is_file) |
300 |
val log_db = input_dirs.view.map(_ + store.log_db(name)).find(_.is_file) |
|
79674 | 301 |
new Store.Session(name, heap, log_db, input_dirs) |
79663
4a299bdb5d61
clarified signature: more comprehensive operations;
wenzelm
parents:
79662
diff
changeset
|
302 |
} |
79662 | 303 |
|
304 |
||
78178 | 305 |
/* heap */ |
306 |
||
78212 | 307 |
def heap_shasum(database_server: Option[SQL.Database], name: String): SHA1.Shasum = { |
78510
8f45302a9ff0
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
wenzelm
parents:
78400
diff
changeset
|
308 |
def get_database: Option[SHA1.Digest] = { |
8f45302a9ff0
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
wenzelm
parents:
78400
diff
changeset
|
309 |
for { |
8f45302a9ff0
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
wenzelm
parents:
78400
diff
changeset
|
310 |
db <- database_server |
79677 | 311 |
digest <- ML_Heap.read_digests(db, List(name)).valuesIterator.nextOption() |
78510
8f45302a9ff0
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
wenzelm
parents:
78400
diff
changeset
|
312 |
} yield digest |
8f45302a9ff0
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
wenzelm
parents:
78400
diff
changeset
|
313 |
} |
8f45302a9ff0
more thorough ML_Heap.restore: include ancestors; prefer simultaneous ML_Heap.get_entries: just one database access for heap hierarchy;
wenzelm
parents:
78400
diff
changeset
|
314 |
|
79663
4a299bdb5d61
clarified signature: more comprehensive operations;
wenzelm
parents:
79662
diff
changeset
|
315 |
get_database orElse get_session(name).heap_digest() match { |
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78190
diff
changeset
|
316 |
case Some(digest) => SHA1.shasum(digest, name) |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78190
diff
changeset
|
317 |
case None => SHA1.no_shasum |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78190
diff
changeset
|
318 |
} |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78190
diff
changeset
|
319 |
} |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78190
diff
changeset
|
320 |
|
78178 | 321 |
|
322 |
/* databases for build process and session content */ |
|
323 |
||
324 |
def build_database_server: Boolean = options.bool("build_database_server") |
|
78511 | 325 |
def build_database: Boolean = options.bool("build_database") |
78178 | 326 |
|
78366 | 327 |
def open_server(): SSH.Server = |
328 |
PostgreSQL.open_server(options, |
|
329 |
host = options.string("build_database_host"), |
|
330 |
port = options.int("build_database_port"), |
|
331 |
ssh_host = options.string("build_database_ssh_host"), |
|
332 |
ssh_port = options.int("build_database_ssh_port"), |
|
333 |
ssh_user = options.string("build_database_ssh_user")) |
|
334 |
||
78347 | 335 |
def open_database_server(server: SSH.Server = SSH.no_server): PostgreSQL.Database = |
336 |
PostgreSQL.open_database_server(options, server = server, |
|
78178 | 337 |
user = options.string("build_database_user"), |
338 |
password = options.string("build_database_password"), |
|
339 |
database = options.string("build_database_name"), |
|
340 |
host = options.string("build_database_host"), |
|
341 |
port = options.int("build_database_port"), |
|
78347 | 342 |
ssh_host = options.string("build_database_ssh_host"), |
343 |
ssh_port = options.int("build_database_ssh_port"), |
|
78863
f627ab8c276c
discontinued pointless option (reverting 63d55ba90a9f): performance tuning works better via SQL.Database.execute_batch_statement;
wenzelm
parents:
78555
diff
changeset
|
344 |
ssh_user = options.string("build_database_ssh_user")) |
78178 | 345 |
|
78372 | 346 |
def maybe_open_database_server(server: SSH.Server = SSH.no_server): Option[SQL.Database] = |
347 |
if (build_database_server) Some(open_database_server(server = server)) else None |
|
78205
a40ae2df39ad
clarified database for heaps: do not depend on build_database_test;
wenzelm
parents:
78198
diff
changeset
|
348 |
|
78372 | 349 |
def open_build_database(path: Path, server: SSH.Server = SSH.no_server): SQL.Database = |
79676
0cac7e3634d0
more explicit build_cluster flag to guard open_build_database server;
wenzelm
parents:
79674
diff
changeset
|
350 |
if (build_database_server || build_cluster) open_database_server(server = server) |
78178 | 351 |
else SQLite.open_database(path, restrict = true) |
352 |
||
78223 | 353 |
def maybe_open_build_database( |
78372 | 354 |
path: Path = Path.explode("$ISABELLE_HOME_USER/build.db"), |
355 |
server: SSH.Server = SSH.no_server |
|
356 |
): Option[SQL.Database] = { |
|
78511 | 357 |
if (build_database) Some(open_build_database(path, server = server)) else None |
78372 | 358 |
} |
78184 | 359 |
|
78178 | 360 |
def try_open_database( |
361 |
name: String, |
|
362 |
output: Boolean = false, |
|
78372 | 363 |
server: SSH.Server = SSH.no_server, |
78367 | 364 |
server_mode: Boolean = build_database_server |
78178 | 365 |
): Option[SQL.Database] = { |
366 |
def check(db: SQL.Database): Option[SQL.Database] = |
|
367 |
if (output || session_info_exists(db)) Some(db) else { db.close(); None } |
|
368 |
||
78372 | 369 |
if (server_mode) check(open_database_server(server = server)) |
79661
2a9d8c74eb3c
clarified signature: emphasize physical db files;
wenzelm
parents:
79502
diff
changeset
|
370 |
else if (output) Some(SQLite.open_database(output_log_db(name))) |
78178 | 371 |
else { |
372 |
(for { |
|
373 |
dir <- input_dirs.view |
|
79661
2a9d8c74eb3c
clarified signature: emphasize physical db files;
wenzelm
parents:
79502
diff
changeset
|
374 |
path = dir + log_db(name) if path.is_file |
78178 | 375 |
db <- check(SQLite.open_database(path)) |
376 |
} yield db).headOption |
|
377 |
} |
|
378 |
} |
|
379 |
||
380 |
def error_database(name: String): Nothing = |
|
381 |
error("Missing build database for session " + quote(name)) |
|
382 |
||
78372 | 383 |
def open_database( |
384 |
name: String, |
|
385 |
output: Boolean = false, |
|
386 |
server: SSH.Server = SSH.no_server |
|
387 |
): SQL.Database = { |
|
388 |
try_open_database(name, output = output, server = server) getOrElse error_database(name) |
|
389 |
} |
|
78178 | 390 |
|
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78212
diff
changeset
|
391 |
def clean_output( |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78212
diff
changeset
|
392 |
database_server: Option[SQL.Database], |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78212
diff
changeset
|
393 |
name: String, |
78217 | 394 |
session_init: Boolean = false |
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78212
diff
changeset
|
395 |
): Option[Boolean] = { |
78178 | 396 |
val relevant_db = |
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78212
diff
changeset
|
397 |
database_server match { |
78217 | 398 |
case Some(db) => |
399 |
ML_Heap.clean_entry(db, name) |
|
400 |
clean_session_info(db, name) |
|
78227
1ba48d402005
proper session_init *after* deleting db files (amending af6c493b0441);
wenzelm
parents:
78223
diff
changeset
|
401 |
case None => false |
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78212
diff
changeset
|
402 |
} |
78178 | 403 |
|
404 |
val del = |
|
405 |
for { |
|
406 |
dir <- |
|
407 |
(if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir)) |
|
79661
2a9d8c74eb3c
clarified signature: emphasize physical db files;
wenzelm
parents:
79502
diff
changeset
|
408 |
file <- List(heap(name), log_db(name), log(name), log_gz(name)) |
78178 | 409 |
path = dir + file if path.is_file |
410 |
} yield path.file.delete |
|
411 |
||
78227
1ba48d402005
proper session_init *after* deleting db files (amending af6c493b0441);
wenzelm
parents:
78223
diff
changeset
|
412 |
if (database_server.isEmpty && session_init) { |
1ba48d402005
proper session_init *after* deleting db files (amending af6c493b0441);
wenzelm
parents:
78223
diff
changeset
|
413 |
using(open_database(name, output = true))(clean_session_info(_, name)) |
1ba48d402005
proper session_init *after* deleting db files (amending af6c493b0441);
wenzelm
parents:
78223
diff
changeset
|
414 |
} |
1ba48d402005
proper session_init *after* deleting db files (amending af6c493b0441);
wenzelm
parents:
78223
diff
changeset
|
415 |
|
78185 | 416 |
if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None |
78178 | 417 |
} |
418 |
||
419 |
def check_output( |
|
78374 | 420 |
database_server: Option[SQL.Database], |
78178 | 421 |
name: String, |
422 |
session_options: Options, |
|
423 |
sources_shasum: SHA1.Shasum, |
|
424 |
input_shasum: SHA1.Shasum, |
|
425 |
fresh_build: Boolean, |
|
426 |
store_heap: Boolean |
|
427 |
): (Boolean, SHA1.Shasum) = { |
|
78374 | 428 |
def no_check: (Boolean, SHA1.Shasum) = (false, SHA1.no_shasum) |
429 |
||
430 |
def check(db: SQL.Database): (Boolean, SHA1.Shasum) = |
|
431 |
read_build(db, name) match { |
|
432 |
case Some(build) => |
|
433 |
val output_shasum = heap_shasum(if (db.is_postgresql) Some(db) else None, name) |
|
434 |
val current = |
|
435 |
!fresh_build && |
|
436 |
build.ok && |
|
437 |
Sessions.eq_sources(session_options, build.sources, sources_shasum) && |
|
438 |
build.input_heaps == input_shasum && |
|
439 |
build.output_heap == output_shasum && |
|
440 |
!(store_heap && output_shasum.is_empty) |
|
441 |
(current, output_shasum) |
|
442 |
case None => no_check |
|
443 |
} |
|
444 |
||
445 |
database_server match { |
|
446 |
case Some(db) => if (session_info_exists(db)) check(db) else no_check |
|
447 |
case None => using_option(try_open_database(name))(check) getOrElse no_check |
|
78178 | 448 |
} |
449 |
} |
|
450 |
||
451 |
||
452 |
/* session info */ |
|
453 |
||
78375
234f2ff9afe6
clarified signature: more specific exists_table --- avoid retrieving full list beforehand;
wenzelm
parents:
78374
diff
changeset
|
454 |
def session_info_exists(db: SQL.Database): Boolean = |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
455 |
Store.private_data.tables.forall(db.exists_table) |
78181 | 456 |
|
457 |
def session_info_defined(db: SQL.Database, name: String): Boolean = |
|
458 |
db.execute_query_statementB( |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
459 |
Store.private_data.Session_Info.table.select(List(Store.private_data.Session_Info.session_name), |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
460 |
sql = Store.private_data.Session_Info.session_name.where_equal(name))) |
78181 | 461 |
|
78260
0a7f7abbe4f0
more robust transaction_lock: avoid overlapping data spaces;
wenzelm
parents:
78227
diff
changeset
|
462 |
def clean_session_info(db: SQL.Database, name: String): Boolean = { |
0a7f7abbe4f0
more robust transaction_lock: avoid overlapping data spaces;
wenzelm
parents:
78227
diff
changeset
|
463 |
Export.clean_session(db, name) |
0a7f7abbe4f0
more robust transaction_lock: avoid overlapping data spaces;
wenzelm
parents:
78227
diff
changeset
|
464 |
Document_Build.clean_session(db, name) |
0a7f7abbe4f0
more robust transaction_lock: avoid overlapping data spaces;
wenzelm
parents:
78227
diff
changeset
|
465 |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
466 |
Store.private_data.transaction_lock(db, create = true, label = "Store.clean_session_info") { |
78178 | 467 |
val already_defined = session_info_defined(db, name) |
468 |
||
469 |
db.execute_statement( |
|
78555 | 470 |
SQL.multi( |
471 |
Store.private_data.Session_Info.table.delete( |
|
472 |
sql = Store.private_data.Session_Info.session_name.where_equal(name)), |
|
473 |
Store.private_data.Sources.table.delete( |
|
474 |
sql = Store.private_data.Sources.where_equal(name)))) |
|
78178 | 475 |
|
476 |
already_defined |
|
477 |
} |
|
78260
0a7f7abbe4f0
more robust transaction_lock: avoid overlapping data spaces;
wenzelm
parents:
78227
diff
changeset
|
478 |
} |
78178 | 479 |
|
480 |
def write_session_info( |
|
481 |
db: SQL.Database, |
|
482 |
session_name: String, |
|
483 |
sources: Store.Sources, |
|
484 |
build_log: Build_Log.Session_Info, |
|
485 |
build: Store.Build_Info |
|
486 |
): Unit = { |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
487 |
Store.private_data.transaction_lock(db, label = "Store.write_session_info") { |
78555 | 488 |
for (source_files <- sources.iterator.toList.grouped(200)) { |
489 |
Store.private_data.write_sources(db, session_name, source_files) |
|
490 |
} |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
491 |
Store.private_data.write_session_info(db, cache.compress, session_name, build_log, build) |
78178 | 492 |
} |
493 |
} |
|
494 |
||
78265 | 495 |
def read_session_timing(db: SQL.Database, session: String): Properties.T = |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
496 |
Store.private_data.transaction_lock(db, label = "Store.read_session_timing") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
497 |
Store.private_data.read_session_timing(db, session, cache) |
78356 | 498 |
} |
78178 | 499 |
|
78265 | 500 |
def read_command_timings(db: SQL.Database, session: String): Bytes = |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
501 |
Store.private_data.transaction_lock(db, label = "Store.read_command_timings") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
502 |
Store.private_data.read_command_timings(db, session) |
78356 | 503 |
} |
78178 | 504 |
|
78265 | 505 |
def read_theory_timings(db: SQL.Database, session: String): List[Properties.T] = |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
506 |
Store.private_data.transaction_lock(db, label = "Store.read_theory_timings") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
507 |
Store.private_data.read_theory_timings(db, session, cache) |
78356 | 508 |
} |
78178 | 509 |
|
78265 | 510 |
def read_ml_statistics(db: SQL.Database, session: String): List[Properties.T] = |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
511 |
Store.private_data.transaction_lock(db, label = "Store.read_ml_statistics") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
512 |
Store.private_data.read_ml_statistics(db, session, cache) |
78356 | 513 |
} |
78178 | 514 |
|
78265 | 515 |
def read_task_statistics(db: SQL.Database, session: String): List[Properties.T] = |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
516 |
Store.private_data.transaction_lock(db, label = "Store.read_task_statistics") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
517 |
Store.private_data.read_task_statistics(db, session, cache) |
78356 | 518 |
} |
78265 | 519 |
|
520 |
def read_theories(db: SQL.Database, session: String): List[String] = |
|
521 |
read_theory_timings(db, session).flatMap(Markup.Name.unapply) |
|
522 |
||
523 |
def read_errors(db: SQL.Database, session: String): List[String] = |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
524 |
Store.private_data.transaction_lock(db, label = "Store.read_errors") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
525 |
Store.private_data.read_errors(db, session, cache) |
78356 | 526 |
} |
78265 | 527 |
|
528 |
def read_build(db: SQL.Database, session: String): Option[Store.Build_Info] = |
|
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
529 |
Store.private_data.transaction_lock(db, label = "Store.read_build") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
530 |
if (session_info_exists(db)) Store.private_data.read_build(db, session) else None |
78356 | 531 |
} |
78178 | 532 |
|
78179 | 533 |
def read_sources(db: SQL.Database, session: String, name: String = ""): List[Store.Source_File] = |
78396
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
534 |
Store.private_data.transaction_lock(db, label = "Store.read_sources") { |
7853d9072d1b
renamed object Data to private_data, to emphasize its intended scope (but it is publicly accessible in the database);
wenzelm
parents:
78377
diff
changeset
|
535 |
Store.private_data.read_sources(db, session, name, cache.compress) |
78356 | 536 |
} |
78178 | 537 |
} |