author | wenzelm |
Mon, 07 May 2018 17:20:39 +0200 | |
changeset 68102 | 813b5d0904c6 |
parent 68101 | 0699a0bacc50 |
child 68103 | c5764b8b2a87 |
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( |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
37 |
session_name: String, theory_name: String, name: String, compressed: Boolean, body: Bytes) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
38 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
39 |
override def toString: String = theory_name + ":" + name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
40 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
41 |
def message(msg: String): String = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
42 |
msg + " " + quote(name) + " for theory " + quote(theory_name) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
43 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
44 |
lazy val compressed_body: Bytes = if (compressed) body else body.compress() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
45 |
lazy val uncompressed_body: Bytes = if (compressed) body.uncompress() else body |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
46 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
47 |
def write(db: SQL.Database) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
48 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
49 |
db.using_statement(Data.table.insert())(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
50 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
51 |
stmt.string(1) = session_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
52 |
stmt.string(2) = theory_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
53 |
stmt.string(3) = name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
54 |
stmt.bool(4) = compressed |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
55 |
stmt.bytes(5) = body |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
56 |
stmt.execute() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
57 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
58 |
} |
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 |
|
68101 | 61 |
def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes): Entry = |
62 |
{ |
|
63 |
val bytes = if (args.compress) body.compress() else body |
|
64 |
Entry(session_name, args.theory_name, args.name, args.compress, bytes) |
|
65 |
} |
|
66 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
67 |
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
|
68 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
69 |
val select = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
70 |
Data.table.select(List(Data.compressed, Data.body), |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
71 |
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
|
72 |
db.using_statement(select)(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
73 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
74 |
val res = stmt.execute_query() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
75 |
if (res.next()) { |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
76 |
val compressed = res.bool(Data.compressed) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
77 |
val body = res.bytes(Data.body) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
78 |
Entry(session_name, theory_name, name, compressed, body) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
79 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
80 |
else error(Entry(session_name, theory_name, name, false, Bytes.empty).message("Bad export")) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
81 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
82 |
} |
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 |
/* database consumer thread */ |
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 |
def consumer(db: SQL.Database): Consumer = new Consumer(db) |
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 |
class Consumer private[Export](db: SQL.Database) |
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 |
db.create_table(Data.table) |
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 |
private val export_errors = Synchronized[List[String]](Nil) |
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 consumer = |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
96 |
Consumer_Thread.fork(name = "export")(consume = (future: Future[Entry]) => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
97 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
98 |
val entry = future.join |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
99 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
100 |
db.transaction { |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
101 |
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
|
102 |
export_errors.change(errs => entry.message("Duplicate export") :: errs) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
103 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
104 |
else entry.write(db) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
105 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
106 |
true |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
107 |
}) |
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 |
def apply(session_name: String, args: Markup.Export.Args, body: Bytes) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
110 |
{ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
111 |
consumer.send( |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
112 |
if (args.compress) |
68101 | 113 |
Future.fork(make_entry(session_name, args, body)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
114 |
else |
68101 | 115 |
Future.value(make_entry(session_name, args, body))) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
116 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
117 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
118 |
def shutdown(close: Boolean = false): List[String] = |
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 |
consumer.shutdown() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
121 |
if (close) db.close() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
122 |
export_errors.value.reverse |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
123 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
124 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
125 |
} |