author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 74686 | 42f358ea8dee |
child 75394 | 42267c650205 |
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 |
|
68116 | 9 |
|
10 |
import scala.annotation.tailrec |
|
11 |
import scala.util.matching.Regex |
|
12 |
||
13 |
||
75393 | 14 |
object Export { |
72691 | 15 |
/* artefact names */ |
16 |
||
72844 | 17 |
val DOCUMENT_ID = "PIDE/document_id" |
18 |
val FILES = "PIDE/files" |
|
72702 | 19 |
val MARKUP = "PIDE/markup" |
20 |
val MESSAGES = "PIDE/messages" |
|
72691 | 21 |
val DOCUMENT_PREFIX = "document/" |
73785 | 22 |
val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex" |
23 |
val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations" |
|
72691 | 24 |
val THEORY_PREFIX: String = "theory/" |
25 |
val PROOFS_PREFIX: String = "proofs/" |
|
69634 | 26 |
|
69756 | 27 |
def explode_name(s: String): List[String] = space_explode('/', s) |
28 |
def implode_name(elems: Iterable[String]): String = elems.mkString("/") |
|
69634 | 29 |
|
30 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
31 |
/* SQL data model */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
32 |
|
75393 | 33 |
object Data { |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
34 |
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
|
35 |
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
|
36 |
val name = SQL.Column.string("name").make_primary_key |
69788 | 37 |
val executable = SQL.Column.bool("executable") |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
38 |
val compressed = SQL.Column.bool("compressed") |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
39 |
val body = SQL.Column.bytes("body") |
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 |
val table = |
69788 | 42 |
SQL.Table("isabelle_exports", |
43 |
List(session_name, theory_name, name, executable, compressed, body)) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
44 |
|
68116 | 45 |
def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source = |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
46 |
"WHERE " + Data.session_name.equal(session_name) + |
68116 | 47 |
(if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) + |
48 |
(if (name == "") "" else " AND " + Data.name.equal(name)) |
|
49 |
} |
|
50 |
||
75393 | 51 |
def read_name( |
52 |
db: SQL.Database, |
|
53 |
session_name: String, |
|
54 |
theory_name: String, |
|
55 |
name: String |
|
56 |
): Boolean = { |
|
68116 | 57 |
val select = |
58 |
Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name, name)) |
|
59 |
db.using_statement(select)(stmt => stmt.execute_query().next()) |
|
68092
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 |
|
75393 | 62 |
def read_names(db: SQL.Database, session_name: String, theory_name: String): List[String] = { |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
63 |
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
|
64 |
db.using_statement(select)(stmt => |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
65 |
stmt.execute_query().iterator(res => res.string(Data.name)).toList) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
66 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
67 |
|
75393 | 68 |
def read_theory_names(db: SQL.Database, session_name: String): List[String] = { |
68222 | 69 |
val select = |
70 |
Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) |
|
71 |
db.using_statement(select)(stmt => |
|
72 |
stmt.execute_query().iterator(_.string(Data.theory_name)).toList) |
|
73 |
} |
|
74 |
||
75393 | 75 |
def read_theory_exports(db: SQL.Database, session_name: String): List[(String, String)] = { |
68116 | 76 |
val select = Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) |
77 |
db.using_statement(select)(stmt => |
|
78 |
stmt.execute_query().iterator(res => |
|
79 |
(res.string(Data.theory_name), res.string(Data.name))).toList) |
|
68115 | 80 |
} |
81 |
||
68104 | 82 |
def message(msg: String, theory_name: String, name: String): String = |
83 |
msg + " " + quote(name) + " for theory " + quote(theory_name) |
|
84 |
||
73693 | 85 |
def compound_name(a: String, b: String): String = |
86 |
if (a.isEmpty) b else a + ":" + b |
|
68116 | 87 |
|
72854 | 88 |
def empty_entry(theory_name: String, name: String): Entry = |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
89 |
Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none) |
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
90 |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
91 |
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
|
92 |
session_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
93 |
theory_name: String, |
c5764b8b2a87
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;
wenzelm
parents:
68102
diff
changeset
|
94 |
name: String, |
69788 | 95 |
executable: Boolean, |
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
96 |
body: Future[(Boolean, Bytes)], |
75393 | 97 |
cache: XML.Cache |
98 |
) { |
|
69635 | 99 |
override def toString: String = name |
69630 | 100 |
|
71141 | 101 |
def compound_name: String = Export.compound_name(theory_name, name) |
102 |
||
72691 | 103 |
def name_has_prefix(s: String): Boolean = name.startsWith(s) |
69634 | 104 |
val name_elems: List[String] = explode_name(name) |
105 |
||
106 |
def name_extends(elems: List[String]): Boolean = |
|
107 |
name_elems.startsWith(elems) && name_elems != elems |
|
108 |
||
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
109 |
def text: String = uncompressed.text |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
110 |
|
75393 | 111 |
def uncompressed: Bytes = { |
69629 | 112 |
val (compressed, bytes) = body.join |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
113 |
if (compressed) bytes.uncompress(cache = cache.xz) else bytes |
69629 | 114 |
} |
115 |
||
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
116 |
def uncompressed_yxml: XML.Body = |
73033 | 117 |
YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache) |
69629 | 118 |
|
75393 | 119 |
def write(db: SQL.Database): Unit = { |
68167 | 120 |
val (compressed, bytes) = body.join |
75393 | 121 |
db.using_statement(Data.table.insert())(stmt => { |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
122 |
stmt.string(1) = session_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
123 |
stmt.string(2) = theory_name |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
124 |
stmt.string(3) = name |
69788 | 125 |
stmt.bool(4) = executable |
126 |
stmt.bool(5) = compressed |
|
127 |
stmt.bytes(6) = bytes |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
128 |
stmt.execute() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
129 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
130 |
} |
68116 | 131 |
} |
132 |
||
75393 | 133 |
def make_regex(pattern: String): Regex = { |
68116 | 134 |
@tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex = |
135 |
chs match { |
|
136 |
case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest) |
|
137 |
case '*' :: rest => make("[^:/]*" :: result, depth, rest) |
|
138 |
case '?' :: rest => make("[^:/]" :: result, depth, rest) |
|
139 |
case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest) |
|
140 |
case '{' :: rest => make("(" :: result, depth + 1, rest) |
|
141 |
case ',' :: rest if depth > 0 => make("|" :: result, depth, rest) |
|
142 |
case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest) |
|
143 |
case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest) |
|
144 |
case c :: rest => make(c.toString :: result, depth, rest) |
|
145 |
case Nil => result.reverse.mkString.r |
|
146 |
} |
|
147 |
make(Nil, 0, pattern.toList) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
148 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
149 |
|
75393 | 150 |
def make_matcher(pattern: String): (String, String) => Boolean = { |
68151 | 151 |
val regex = make_regex(pattern) |
152 |
(theory_name: String, name: String) => |
|
153 |
regex.pattern.matcher(compound_name(theory_name, name)).matches |
|
154 |
} |
|
155 |
||
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
156 |
def make_entry( |
75393 | 157 |
session_name: String, |
158 |
args: Protocol.Export.Args, |
|
159 |
bytes: Bytes, |
|
160 |
cache: XML.Cache |
|
161 |
): Entry = { |
|
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
162 |
val body = |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
163 |
if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz)) |
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
164 |
else Future.value((false, bytes)) |
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
165 |
Entry(session_name, args.theory_name, args.name, args.executable, body, cache) |
68101 | 166 |
} |
167 |
||
75393 | 168 |
def read_entry( |
169 |
db: SQL.Database, |
|
170 |
cache: XML.Cache, |
|
171 |
session_name: String, |
|
172 |
theory_name: String, |
|
173 |
name: String |
|
174 |
): Option[Entry] = { |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
175 |
val select = |
69788 | 176 |
Data.table.select(List(Data.executable, Data.compressed, Data.body), |
68116 | 177 |
Data.where_equal(session_name, theory_name, name)) |
75393 | 178 |
db.using_statement(select)(stmt => { |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
179 |
val res = stmt.execute_query() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
180 |
if (res.next()) { |
69788 | 181 |
val executable = res.bool(Data.executable) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
182 |
val compressed = res.bool(Data.compressed) |
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
183 |
val bytes = res.bytes(Data.body) |
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
184 |
val body = Future.value(compressed, bytes) |
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
185 |
Some(Entry(session_name, theory_name, name, executable, body, cache)) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
186 |
} |
68202 | 187 |
else None |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
188 |
}) |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
189 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
190 |
|
75393 | 191 |
def read_entry( |
192 |
dir: Path, |
|
193 |
cache: XML.Cache, |
|
194 |
session_name: String, |
|
195 |
theory_name: String, |
|
196 |
name: String |
|
197 |
): Option[Entry] = { |
|
68831 | 198 |
val path = dir + Path.basic(theory_name) + Path.explode(name) |
199 |
if (path.is_file) { |
|
69788 | 200 |
val executable = File.is_executable(path) |
68831 | 201 |
val uncompressed = Bytes.read(path) |
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
202 |
val body = Future.value((false, uncompressed)) |
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
203 |
Some(Entry(session_name, theory_name, name, executable, body, cache)) |
68831 | 204 |
} |
205 |
else None |
|
206 |
} |
|
207 |
||
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
208 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
209 |
/* database consumer thread */ |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
210 |
|
74255 | 211 |
def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer = |
212 |
new Consumer(db, cache, progress) |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
213 |
|
75393 | 214 |
class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress) { |
68924 | 215 |
private val errors = Synchronized[List[String]](Nil) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
216 |
|
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
217 |
private val consumer = |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
218 |
Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")( |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
219 |
bulk = { case (entry, _) => entry.body.is_finished }, |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
220 |
consume = |
75393 | 221 |
(args: List[(Entry, Boolean)]) => { |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
222 |
val results = |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
223 |
db.transaction { |
74256 | 224 |
for ((entry, strict) <- args) |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
225 |
yield { |
74257 | 226 |
if (progress.stopped) { |
227 |
entry.body.cancel() |
|
228 |
Exn.Res(()) |
|
229 |
} |
|
74256 | 230 |
else if (read_name(db, entry.session_name, entry.theory_name, entry.name)) { |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
231 |
if (strict) { |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
232 |
val msg = message("Duplicate export", entry.theory_name, entry.name) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
233 |
errors.change(msg :: _) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
234 |
} |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
235 |
Exn.Res(()) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
236 |
} |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
237 |
else Exn.capture { entry.write(db) } |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
238 |
} |
70499 | 239 |
} |
71145
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
240 |
(results, true) |
2f782d5f5d5a
improved performance of session exports via bulk transactions;
wenzelm
parents:
71141
diff
changeset
|
241 |
}) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
242 |
|
75393 | 243 |
def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = { |
74257 | 244 |
if (!progress.stopped) { |
245 |
consumer.send(make_entry(session_name, args, body, cache) -> args.strict) |
|
246 |
} |
|
247 |
} |
|
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
248 |
|
75393 | 249 |
def shutdown(close: Boolean = false): List[String] = { |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
250 |
consumer.shutdown() |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
251 |
if (close) db.close() |
74255 | 252 |
errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
253 |
} |
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
254 |
} |
68116 | 255 |
|
256 |
||
68418 | 257 |
/* abstract provider */ |
258 |
||
75393 | 259 |
object Provider { |
71014 | 260 |
def none: Provider = |
261 |
new Provider { |
|
262 |
def apply(export_name: String): Option[Entry] = None |
|
263 |
def focus(other_theory: String): Provider = this |
|
264 |
||
265 |
override def toString: String = "none" |
|
266 |
} |
|
267 |
||
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
268 |
def database_context( |
72854 | 269 |
context: Sessions.Database_Context, |
74686 | 270 |
session_hierarchy: List[String], |
72854 | 271 |
theory_name: String): Provider = |
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
272 |
new Provider { |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
273 |
def apply(export_name: String): Option[Entry] = |
74686 | 274 |
context.read_export(session_hierarchy, theory_name, export_name) |
72634
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
275 |
|
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
276 |
def focus(other_theory: String): Provider = this |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
277 |
|
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
278 |
override def toString: String = context.toString |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
279 |
} |
5cea0993ee4f
clarified access to single database server vs. collection of database files;
wenzelm
parents:
72375
diff
changeset
|
280 |
|
75393 | 281 |
def database( |
282 |
db: SQL.Database, |
|
283 |
cache: XML.Cache, |
|
284 |
session_name: String, |
|
285 |
theory_name: String |
|
286 |
) : Provider = { |
|
68418 | 287 |
new Provider { |
288 |
def apply(export_name: String): Option[Entry] = |
|
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
289 |
read_entry(db, cache, session_name, theory_name, export_name) |
68832 | 290 |
|
70539
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
291 |
def focus(other_theory: String): Provider = |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
292 |
if (other_theory == theory_name) this |
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
293 |
else Provider.database(db, cache, session_name, other_theory) |
70539
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
294 |
|
68832 | 295 |
override def toString: String = db.toString |
68418 | 296 |
} |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
297 |
} |
68418 | 298 |
|
299 |
def snapshot(snapshot: Document.Snapshot): Provider = |
|
300 |
new Provider { |
|
301 |
def apply(export_name: String): Option[Entry] = |
|
302 |
snapshot.exports_map.get(export_name) |
|
68832 | 303 |
|
70539
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
304 |
def focus(other_theory: String): Provider = |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
305 |
if (other_theory == snapshot.node_name.theory) this |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
306 |
else { |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
307 |
val node_name = |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
308 |
snapshot.version.nodes.theory_name(other_theory) getOrElse |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
309 |
error("Bad theory " + quote(other_theory)) |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
310 |
Provider.snapshot(snapshot.state.snapshot(node_name)) |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
311 |
} |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
312 |
|
68832 | 313 |
override def toString: String = snapshot.toString |
68418 | 314 |
} |
68831 | 315 |
|
75393 | 316 |
def directory( |
317 |
dir: Path, |
|
318 |
cache: XML.Cache, |
|
319 |
session_name: String, |
|
320 |
theory_name: String |
|
321 |
) : Provider = { |
|
68831 | 322 |
new Provider { |
323 |
def apply(export_name: String): Option[Entry] = |
|
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
324 |
read_entry(dir, cache, session_name, theory_name, export_name) |
68832 | 325 |
|
70539
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
326 |
def focus(other_theory: String): Provider = |
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
327 |
if (other_theory == theory_name) this |
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
328 |
else Provider.directory(dir, cache, session_name, other_theory) |
70539
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
329 |
|
68832 | 330 |
override def toString: String = dir.toString |
68831 | 331 |
} |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
332 |
} |
68418 | 333 |
} |
334 |
||
75393 | 335 |
trait Provider { |
68418 | 336 |
def apply(export_name: String): Option[Entry] |
337 |
||
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
338 |
def uncompressed_yxml(export_name: String): XML.Body = |
68418 | 339 |
apply(export_name) match { |
72847
9dda93a753b1
clarified signature: provide XZ.Cache where Export.Entry is created;
wenzelm
parents:
72844
diff
changeset
|
340 |
case Some(entry) => entry.uncompressed_yxml |
68418 | 341 |
case None => Nil |
342 |
} |
|
70539
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
343 |
|
30b3c58a1933
support Export_Theory.read_proof, based on theory_name and serial;
wenzelm
parents:
70499
diff
changeset
|
344 |
def focus(other_theory: String): Provider |
68418 | 345 |
} |
346 |
||
347 |
||
68288 | 348 |
/* export to file-system */ |
349 |
||
350 |
def export_files( |
|
351 |
store: Sessions.Store, |
|
352 |
session_name: String, |
|
353 |
export_dir: Path, |
|
71726
a5fda30edae2
clarified signature: more uniform treatment of stopped/interrupted state;
wenzelm
parents:
71624
diff
changeset
|
354 |
progress: Progress = new Progress, |
69671 | 355 |
export_prune: Int = 0, |
68288 | 356 |
export_list: Boolean = false, |
75393 | 357 |
export_patterns: List[String] = Nil |
358 |
): Unit = { |
|
359 |
using(store.open_database(session_name))(db => { |
|
68288 | 360 |
db.transaction { |
361 |
val export_names = read_theory_exports(db, session_name) |
|
362 |
||
363 |
// list |
|
364 |
if (export_list) { |
|
365 |
(for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)). |
|
71601 | 366 |
sorted.foreach(progress.echo) |
68288 | 367 |
} |
368 |
||
369 |
// export |
|
68290 | 370 |
if (export_patterns.nonEmpty) { |
371 |
val exports = |
|
372 |
(for { |
|
373 |
export_pattern <- export_patterns.iterator |
|
374 |
matcher = make_matcher(export_pattern) |
|
375 |
(theory_name, name) <- export_names if matcher(theory_name, name) |
|
376 |
} yield (theory_name, name)).toSet |
|
68288 | 377 |
for { |
68290 | 378 |
(theory_name, group) <- exports.toList.groupBy(_._1).toList.sortBy(_._1) |
379 |
name <- group.map(_._2).sorted |
|
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
73024
diff
changeset
|
380 |
entry <- read_entry(db, store.cache, session_name, theory_name, name) |
68288 | 381 |
} { |
69671 | 382 |
val elems = theory_name :: space_explode('/', name) |
383 |
val path = |
|
384 |
if (elems.length < export_prune + 1) { |
|
385 |
error("Cannot prune path by " + export_prune + " element(s): " + Path.make(elems)) |
|
386 |
} |
|
387 |
else export_dir + Path.make(elems.drop(export_prune)) |
|
388 |
||
69811
18f61ce86425
clarified 'export_files' in session ROOT: require explicit "isabelle build -e";
wenzelm
parents:
69789
diff
changeset
|
389 |
progress.echo("export " + path + (if (entry.executable) " (executable)" else "")) |
72375 | 390 |
Isabelle_System.make_directory(path.dir) |
74215
7515abfe18cf
avoid change of existing file, notably rebuild via ghc_stack;
wenzelm
parents:
73785
diff
changeset
|
391 |
val bytes = entry.uncompressed |
7515abfe18cf
avoid change of existing file, notably rebuild via ghc_stack;
wenzelm
parents:
73785
diff
changeset
|
392 |
if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes) |
69789
2c3e5e58d93f
more thorough File.set_executable, notably for Windows;
wenzelm
parents:
69788
diff
changeset
|
393 |
File.set_executable(path, entry.executable) |
68288 | 394 |
} |
395 |
} |
|
396 |
} |
|
397 |
}) |
|
398 |
} |
|
399 |
||
400 |
||
68116 | 401 |
/* Isabelle tool wrapper */ |
402 |
||
71601 | 403 |
val default_export_dir: Path = Path.explode("export") |
68116 | 404 |
|
72763 | 405 |
val isabelle_tool = Isabelle_Tool("export", "retrieve theory exports", |
75393 | 406 |
Scala_Project.here, args => { |
68116 | 407 |
/* arguments */ |
408 |
||
409 |
var export_dir = default_export_dir |
|
410 |
var dirs: List[Path] = Nil |
|
411 |
var export_list = false |
|
412 |
var no_build = false |
|
413 |
var options = Options.init() |
|
69671 | 414 |
var export_prune = 0 |
68290 | 415 |
var export_patterns: List[String] = Nil |
68116 | 416 |
|
417 |
val getopts = Getopts(""" |
|
418 |
Usage: isabelle export [OPTIONS] SESSION |
|
419 |
||
420 |
Options are: |
|
68314
2acbf8129d8b
clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents:
68305
diff
changeset
|
421 |
-O DIR output directory for exported files (default: """ + default_export_dir + """) |
68116 | 422 |
-d DIR include session directory |
423 |
-l list exports |
|
424 |
-n no build of session |
|
425 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
69671 | 426 |
-p NUM prune path of exported files by NUM elements |
68116 | 427 |
-x PATTERN extract files matching pattern (e.g. "*:**" for all) |
428 |
||
429 |
List or export theory exports for SESSION: named blobs produced by |
|
68290 | 430 |
isabelle build. Option -l or -x is required; option -x may be repeated. |
68116 | 431 |
|
432 |
The PATTERN language resembles glob patterns in the shell, with ? and * |
|
433 |
(both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc], |
|
434 |
and variants {pattern1,pattern2,pattern3}. |
|
435 |
""", |
|
68314
2acbf8129d8b
clarified option -O: avoid conflict with build/dump option -D;
wenzelm
parents:
68305
diff
changeset
|
436 |
"O:" -> (arg => export_dir = Path.explode(arg)), |
68116 | 437 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
438 |
"l" -> (_ => export_list = true), |
|
439 |
"n" -> (_ => no_build = true), |
|
440 |
"o:" -> (arg => options = options + arg), |
|
69671 | 441 |
"p:" -> (arg => export_prune = Value.Int.parse(arg)), |
68290 | 442 |
"x:" -> (arg => export_patterns ::= arg)) |
68116 | 443 |
|
444 |
val more_args = getopts(args) |
|
445 |
val session_name = |
|
446 |
more_args match { |
|
68290 | 447 |
case List(session_name) if export_list || export_patterns.nonEmpty => session_name |
68116 | 448 |
case _ => getopts.usage() |
449 |
} |
|
450 |
||
68305 | 451 |
val progress = new Console_Progress() |
452 |
||
68116 | 453 |
|
454 |
/* build */ |
|
455 |
||
68305 | 456 |
if (!no_build) { |
457 |
val rc = |
|
68331 | 458 |
progress.interrupt_handler { |
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
459 |
Build.build_logic(options, session_name, progress = progress, dirs = dirs) |
68331 | 460 |
} |
74306 | 461 |
if (rc != Process_Result.RC.ok) sys.exit(rc) |
68116 | 462 |
} |
463 |
||
464 |
||
68288 | 465 |
/* export files */ |
68116 | 466 |
|
69854
cc0b3e177b49
system option "system_heaps" supersedes various command-line options for "system build mode";
wenzelm
parents:
69811
diff
changeset
|
467 |
val store = Sessions.store(options) |
69671 | 468 |
export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune, |
68290 | 469 |
export_list = export_list, export_patterns = export_patterns) |
68116 | 470 |
}) |
68092
888d35a19866
store exports in session database, with asynchronous / parallel compression;
wenzelm
parents:
diff
changeset
|
471 |
} |