author | wenzelm |
Mon, 07 Oct 2019 10:44:59 +0200 | |
changeset 70794 | da647a0c8313 |
parent 70787 | 15656ad28691 |
child 70795 | a90e40118874 |
permissions | -rw-r--r-- |
69012 | 1 |
/* Title: Pure/PIDE/headless.scala |
67054 | 2 |
Author: Makarius |
3 |
||
69012 | 4 |
Headless PIDE session and resources from file-system. |
67054 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
67925 | 10 |
import java.io.{File => JFile} |
11 |
||
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
12 |
import scala.annotation.tailrec |
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
13 |
import scala.collection.mutable |
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
14 |
|
67925 | 15 |
|
69012 | 16 |
object Headless |
67054 | 17 |
{ |
69012 | 18 |
/** session **/ |
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
19 |
|
68916 | 20 |
private def stable_snapshot( |
21 |
state: Document.State, version: Document.Version, name: Document.Node.Name): Document.Snapshot = |
|
22 |
{ |
|
23 |
val snapshot = state.snapshot(name) |
|
24 |
assert(version.id == snapshot.version.id) |
|
25 |
snapshot |
|
26 |
} |
|
27 |
||
69013 | 28 |
class Use_Theories_Result private[Headless]( |
67883 | 29 |
val state: Document.State, |
67889 | 30 |
val version: Document.Version, |
68925 | 31 |
val nodes: List[(Document.Node.Name, Document_Status.Node_Status)], |
32 |
val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)]) |
|
67879 | 33 |
{ |
69032
90bb4cabe1e8
clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents:
69013
diff
changeset
|
34 |
def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] = |
90bb4cabe1e8
clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents:
69013
diff
changeset
|
35 |
{ |
90bb4cabe1e8
clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents:
69013
diff
changeset
|
36 |
val committed = nodes_committed.iterator.map(_._1).toSet |
90bb4cabe1e8
clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents:
69013
diff
changeset
|
37 |
nodes.filter(p => !committed(p._1)) |
90bb4cabe1e8
clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents:
69013
diff
changeset
|
38 |
} |
90bb4cabe1e8
clarified errors: no result from forced session.stop, check pending theories;
wenzelm
parents:
69013
diff
changeset
|
39 |
|
68925 | 40 |
def snapshot(name: Document.Node.Name): Document.Snapshot = |
41 |
stable_snapshot(state, version, name) |
|
42 |
||
43 |
def ok: Boolean = |
|
44 |
(nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) |
|
67879 | 45 |
} |
46 |
||
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
47 |
private type Load = (List[Document.Node.Name], Boolean) |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
48 |
private val no_load: Load = (Nil, false) |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
49 |
|
70765 | 50 |
private sealed abstract class Load_State |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
51 |
{ |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
52 |
def next( |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
53 |
limit: Int, |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
54 |
dep_graph: Document.Node.Name.Graph[Unit], |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
55 |
finished: Document.Node.Name => Boolean): (Load, Load_State) = |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
56 |
{ |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
57 |
def make_pending(maximals: List[Document.Node.Name]): List[Document.Node.Name] = |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
58 |
{ |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
59 |
val pending = maximals.filterNot(finished) |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
60 |
if (pending.isEmpty || pending.tail.isEmpty) pending |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
61 |
else { |
70794 | 62 |
val depth = dep_graph.node_depth(_ => 1) |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
63 |
pending.sortBy(node => - depth(node)) |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
64 |
} |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
65 |
} |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
66 |
|
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
67 |
def load_checkpoints(checkpoints: List[Document.Node.Name]): (Load, Load_State) = |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
68 |
Load_Init(checkpoints).next(limit, dep_graph, finished) |
70769
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
69 |
|
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
70 |
def load_requirements( |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
71 |
pending: List[Document.Node.Name], |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
72 |
checkpoints: List[Document.Node.Name] = Nil, |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
73 |
share_common_data: Boolean = false): (Load, Load_State) = |
70769
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
74 |
{ |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
75 |
if (pending.isEmpty) load_checkpoints(checkpoints) |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
76 |
else if (limit == 0) { |
70769
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
77 |
val requirements = dep_graph.all_preds(pending).reverse |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
78 |
((requirements, share_common_data), Load_Bulk(pending, Nil, checkpoints)) |
70769
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
79 |
} |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
80 |
else { |
70794 | 81 |
def count(node: Document.Node.Name): Int = if (finished(node)) 0 else 1 |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
82 |
val reachable = dep_graph.reachable_limit(limit, count _, dep_graph.imm_preds, pending) |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
83 |
val (pending1, pending2) = pending.partition(reachable) |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
84 |
val requirements = dep_graph.all_preds(pending1).reverse |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
85 |
((requirements, share_common_data), Load_Bulk(pending1, pending2, checkpoints)) |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
86 |
} |
70769
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
87 |
} |
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
88 |
|
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
89 |
val result: (Load, Load_State) = |
70765 | 90 |
this match { |
91 |
case Load_Init(Nil) => |
|
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
92 |
val pending = make_pending(dep_graph.maximals) |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
93 |
if (pending.isEmpty) (no_load, Load_Finished) |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
94 |
else load_requirements(pending) |
70767 | 95 |
case Load_Init(target :: checkpoints) => |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
96 |
val requirements = dep_graph.all_preds(List(target)).reverse |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
97 |
((requirements, false), Load_Target(target, checkpoints)) |
70768 | 98 |
case Load_Target(pending, checkpoints) if finished(pending) => |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
99 |
val dep_graph1 = |
70767 | 100 |
if (checkpoints.isEmpty) dep_graph |
101 |
else dep_graph.exclude(dep_graph.all_succs(checkpoints).toSet) |
|
70769
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
102 |
val dep_graph2 = |
9514fdbb8abe
clarified incremental loading: requirements based on maximal nodes;
wenzelm
parents:
70768
diff
changeset
|
103 |
dep_graph1.restrict(dep_graph.all_succs(List(pending)).toSet) |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
104 |
val pending2 = make_pending(dep_graph.maximals.filter(dep_graph2.defined)) |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
105 |
load_requirements(pending2, checkpoints = checkpoints, share_common_data = true) |
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
106 |
case Load_Bulk(pending, remaining, checkpoints) if pending.forall(finished) => |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
107 |
load_requirements(remaining, checkpoints = checkpoints) |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
108 |
case st => (no_load, st) |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
109 |
} |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
110 |
|
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
111 |
val ((load_theories, share_common_data), st1) = result |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
112 |
((load_theories.filterNot(finished), share_common_data), st1) |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
113 |
} |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
114 |
} |
70765 | 115 |
private case class Load_Init(checkpoints: List[Document.Node.Name]) extends Load_State |
116 |
private case class Load_Target( |
|
70768 | 117 |
pending: Document.Node.Name, checkpoints: List[Document.Node.Name]) extends Load_State |
118 |
private case class Load_Bulk( |
|
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
119 |
pending: List[Document.Node.Name], |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
120 |
remaining: List[Document.Node.Name], |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
121 |
checkpoints: List[Document.Node.Name]) extends Load_State |
70765 | 122 |
private case object Load_Finished extends Load_State |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
123 |
|
69520 | 124 |
class Session private[Headless]( |
125 |
session_name: String, |
|
126 |
_session_options: => Options, |
|
127 |
override val resources: Resources) extends isabelle.Session(_session_options, resources) |
|
128 |
{ |
|
129 |
session => |
|
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
130 |
|
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
131 |
|
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
132 |
private def loaded_theory(name: Document.Node.Name): Boolean = |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
133 |
resources.session_base.loaded_theory(name.theory) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
134 |
|
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
135 |
|
69520 | 136 |
/* options */ |
137 |
||
70787 | 138 |
override def consolidate_delay: Time = session_options.seconds("headless_consolidate_delay") |
139 |
override def prune_delay: Time = session_options.seconds("headless_prune_delay") |
|
140 |
||
69520 | 141 |
def default_check_delay: Time = session_options.seconds("headless_check_delay") |
142 |
def default_check_limit: Int = session_options.int("headless_check_limit") |
|
143 |
def default_nodes_status_delay: Time = session_options.seconds("headless_nodes_status_delay") |
|
144 |
def default_watchdog_timeout: Time = session_options.seconds("headless_watchdog_timeout") |
|
145 |
def default_commit_cleanup_delay: Time = session_options.seconds("headless_commit_cleanup_delay") |
|
67063 | 146 |
|
70772
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
147 |
def load_limit: Int = |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
148 |
{ |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
149 |
val limit = session_options.int("headless_load_limit") |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
150 |
if (limit == 0) Integer.MAX_VALUE else limit |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
151 |
} |
030a6baa5cb2
support headless_load_limit for more scalable load process;
wenzelm
parents:
70770
diff
changeset
|
152 |
|
68922 | 153 |
|
154 |
/* temporary directory */ |
|
155 |
||
67925 | 156 |
val tmp_dir: JFile = Isabelle_System.tmp_dir("server_session") |
67946 | 157 |
val tmp_dir_name: String = File.path(tmp_dir).implode |
67925 | 158 |
|
68923 | 159 |
def master_directory(master_dir: String): String = |
160 |
proper_string(master_dir) getOrElse tmp_dir_name |
|
161 |
||
67945 | 162 |
override def toString: String = session_name |
163 |
||
67925 | 164 |
override def stop(): Process_Result = |
165 |
{ |
|
166 |
try { super.stop() } |
|
167 |
finally { Isabelle_System.rm_tree(tmp_dir) } |
|
168 |
} |
|
169 |
||
67936 | 170 |
|
171 |
/* theories */ |
|
172 |
||
68914 | 173 |
private sealed case class Use_Theories_State( |
70697 | 174 |
dep_graph: Document.Node.Name.Graph[Unit], |
70765 | 175 |
load_state: Load_State, |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
176 |
watchdog_timeout: Time, |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
177 |
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit], |
68914 | 178 |
last_update: Time = Time.now(), |
179 |
nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty, |
|
68925 | 180 |
already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty, |
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
181 |
result: Option[Exn.Result[Use_Theories_Result]] = None) |
68914 | 182 |
{ |
183 |
def update(new_nodes_status: Document_Status.Nodes_Status): Use_Theories_State = |
|
184 |
copy(last_update = Time.now(), nodes_status = new_nodes_status) |
|
185 |
||
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
186 |
def watchdog: Boolean = |
68914 | 187 |
watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout |
188 |
||
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
189 |
def finished_result: Boolean = result.isDefined |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
190 |
|
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
191 |
def join_result: Option[(Exn.Result[Use_Theories_Result], Use_Theories_State)] = |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
192 |
if (finished_result) Some((result.get, this)) else None |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
193 |
|
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
194 |
def cancel_result: Use_Theories_State = |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
195 |
if (finished_result) this else copy(result = Some(Exn.Exn(Exn.Interrupt()))) |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
196 |
|
70763
5fae55752c70
tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents:
70710
diff
changeset
|
197 |
def clean_theories: (List[Document.Node.Name], Use_Theories_State) = |
70698 | 198 |
{ |
199 |
@tailrec def frontier(base: List[Document.Node.Name], front: Set[Document.Node.Name]) |
|
200 |
: Set[Document.Node.Name] = |
|
201 |
{ |
|
202 |
val add = base.filter(name => dep_graph.imm_succs(name).forall(front)) |
|
203 |
if (add.isEmpty) front |
|
204 |
else { |
|
205 |
val preds = add.map(dep_graph.imm_preds) |
|
206 |
val base1 = (preds.head /: preds.tail)(_ ++ _).toList.filter(already_committed.keySet) |
|
207 |
frontier(base1, front ++ add) |
|
208 |
} |
|
209 |
} |
|
210 |
||
70763
5fae55752c70
tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents:
70710
diff
changeset
|
211 |
if (already_committed.isEmpty) (Nil, this) |
70698 | 212 |
else { |
70705 | 213 |
val base = |
214 |
(for { |
|
215 |
(name, (_, (_, succs))) <- dep_graph.iterator |
|
216 |
if succs.isEmpty && already_committed.isDefinedAt(name) |
|
217 |
} yield name).toList |
|
218 |
val clean = frontier(base, Set.empty) |
|
70763
5fae55752c70
tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents:
70710
diff
changeset
|
219 |
if (clean.isEmpty) (Nil, this) |
70698 | 220 |
else { |
70763
5fae55752c70
tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents:
70710
diff
changeset
|
221 |
(dep_graph.topological_order.filter(clean), |
70699 | 222 |
copy(dep_graph = dep_graph.exclude(clean))) |
70698 | 223 |
} |
224 |
} |
|
225 |
} |
|
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
226 |
|
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
227 |
def check(state: Document.State, version: Document.Version, beyond_limit: Boolean) |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
228 |
: ((List[Document.Node.Name], Boolean), Use_Theories_State) = |
68916 | 229 |
{ |
69035 | 230 |
val already_committed1 = |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
231 |
commit match { |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
232 |
case None => already_committed |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
233 |
case Some(commit_fn) => |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
234 |
(already_committed /: dep_graph.topological_order)( |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
235 |
{ case (committed, name) => |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
236 |
def parents_committed: Boolean = |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
237 |
version.nodes(name).header.imports.forall(parent => |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
238 |
loaded_theory(parent) || committed.isDefinedAt(parent)) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
239 |
if (!committed.isDefinedAt(name) && parents_committed && |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
240 |
state.node_consolidated(version, name)) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
241 |
{ |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
242 |
val snapshot = stable_snapshot(state, version, name) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
243 |
val status = Document_Status.Node_Status.make(state, version, name) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
244 |
commit_fn(snapshot, status) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
245 |
committed + (name -> status) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
246 |
} |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
247 |
else committed |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
248 |
}) |
68916 | 249 |
} |
250 |
||
70657 | 251 |
def finished_theory(name: Document.Node.Name): Boolean = |
252 |
loaded_theory(name) || |
|
70704 | 253 |
(if (commit.isDefined) already_committed1.isDefinedAt(name) |
254 |
else state.node_consolidated(version, name)) |
|
70657 | 255 |
|
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
256 |
val result1 = |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
257 |
if (!finished_result && |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
258 |
(beyond_limit || watchdog || |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
259 |
dep_graph.keys_iterator.forall(name => |
70657 | 260 |
finished_theory(name) || nodes_status.quasi_consolidated(name)))) |
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
261 |
{ |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
262 |
val nodes = |
70657 | 263 |
(for { |
264 |
name <- dep_graph.keys_iterator |
|
265 |
if !loaded_theory(name) |
|
266 |
} yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList |
|
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
267 |
val nodes_committed = |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
268 |
(for { |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
269 |
name <- dep_graph.keys_iterator |
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
270 |
status <- already_committed1.get(name) |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
271 |
} yield (name -> status)).toList |
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
272 |
Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed))) |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
273 |
} |
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
274 |
else result |
68925 | 275 |
|
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
276 |
val (load, load_state1) = load_state.next(load_limit, dep_graph, finished_theory(_)) |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
277 |
|
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
278 |
(load, |
70765 | 279 |
copy(already_committed = already_committed1, result = result1, load_state = load_state1)) |
68916 | 280 |
} |
68914 | 281 |
} |
282 |
||
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
283 |
def use_theories( |
67940
b4e80f062fbf
clarified signature -- eliminated somewhat pointless positions;
wenzelm
parents:
67939
diff
changeset
|
284 |
theories: List[String], |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
285 |
qualifier: String = Sessions.DRAFT, |
67881 | 286 |
master_dir: String = "", |
69920 | 287 |
unicode_symbols: Boolean = false, |
68943 | 288 |
check_delay: Time = default_check_delay, |
69520 | 289 |
check_limit: Int = default_check_limit, |
68947 | 290 |
watchdog_timeout: Time = default_watchdog_timeout, |
68943 | 291 |
nodes_status_delay: Time = default_nodes_status_delay, |
69458 | 292 |
id: UUID.T = UUID.random(), |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
293 |
checkpoints: Set[Document.Node.Name] = Set.empty, |
68916 | 294 |
// commit: must not block, must not fail |
295 |
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None, |
|
68981 | 296 |
commit_cleanup_delay: Time = default_commit_cleanup_delay, |
69013 | 297 |
progress: Progress = No_Progress): Use_Theories_Result = |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
298 |
{ |
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
299 |
val dependencies = |
68894
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
300 |
{ |
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
301 |
val import_names = |
68923 | 302 |
theories.map(thy => |
303 |
resources.import_name(qualifier, master_directory(master_dir), thy) -> Position.none) |
|
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
304 |
resources.dependencies(import_names, progress = progress).check_errors |
68894
1dbdad1b57a5
more robust: load_theories after consumer is installed;
wenzelm
parents:
68888
diff
changeset
|
305 |
} |
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
306 |
val dep_theories = dependencies.theories |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
307 |
val dep_theories_set = dep_theories.toSet |
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
308 |
val dep_files = |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
309 |
dependencies.loaded_files(false).flatMap(_._2). |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
310 |
map(path => Document.Node.Name(resources.append("", path))) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
311 |
|
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
312 |
val use_theories_state = |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
313 |
{ |
70765 | 314 |
val load_state = |
315 |
Load_Init( |
|
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
316 |
if (checkpoints.isEmpty) Nil |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
317 |
else dependencies.theory_graph.topological_order.filter(checkpoints(_))) |
70697 | 318 |
Synchronized( |
70765 | 319 |
Use_Theories_State(dependencies.theory_graph, load_state, watchdog_timeout, commit)) |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
320 |
} |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
321 |
|
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
322 |
def check_state(beyond_limit: Boolean = false) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
323 |
{ |
70775
97d3485028b6
more sequential access to Session.manager.global_state: avoid minor divergence of tip version;
wenzelm
parents:
70774
diff
changeset
|
324 |
val state = session.get_state() |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
325 |
for (version <- state.stable_tip_version) { |
70774
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
326 |
val (load_theories, share_common_data) = |
64751a7abfa6
clarified share_common_data: after finished checkpoint, before next edits;
wenzelm
parents:
70772
diff
changeset
|
327 |
use_theories_state.change_result(_.check(state, version, beyond_limit)) |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
328 |
if (load_theories.nonEmpty) { |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
329 |
resources.load_theories( |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
330 |
session, id, load_theories, dep_files, unicode_symbols, share_common_data, progress) |
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
331 |
} |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
332 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
333 |
} |
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
334 |
|
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
335 |
val check_progress = |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
336 |
{ |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
337 |
var check_count = 0 |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
338 |
Event_Timer.request(Time.now(), repeat = Some(check_delay)) |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
339 |
{ |
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
340 |
if (progress.stopped) use_theories_state.change(_.cancel_result) |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
341 |
else { |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
342 |
check_count += 1 |
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
343 |
check_state(check_limit > 0 && check_count > check_limit) |
68694
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
344 |
} |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
345 |
} |
03e104be99af
added check_delay / check_limit for more robust treatment of structurally broken theory sources (or genuine non-termination);
wenzelm
parents:
68365
diff
changeset
|
346 |
} |
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
347 |
|
68906 | 348 |
val consumer = |
349 |
{ |
|
350 |
val delay_nodes_status = |
|
351 |
Standard_Thread.delay_first(nodes_status_delay max Time.zero) { |
|
69818
60d0ee8f2ddb
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents:
69817
diff
changeset
|
352 |
progress.nodes_status(use_theories_state.value.nodes_status) |
68906 | 353 |
} |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
354 |
|
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
355 |
val delay_commit_clean = |
68981 | 356 |
Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) { |
70763
5fae55752c70
tuned messages (again) -- avoid confusion wrt. total remaining size;
wenzelm
parents:
70710
diff
changeset
|
357 |
val clean_theories = use_theories_state.change_result(_.clean_theories) |
70702 | 358 |
if (clean_theories.nonEmpty) { |
70770 | 359 |
progress.echo("Removing " + clean_theories.length + " theories ...") |
70702 | 360 |
resources.clean_theories(session, id, clean_theories) |
361 |
} |
|
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
362 |
} |
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
363 |
|
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
364 |
Session.Consumer[Session.Commands_Changed](getClass.getName) { |
68330 | 365 |
case changed => |
68770
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
366 |
if (changed.nodes.exists(dep_theories_set)) { |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
367 |
val snapshot = session.snapshot() |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
368 |
val state = snapshot.state |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
369 |
val version = snapshot.version |
add44e2b8cb0
optional notification of nodes_status (via progress);
wenzelm
parents:
68758
diff
changeset
|
370 |
|
68957 | 371 |
val theory_progress = |
68914 | 372 |
use_theories_state.change_result(st => |
68903 | 373 |
{ |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
374 |
val domain = |
68914 | 375 |
if (st.nodes_status.is_empty) dep_theories_set |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
376 |
else changed.nodes.iterator.filter(dep_theories_set).toSet |
68899 | 377 |
|
68903 | 378 |
val (nodes_status_changed, nodes_status1) = |
69255
800b1ce96fce
more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents:
69035
diff
changeset
|
379 |
st.nodes_status.update(resources, state, version, |
68903 | 380 |
domain = Some(domain), trim = changed.assignment) |
68899 | 381 |
|
68903 | 382 |
if (nodes_status_delay >= Time.zero && nodes_status_changed) { |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
383 |
delay_nodes_status.invoke |
68899 | 384 |
} |
68883
3653b3ad729e
clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents:
68771
diff
changeset
|
385 |
|
68957 | 386 |
val theory_progress = |
68905 | 387 |
(for { |
69818
60d0ee8f2ddb
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents:
69817
diff
changeset
|
388 |
(name, node_status) <- nodes_status1.present.iterator |
68959 | 389 |
if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name) |
68962 | 390 |
p1 = node_status.percentage |
391 |
if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage) |
|
392 |
} yield Progress.Theory(name.theory, percentage = Some(p1))).toList |
|
68903 | 393 |
|
68957 | 394 |
(theory_progress, st.update(nodes_status1)) |
68903 | 395 |
}) |
68330 | 396 |
|
68957 | 397 |
theory_progress.foreach(progress.theory(_)) |
68903 | 398 |
|
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
399 |
check_state() |
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
400 |
|
68981 | 401 |
if (commit.isDefined && commit_cleanup_delay > Time.zero) { |
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
402 |
if (use_theories_state.value.finished_result) |
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
403 |
delay_commit_clean.revoke |
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
404 |
else delay_commit_clean.invoke |
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
405 |
} |
68330 | 406 |
} |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
407 |
} |
68906 | 408 |
} |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
409 |
|
67892 | 410 |
try { |
411 |
session.commands_changed += consumer |
|
70653
f7c5b30fc432
load theories in stages, to reduce ML heap requirements;
wenzelm
parents:
70649
diff
changeset
|
412 |
check_state() |
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
413 |
use_theories_state.guarded_access(_.join_result) |
67894
fee080c4045f
more robust check_state loop, even without session activity (e.g. idempotent use_theories);
wenzelm
parents:
67893
diff
changeset
|
414 |
check_progress.cancel |
67892 | 415 |
} |
416 |
finally { |
|
68907 | 417 |
session.commands_changed -= consumer |
67892 | 418 |
resources.unload_theories(session, id, dep_theories) |
419 |
} |
|
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
420 |
|
70644
b23a6dfcfd57
clarified state variable: avoid extra mutability via Promise;
wenzelm
parents:
70640
diff
changeset
|
421 |
Exn.release(use_theories_state.guarded_access(_.join_result)) |
67064
fb487246ef4f
synchronous use_theories, based on consolidated_state;
wenzelm
parents:
67063
diff
changeset
|
422 |
} |
67936 | 423 |
|
67939 | 424 |
def purge_theories( |
68915 | 425 |
theories: List[String], |
426 |
qualifier: String = Sessions.DRAFT, |
|
427 |
master_dir: String = "", |
|
428 |
all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) = |
|
429 |
{ |
|
68923 | 430 |
val nodes = |
431 |
if (all) None |
|
432 |
else Some(theories.map(resources.import_name(qualifier, master_directory(master_dir), _))) |
|
68915 | 433 |
resources.purge_theories(session, nodes) |
434 |
} |
|
67063 | 435 |
} |
436 |
||
67061
2efa25302f34
synchronous session start (similar to isabelle.vscode.Server);
wenzelm
parents:
67059
diff
changeset
|
437 |
|
67054 | 438 |
|
69012 | 439 |
/** resources **/ |
68922 | 440 |
|
69012 | 441 |
object Resources |
442 |
{ |
|
69536 | 443 |
def apply(base_info: Sessions.Base_Info, log: Logger = No_Logger): Resources = |
444 |
new Resources(base_info, log = log) |
|
445 |
||
446 |
def make( |
|
447 |
options: Options, |
|
448 |
session_name: String, |
|
449 |
session_dirs: List[Path] = Nil, |
|
450 |
include_sessions: List[String] = Nil, |
|
451 |
progress: Progress = No_Progress, |
|
452 |
log: Logger = No_Logger): Resources = |
|
453 |
{ |
|
454 |
val base_info = |
|
455 |
Sessions.base_info(options, session_name, dirs = session_dirs, |
|
456 |
include_sessions = include_sessions, progress = progress) |
|
457 |
apply(base_info, log = log) |
|
458 |
} |
|
459 |
||
69012 | 460 |
final class Theory private[Headless]( |
461 |
val node_name: Document.Node.Name, |
|
462 |
val node_header: Document.Node.Header, |
|
463 |
val text: String, |
|
464 |
val node_required: Boolean) |
|
68922 | 465 |
{ |
69012 | 466 |
override def toString: String = node_name.toString |
68922 | 467 |
|
69012 | 468 |
def node_perspective: Document.Node.Perspective_Text = |
469 |
Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty) |
|
68922 | 470 |
|
69012 | 471 |
def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] = |
472 |
List(node_name -> Document.Node.Deps(node_header), |
|
473 |
node_name -> Document.Node.Edits(text_edits), |
|
474 |
node_name -> node_perspective) |
|
68922 | 475 |
|
69012 | 476 |
def node_edits(old: Option[Theory]): List[Document.Edit_Text] = |
477 |
{ |
|
478 |
val (text_edits, old_required) = |
|
479 |
if (old.isEmpty) (Text.Edit.inserts(0, text), false) |
|
480 |
else (Text.Edit.replace(0, old.get.text, text), old.get.node_required) |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
481 |
|
69012 | 482 |
if (text_edits.isEmpty && node_required == old_required) Nil |
483 |
else make_edits(text_edits) |
|
484 |
} |
|
67887
a4d5342898b1
unload_theories: actually observe required state;
wenzelm
parents:
67885
diff
changeset
|
485 |
|
69012 | 486 |
def purge_edits: List[Document.Edit_Text] = |
487 |
make_edits(Text.Edit.removes(0, text)) |
|
67936 | 488 |
|
69012 | 489 |
def required(required: Boolean): Theory = |
490 |
if (required == node_required) this |
|
491 |
else new Theory(node_name, node_header, text, required) |
|
67936 | 492 |
} |
493 |
||
69012 | 494 |
sealed case class State( |
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
495 |
blobs: Map[Document.Node.Name, Document.Blob] = Map.empty, |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
496 |
theories: Map[Document.Node.Name, Theory] = Map.empty, |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
497 |
required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty) |
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
498 |
{ |
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
499 |
/* blobs */ |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
500 |
|
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
501 |
def doc_blobs: Document.Blobs = Document.Blobs(blobs) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
502 |
|
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
503 |
def update_blobs(names: List[Document.Node.Name]): (Document.Blobs, State) = |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
504 |
{ |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
505 |
val new_blobs = |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
506 |
names.flatMap(name => |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
507 |
{ |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
508 |
val bytes = Bytes.read(name.path) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
509 |
def new_blob: Document.Blob = |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
510 |
{ |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
511 |
val text = bytes.text |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
512 |
Document.Blob(bytes, text, Symbol.Text_Chunk(text), changed = true) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
513 |
} |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
514 |
blobs.get(name) match { |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
515 |
case Some(blob) => if (blob.bytes == bytes) None else Some(name -> new_blob) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
516 |
case None => Some(name -> new_blob) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
517 |
} |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
518 |
}) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
519 |
val blobs1 = (blobs /: new_blobs)(_ + _) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
520 |
val blobs2 = (blobs /: new_blobs)({ case (map, (a, b)) => map + (a -> b.unchanged) }) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
521 |
(Document.Blobs(blobs1), copy(blobs = blobs2)) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
522 |
} |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
523 |
|
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
524 |
def blob_edits(name: Document.Node.Name, old_blob: Option[Document.Blob]) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
525 |
: List[Document.Edit_Text] = |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
526 |
{ |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
527 |
val blob = blobs.getOrElse(name, error("Missing blob " + quote(name.toString))) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
528 |
val text_edits = |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
529 |
old_blob match { |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
530 |
case None => List(Text.Edit.insert(0, blob.source)) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
531 |
case Some(blob0) => Text.Edit.replace(0, blob0.source, blob.source) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
532 |
} |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
533 |
if (text_edits.isEmpty) Nil |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
534 |
else List(name -> Document.Node.Blob(blob), name -> Document.Node.Edits(text_edits)) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
535 |
} |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
536 |
|
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
537 |
|
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
538 |
/* theories */ |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
539 |
|
70674
29bb1ebb188f
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents:
70657
diff
changeset
|
540 |
lazy val theory_graph: Document.Node.Name.Graph[Unit] = |
29bb1ebb188f
clarified signature: proper Document.Node.Ordering conforming to equality (e.g. required in situations where theory names are ambiguous due to overlapping session directories);
wenzelm
parents:
70657
diff
changeset
|
541 |
Document.Node.Name.make_graph( |
69012 | 542 |
for ((name, theory) <- theories.toList) |
70647 | 543 |
yield ((name, ()), theory.node_header.imports.filter(theories.isDefinedAt(_)))) |
67056 | 544 |
|
69012 | 545 |
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name) |
546 |
||
69458 | 547 |
def insert_required(id: UUID.T, names: List[Document.Node.Name]): State = |
69012 | 548 |
copy(required = (required /: names)(_.insert(_, id))) |
549 |
||
69458 | 550 |
def remove_required(id: UUID.T, names: List[Document.Node.Name]): State = |
69012 | 551 |
copy(required = (required /: names)(_.remove(_, id))) |
68958 | 552 |
|
69012 | 553 |
def update_theories(update: List[(Document.Node.Name, Theory)]): State = |
554 |
copy(theories = |
|
555 |
(theories /: update)({ case (thys, (name, thy)) => |
|
556 |
thys.get(name) match { |
|
557 |
case Some(thy1) if thy1 == thy => thys |
|
558 |
case _ => thys + (name -> thy) |
|
559 |
} |
|
560 |
})) |
|
561 |
||
562 |
def remove_theories(remove: List[Document.Node.Name]): State = |
|
67893 | 563 |
{ |
69012 | 564 |
require(remove.forall(name => !is_required(name))) |
565 |
copy(theories = theories -- remove) |
|
566 |
} |
|
567 |
||
70649 | 568 |
def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
70783 | 569 |
: (List[Document.Edit_Text], State) = |
69012 | 570 |
{ |
70649 | 571 |
val st1 = remove_required(id, theories) |
67893 | 572 |
val theory_edits = |
69012 | 573 |
for { |
70649 | 574 |
node_name <- theories |
69012 | 575 |
theory <- st1.theories.get(node_name) |
576 |
} |
|
67893 | 577 |
yield { |
578 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
69012 | 579 |
val edits = theory1.node_edits(Some(theory)) |
67893 | 580 |
(edits, (node_name, theory1)) |
581 |
} |
|
70783 | 582 |
(theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2))) |
69012 | 583 |
} |
584 |
||
70782 | 585 |
def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) |
70783 | 586 |
: ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) = |
69012 | 587 |
{ |
588 |
val all_nodes = theory_graph.topological_order |
|
70782 | 589 |
val purge = nodes.getOrElse(all_nodes).filterNot(is_required(_)).toSet |
69012 | 590 |
|
591 |
val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet |
|
592 |
val (retained, purged) = all_nodes.partition(retain) |
|
70783 | 593 |
val purge_edits = purged.flatMap(name => theories(name).purge_edits) |
69012 | 594 |
|
70783 | 595 |
((purged, retained, purge_edits), remove_theories(purged)) |
69012 | 596 |
} |
597 |
} |
|
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
598 |
} |
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
599 |
|
69536 | 600 |
class Resources private[Headless]( |
601 |
val session_base_info: Sessions.Base_Info, |
|
602 |
log: Logger = No_Logger) |
|
70683
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70674
diff
changeset
|
603 |
extends isabelle.Resources( |
8c7706b053c7
find theory files via session structure: much faster Prover IDE startup;
wenzelm
parents:
70674
diff
changeset
|
604 |
session_base_info.sessions_structure, session_base_info.check_base, log = log) |
67884
43af581d7d8e
unload_theories after consolidation -- reset node_required;
wenzelm
parents:
67883
diff
changeset
|
605 |
{ |
69012 | 606 |
resources => |
607 |
||
69538
faf547d2834c
clarified signature, notably cascade of dump_options, deps, resources, session;
wenzelm
parents:
69536
diff
changeset
|
608 |
def options: Options = session_base_info.options |
faf547d2834c
clarified signature, notably cascade of dump_options, deps, resources, session;
wenzelm
parents:
69536
diff
changeset
|
609 |
|
69536 | 610 |
|
611 |
/* session */ |
|
612 |
||
613 |
def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session = |
|
614 |
{ |
|
615 |
val session = new Session(session_base_info.session, options, resources) |
|
616 |
||
617 |
val session_error = Future.promise[String] |
|
618 |
var session_phase: Session.Consumer[Session.Phase] = null |
|
619 |
session_phase = |
|
620 |
Session.Consumer(getClass.getName) { |
|
621 |
case Session.Ready => |
|
622 |
session.phase_changed -= session_phase |
|
623 |
session_error.fulfill("") |
|
624 |
case Session.Terminated(result) if !result.ok => |
|
625 |
session.phase_changed -= session_phase |
|
626 |
session_error.fulfill("Session start failed: return code " + result.rc) |
|
627 |
case _ => |
|
628 |
} |
|
629 |
session.phase_changed += session_phase |
|
630 |
||
631 |
progress.echo("Starting session " + session_base_info.session + " ...") |
|
632 |
Isabelle_Process.start(session, options, |
|
633 |
logic = session_base_info.session, dirs = session_base_info.dirs, modes = print_mode) |
|
634 |
||
635 |
session_error.join match { |
|
636 |
case "" => session |
|
637 |
case msg => session.stop(); error(msg) |
|
638 |
} |
|
639 |
} |
|
640 |
||
641 |
||
642 |
/* theories */ |
|
643 |
||
69012 | 644 |
private val state = Synchronized(Resources.State()) |
645 |
||
646 |
def load_theories( |
|
647 |
session: Session, |
|
69458 | 648 |
id: UUID.T, |
70649 | 649 |
theories: List[Document.Node.Name], |
650 |
files: List[Document.Node.Name], |
|
69920 | 651 |
unicode_symbols: Boolean, |
70625
1ae987cc052f
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
wenzelm
parents:
69920
diff
changeset
|
652 |
share_common_data: Boolean, |
69012 | 653 |
progress: Progress) |
654 |
{ |
|
655 |
val loaded_theories = |
|
70649 | 656 |
for (node_name <- theories) |
69012 | 657 |
yield { |
658 |
val path = node_name.path |
|
659 |
if (!node_name.is_theory) error("Not a theory file: " + path) |
|
660 |
||
661 |
progress.expose_interrupt() |
|
69920 | 662 |
val text0 = File.read(path) |
663 |
val text = if (unicode_symbols) Symbol.decode(text0) else text0 |
|
69012 | 664 |
val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text)) |
665 |
new Resources.Theory(node_name, node_header, text, true) |
|
68936
90c08c7bab9c
continuously clean frontier of already committed theories: much less resource requirements;
wenzelm
parents:
68935
diff
changeset
|
666 |
} |
69012 | 667 |
|
668 |
val loaded = loaded_theories.length |
|
669 |
if (loaded > 1) progress.echo("Loading " + loaded + " theories ...") |
|
670 |
||
671 |
state.change(st => |
|
672 |
{ |
|
70649 | 673 |
val (doc_blobs1, st1) = st.insert_required(id, theories).update_blobs(files) |
69012 | 674 |
val theory_edits = |
675 |
for (theory <- loaded_theories) |
|
676 |
yield { |
|
677 |
val node_name = theory.node_name |
|
678 |
val theory1 = theory.required(st1.is_required(node_name)) |
|
679 |
val edits = theory1.node_edits(st1.theories.get(node_name)) |
|
680 |
(edits, (node_name, theory1)) |
|
681 |
} |
|
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
682 |
val file_edits = |
70649 | 683 |
for { node_name <- files if doc_blobs1.changed(node_name) } |
69562
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
684 |
yield st1.blob_edits(node_name, st.blobs.get(node_name)) |
636b3c03a61a
include loaded_files as doc_blobs (without purging);
wenzelm
parents:
69538
diff
changeset
|
685 |
|
70625
1ae987cc052f
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
wenzelm
parents:
69920
diff
changeset
|
686 |
session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten, |
1ae987cc052f
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
wenzelm
parents:
69920
diff
changeset
|
687 |
share_common_data = share_common_data) |
69012 | 688 |
st1.update_theories(theory_edits.map(_._2)) |
689 |
}) |
|
690 |
} |
|
67936 | 691 |
|
70649 | 692 |
def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
69012 | 693 |
{ |
70783 | 694 |
state.change(st => |
695 |
{ |
|
696 |
val (edits, st1) = st.unload_theories(session, id, theories) |
|
697 |
session.update(st.doc_blobs, edits) |
|
698 |
st1 |
|
699 |
}) |
|
69012 | 700 |
} |
701 |
||
70698 | 702 |
def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name]) |
69012 | 703 |
{ |
704 |
state.change(st => |
|
70783 | 705 |
{ |
706 |
val (edits1, st1) = st.unload_theories(session, id, theories) |
|
707 |
val ((_, _, edits2), st2) = st1.purge_theories(session, None) |
|
708 |
session.update(st.doc_blobs, edits1 ::: edits2) |
|
709 |
st2 |
|
710 |
}) |
|
69012 | 711 |
} |
712 |
||
713 |
def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]]) |
|
714 |
: (List[Document.Node.Name], List[Document.Node.Name]) = |
|
715 |
{ |
|
70783 | 716 |
state.change_result(st => |
717 |
{ |
|
718 |
val ((purged, retained, _), st1) = st.purge_theories(session, nodes) |
|
719 |
((purged, retained), st1) |
|
720 |
}) |
|
69012 | 721 |
} |
67936 | 722 |
} |
67054 | 723 |
} |