62631
|
1 |
/* Title: Pure/Thy/sessions.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Session information.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
import scala.collection.SortedSet
|
|
11 |
import scala.collection.mutable
|
|
12 |
|
|
13 |
|
|
14 |
object Sessions
|
|
15 |
{
|
|
16 |
/* info */
|
|
17 |
|
|
18 |
val ROOT = Path.explode("ROOT")
|
|
19 |
val ROOTS = Path.explode("ROOTS")
|
|
20 |
|
|
21 |
def is_pure(name: String): Boolean = name == "Pure"
|
|
22 |
|
|
23 |
sealed case class Info(
|
|
24 |
chapter: String,
|
|
25 |
select: Boolean,
|
|
26 |
pos: Position.T,
|
|
27 |
groups: List[String],
|
|
28 |
dir: Path,
|
|
29 |
parent: Option[String],
|
|
30 |
description: String,
|
|
31 |
options: Options,
|
|
32 |
theories: List[(Boolean, Options, List[Path])],
|
|
33 |
files: List[Path],
|
|
34 |
document_files: List[(Path, Path)],
|
|
35 |
meta_digest: SHA1.Digest)
|
|
36 |
{
|
|
37 |
def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
|
|
38 |
}
|
|
39 |
|
|
40 |
|
|
41 |
/* session tree */
|
|
42 |
|
|
43 |
object Tree
|
|
44 |
{
|
|
45 |
def apply(infos: Seq[(String, Info)]): Tree =
|
|
46 |
{
|
|
47 |
val graph1 =
|
|
48 |
(Graph.string[Info] /: infos) {
|
|
49 |
case (graph, (name, info)) =>
|
|
50 |
if (graph.defined(name))
|
|
51 |
error("Duplicate session " + quote(name) + Position.here(info.pos) +
|
|
52 |
Position.here(graph.get_node(name).pos))
|
|
53 |
else graph.new_node(name, info)
|
|
54 |
}
|
|
55 |
val graph2 =
|
|
56 |
(graph1 /: graph1.iterator) {
|
|
57 |
case (graph, (name, (info, _))) =>
|
|
58 |
info.parent match {
|
|
59 |
case None => graph
|
|
60 |
case Some(parent) =>
|
|
61 |
if (!graph.defined(parent))
|
|
62 |
error("Bad parent session " + quote(parent) + " for " +
|
|
63 |
quote(name) + Position.here(info.pos))
|
|
64 |
|
|
65 |
try { graph.add_edge_acyclic(parent, name) }
|
|
66 |
catch {
|
|
67 |
case exn: Graph.Cycles[_] =>
|
|
68 |
error(cat_lines(exn.cycles.map(cycle =>
|
|
69 |
"Cyclic session dependency of " +
|
|
70 |
cycle.map(c => quote(c.toString)).mkString(" via "))) +
|
|
71 |
Position.here(info.pos))
|
|
72 |
}
|
|
73 |
}
|
|
74 |
}
|
|
75 |
new Tree(graph2)
|
|
76 |
}
|
|
77 |
}
|
|
78 |
|
|
79 |
final class Tree private(val graph: Graph[String, Info])
|
|
80 |
extends PartialFunction[String, Info]
|
|
81 |
{
|
|
82 |
def apply(name: String): Info = graph.get_node(name)
|
|
83 |
def isDefinedAt(name: String): Boolean = graph.defined(name)
|
|
84 |
|
|
85 |
def selection(
|
|
86 |
requirements: Boolean = false,
|
|
87 |
all_sessions: Boolean = false,
|
|
88 |
exclude_session_groups: List[String] = Nil,
|
|
89 |
exclude_sessions: List[String] = Nil,
|
|
90 |
session_groups: List[String] = Nil,
|
|
91 |
sessions: List[String] = Nil): (List[String], Tree) =
|
|
92 |
{
|
|
93 |
val bad_sessions =
|
|
94 |
SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
|
|
95 |
if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
|
|
96 |
|
|
97 |
val excluded =
|
|
98 |
{
|
|
99 |
val exclude_group = exclude_session_groups.toSet
|
|
100 |
val exclude_group_sessions =
|
|
101 |
(for {
|
|
102 |
(name, (info, _)) <- graph.iterator
|
|
103 |
if apply(name).groups.exists(exclude_group)
|
|
104 |
} yield name).toList
|
|
105 |
graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
|
|
106 |
}
|
|
107 |
|
|
108 |
val pre_selected =
|
|
109 |
{
|
|
110 |
if (all_sessions) graph.keys
|
|
111 |
else {
|
|
112 |
val select_group = session_groups.toSet
|
|
113 |
val select = sessions.toSet
|
|
114 |
(for {
|
|
115 |
(name, (info, _)) <- graph.iterator
|
|
116 |
if info.select || select(name) || apply(name).groups.exists(select_group)
|
|
117 |
} yield name).toList
|
|
118 |
}
|
|
119 |
}.filterNot(excluded)
|
|
120 |
|
|
121 |
val selected =
|
|
122 |
if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
|
|
123 |
else pre_selected
|
|
124 |
|
|
125 |
val graph1 = graph.restrict(graph.all_preds(selected).toSet)
|
|
126 |
(selected, new Tree(graph1))
|
|
127 |
}
|
|
128 |
|
|
129 |
def ancestors(name: String): List[String] =
|
|
130 |
graph.all_preds(List(name)).tail.reverse
|
|
131 |
|
|
132 |
def topological_order: List[(String, Info)] =
|
|
133 |
graph.topological_order.map(name => (name, apply(name)))
|
|
134 |
|
|
135 |
override def toString: String = graph.keys_iterator.mkString("Sessions.Tree(", ", ", ")")
|
|
136 |
}
|
|
137 |
|
|
138 |
|
|
139 |
/* parser */
|
|
140 |
|
|
141 |
private val CHAPTER = "chapter"
|
|
142 |
private val SESSION = "session"
|
|
143 |
private val IN = "in"
|
|
144 |
private val DESCRIPTION = "description"
|
|
145 |
private val OPTIONS = "options"
|
|
146 |
private val GLOBAL_THEORIES = "global_theories"
|
|
147 |
private val THEORIES = "theories"
|
|
148 |
private val FILES = "files"
|
|
149 |
private val DOCUMENT_FILES = "document_files"
|
|
150 |
|
|
151 |
lazy val root_syntax =
|
|
152 |
Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
|
|
153 |
(CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
|
|
154 |
IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
|
|
155 |
|
|
156 |
object Parser extends Parse.Parser
|
|
157 |
{
|
|
158 |
private abstract class Entry
|
|
159 |
private sealed case class Chapter(name: String) extends Entry
|
|
160 |
private sealed case class Session_Entry(
|
|
161 |
pos: Position.T,
|
|
162 |
name: String,
|
|
163 |
groups: List[String],
|
|
164 |
path: String,
|
|
165 |
parent: Option[String],
|
|
166 |
description: String,
|
|
167 |
options: List[Options.Spec],
|
|
168 |
theories: List[(Boolean, List[Options.Spec], List[String])],
|
|
169 |
files: List[String],
|
|
170 |
document_files: List[(String, String)]) extends Entry
|
|
171 |
|
|
172 |
private val chapter: Parser[Chapter] =
|
|
173 |
{
|
|
174 |
val chapter_name = atom("chapter name", _.is_name)
|
|
175 |
|
|
176 |
command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
|
|
177 |
}
|
|
178 |
|
|
179 |
private val session_entry: Parser[Session_Entry] =
|
|
180 |
{
|
|
181 |
val session_name = atom("session name", _.is_name)
|
|
182 |
|
|
183 |
val option =
|
|
184 |
name ~ opt($$$("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
|
|
185 |
val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
|
|
186 |
|
|
187 |
val theories =
|
|
188 |
($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
|
|
189 |
((options | success(Nil)) ~ rep(theory_xname)) ^^
|
|
190 |
{ case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
|
|
191 |
|
|
192 |
val document_files =
|
|
193 |
$$$(DOCUMENT_FILES) ~!
|
|
194 |
(($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
|
|
195 |
{ case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
|
|
196 |
rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
|
|
197 |
|
|
198 |
command(SESSION) ~!
|
|
199 |
(position(session_name) ~
|
|
200 |
(($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
|
|
201 |
(($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
|
|
202 |
($$$("=") ~!
|
|
203 |
(opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
|
|
204 |
(($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
|
|
205 |
(($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
|
|
206 |
rep1(theories) ~
|
|
207 |
(($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
|
|
208 |
(rep(document_files) ^^ (x => x.flatten))))) ^^
|
|
209 |
{ case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
|
|
210 |
Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
|
|
211 |
}
|
|
212 |
|
|
213 |
def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
|
|
214 |
{
|
|
215 |
def make_info(entry_chapter: String, entry: Session_Entry): (String, Info) =
|
|
216 |
{
|
|
217 |
try {
|
|
218 |
val name = entry.name
|
|
219 |
|
|
220 |
if (name == "") error("Bad session name")
|
|
221 |
if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
|
|
222 |
if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
|
|
223 |
|
|
224 |
val session_options = options ++ entry.options
|
|
225 |
|
|
226 |
val theories =
|
|
227 |
entry.theories.map({ case (global, opts, thys) =>
|
|
228 |
(global, session_options ++ opts, thys.map(Path.explode(_))) })
|
|
229 |
val files = entry.files.map(Path.explode(_))
|
|
230 |
val document_files =
|
|
231 |
entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
|
|
232 |
|
|
233 |
val meta_digest =
|
|
234 |
SHA1.digest((entry_chapter, name, entry.parent, entry.options,
|
|
235 |
entry.theories, entry.files, entry.document_files).toString)
|
|
236 |
|
|
237 |
val info =
|
|
238 |
Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
|
|
239 |
entry.parent, entry.description, session_options, theories, files,
|
|
240 |
document_files, meta_digest)
|
|
241 |
|
|
242 |
(name, info)
|
|
243 |
}
|
|
244 |
catch {
|
|
245 |
case ERROR(msg) =>
|
|
246 |
error(msg + "\nThe error(s) above occurred in session entry " +
|
|
247 |
quote(entry.name) + Position.here(entry.pos))
|
|
248 |
}
|
|
249 |
}
|
|
250 |
|
|
251 |
val root = dir + ROOT
|
|
252 |
if (root.is_file) {
|
|
253 |
val toks = Token.explode(root_syntax.keywords, File.read(root))
|
|
254 |
val start = Token.Pos.file(root.implode)
|
|
255 |
|
|
256 |
parse_all(rep(chapter | session_entry), Token.reader(toks, start)) match {
|
|
257 |
case Success(result, _) =>
|
|
258 |
var entry_chapter = "Unsorted"
|
|
259 |
val infos = new mutable.ListBuffer[(String, Info)]
|
|
260 |
result.foreach {
|
|
261 |
case Chapter(name) => entry_chapter = name
|
|
262 |
case entry: Session_Entry => infos += make_info(entry_chapter, entry)
|
|
263 |
}
|
|
264 |
infos.toList
|
|
265 |
case bad => error(bad.toString)
|
|
266 |
}
|
|
267 |
}
|
|
268 |
else Nil
|
|
269 |
}
|
|
270 |
}
|
|
271 |
|
|
272 |
|
|
273 |
/* find sessions within certain directories */
|
|
274 |
|
|
275 |
private def is_session_dir(dir: Path): Boolean =
|
|
276 |
(dir + ROOT).is_file || (dir + ROOTS).is_file
|
|
277 |
|
|
278 |
private def check_session_dir(dir: Path): Path =
|
|
279 |
if (is_session_dir(dir)) dir
|
|
280 |
else error("Bad session root directory: " + dir.toString)
|
|
281 |
|
|
282 |
def find(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): Tree =
|
|
283 |
{
|
|
284 |
def find_dir(select: Boolean, dir: Path): List[(String, Info)] =
|
|
285 |
find_root(select, dir) ::: find_roots(select, dir)
|
|
286 |
|
|
287 |
def find_root(select: Boolean, dir: Path): List[(String, Info)] =
|
|
288 |
Parser.parse(options, select, dir)
|
|
289 |
|
|
290 |
def find_roots(select: Boolean, dir: Path): List[(String, Info)] =
|
|
291 |
{
|
|
292 |
val roots = dir + ROOTS
|
|
293 |
if (roots.is_file) {
|
|
294 |
for {
|
|
295 |
line <- split_lines(File.read(roots))
|
|
296 |
if !(line == "" || line.startsWith("#"))
|
|
297 |
dir1 =
|
|
298 |
try { check_session_dir(dir + Path.explode(line)) }
|
|
299 |
catch {
|
|
300 |
case ERROR(msg) =>
|
|
301 |
error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
|
|
302 |
}
|
|
303 |
info <- find_dir(select, dir1)
|
|
304 |
} yield info
|
|
305 |
}
|
|
306 |
else Nil
|
|
307 |
}
|
|
308 |
|
|
309 |
val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
|
|
310 |
dirs.foreach(check_session_dir(_))
|
|
311 |
select_dirs.foreach(check_session_dir(_))
|
|
312 |
|
|
313 |
Tree(
|
|
314 |
for {
|
|
315 |
(select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
|
|
316 |
info <- find_dir(select, dir)
|
|
317 |
} yield info)
|
|
318 |
}
|
62632
|
319 |
|
|
320 |
|
|
321 |
/* persistent store */
|
|
322 |
|
|
323 |
def log(name: String): Path = Path.basic("log") + Path.basic(name)
|
|
324 |
def log_gz(name: String): Path = log(name).ext("gz")
|
|
325 |
|
|
326 |
def store(system_mode: Boolean = false): Store = new Store(system_mode)
|
|
327 |
|
|
328 |
class Store private [Sessions](system_mode: Boolean)
|
|
329 |
{
|
|
330 |
val output_dir: Path =
|
|
331 |
if (system_mode) Path.explode("~~/heaps/$ML_IDENTIFIER")
|
|
332 |
else Path.explode("$ISABELLE_OUTPUT")
|
|
333 |
|
|
334 |
val browser_info: Path =
|
|
335 |
if (system_mode) Path.explode("~~/browser_info")
|
|
336 |
else Path.explode("$ISABELLE_BROWSER_INFO")
|
|
337 |
|
|
338 |
private val input_dirs =
|
|
339 |
if (system_mode) List(output_dir)
|
|
340 |
else output_dir :: Isabelle_System.find_logics_dirs()
|
|
341 |
|
|
342 |
def find(name: String): Option[(Path, Path)] =
|
|
343 |
input_dirs.find(dir => (dir + log_gz(name)).is_file).map(dir =>
|
|
344 |
(dir + Path.basic(name), dir + log_gz(name)))
|
|
345 |
|
|
346 |
def find_log(name: String): Option[Path] = input_dirs.map(_ + log(name)).find(_.is_file)
|
|
347 |
def find_log_gz(name: String): Option[Path] = input_dirs.map(_ + log_gz(name)).find(_.is_file)
|
|
348 |
|
|
349 |
def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
|
|
350 |
}
|
62631
|
351 |
}
|