author | wenzelm |
Mon, 07 May 2018 17:37:03 +0200 | |
changeset 68103 | c5764b8b2a87 |
parent 68102 | 813b5d0904c6 |
child 68104 | 3795f67716e6 |
permissions | -rw-r--r-- |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Thy/export.scala |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
3 |
|
68102 | 4 |
Manage theory exports: compressed blobs. |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
6 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
8 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
9 |
object Export |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
10 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
11 |
/* SQL data model */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
12 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
13 |
object Data |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
14 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
15 |
val session_name = SQL.Column.string("session_name").make_primary_key |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
16 |
val theory_name = SQL.Column.string("theory_name").make_primary_key |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
17 |
val name = SQL.Column.string("name").make_primary_key |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
18 |
val compressed = SQL.Column.bool("compressed") |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
19 |
val body = SQL.Column.bytes("body") |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
20 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
21 |
val table = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
22 |
SQL.Table("isabelle_exports", List(session_name, theory_name, name, compressed, body)) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
23 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
24 |
def where_equal(session_name: String, theory_name: String): SQL.Source = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
25 |
"WHERE " + Data.session_name.equal(session_name) + |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
26 |
" AND " + Data.theory_name.equal(theory_name) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
27 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
28 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
29 |
def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
30 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
31 |
val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name)) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
32 |
db.using_statement(select)(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
33 |
stmt.execute_query().iterator(res => res.string(Data.name)).toList) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
34 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
35 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
36 |
sealed case class Entry( |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
37 |
session_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
38 |
theory_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
39 |
name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
40 |
compressed: Boolean, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
41 |
body: Future[Bytes]) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
42 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
43 |
override def toString: String = theory_name + ":" + name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
44 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
45 |
def message(msg: String): String = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
46 |
msg + " " + quote(name) + " for theory " + quote(theory_name) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
47 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
48 |
def write(db: SQL.Database) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
49 |
{ |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
50 |
val bytes = body.join |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
51 |
db.using_statement(Data.table.insert())(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
52 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
53 |
stmt.string(1) = session_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
54 |
stmt.string(2) = theory_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
55 |
stmt.string(3) = name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
56 |
stmt.bool(4) = compressed |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
57 |
stmt.bytes(5) = bytes |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
58 |
stmt.execute() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
59 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
60 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
61 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
62 |
|
68101 | 63 |
def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry = |
64 |
{ |
|
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
65 |
Entry(session_name, args.theory_name, args.name, args.compress, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
66 |
if (args.compress) Future.fork(body.compress()) else Future.value(body)) |
68101 | 67 |
} |
68 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
69 |
def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
70 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
71 |
val select = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
72 |
Data.table.select(List(Data.compressed, Data.body), |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
73 |
Data.where_equal(session_name, theory_name) + " AND " + Data.name.equal(name)) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
74 |
db.using_statement(select)(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
75 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
76 |
val res = stmt.execute_query() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
77 |
if (res.next()) { |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
78 |
val compressed = res.bool(Data.compressed) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
79 |
val body = res.bytes(Data.body) |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
80 |
Entry(session_name, theory_name, name, compressed, Future.value(body)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
81 |
} |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
82 |
else error(Entry(session_name, theory_name, name, false, Future.value(Bytes.empty)).message("Bad export")) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
83 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
84 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
85 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
86 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
87 |
/* database consumer thread */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
88 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
89 |
def consumer(db: SQL.Database): Consumer = new Consumer(db) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
90 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
91 |
class Consumer private[Export](db: SQL.Database) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
92 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
93 |
db.create_table(Data.table) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
94 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
95 |
private val export_errors = Synchronized[List[String]](Nil) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
96 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
97 |
private val consumer = |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
98 |
Consumer_Thread.fork(name = "export")(consume = (entry: Entry) => |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
99 |
{ |
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
100 |
entry.body.join |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
101 |
db.transaction { |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
102 |
if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) { |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
103 |
export_errors.change(errs => entry.message("Duplicate export") :: errs) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
104 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
105 |
else entry.write(db) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
106 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
107 |
true |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
108 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
109 |
|
68103
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
110 |
def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
111 |
consumer.send(make_entry(session_name, args, body)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
112 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
113 |
def shutdown(close: Boolean = false): List[String] = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
114 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
115 |
consumer.shutdown() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
116 |
if (close) db.close() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
117 |
export_errors.value.reverse |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
118 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
119 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
120 |
} |