include COMPONENT/etc/sessions as catalog for more directories, for improved scalability with hundreds of entries (notably AFP);
misc tuning and simplification;
1 /* Title: Pure/System/build.scala
4 Build and manage Isabelle sessions.
12 import scala.collection.mutable
13 import scala.annotation.tailrec
18 /** session information **/
20 type Options = List[(String, Option[String])]
26 object Ordering extends scala.math.Ordering[Key]
28 def compare(key1: Key, key2: Key): Int =
29 key1.order compare key2.order match {
30 case 0 => key1.name compare key2.name
36 sealed case class Key(name: String, order: Int)
38 override def toString: String = name
41 sealed case class Info(
45 theories: List[(Options, String)],
50 val empty: Queue = new Queue()
53 final class Queue private(
54 keys: Map[String, Key] = Map.empty,
55 graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
57 def defined(name: String): Boolean = keys.isDefinedAt(name)
59 def + (key: Key, info: Info, parent: Option[String]): Queue =
62 if (defined(key.name)) error("Duplicate session: " + quote(key.name))
63 else keys + (key.name -> key)
67 graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
70 case exn: Graph.Cycles[_] =>
71 error(cat_lines(exn.cycles.map(cycle =>
72 "Cyclic session dependency of " +
73 cycle.map(key => quote(key.toString)).mkString(" via "))))
75 new Queue(keys1, graph1)
78 def topological_order: List[(Key, Info)] =
79 graph.topological_order.map(key => (key, graph.get_node(key)))
86 private case class Session_Entry(
91 parent: Option[String],
94 theories: List[(Options, List[String])],
97 private object Parser extends Parse.Parser
99 val SESSION = "session"
101 val DESCRIPTION = "description"
102 val OPTIONS = "options"
103 val THEORIES = "theories"
107 Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
108 SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
110 val session_entry: Parser[Session_Entry] =
112 val session_name = atom("session name", _.is_name)
113 val theory_name = atom("theory name", _.is_name)
116 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
117 val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
120 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
121 { case _ ~ (x ~ y) => (x, y) }
123 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
124 (keyword("!") ^^^ true | success(false)) ~
125 (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
126 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
127 (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
128 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
129 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
131 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
132 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
135 def parse_entries(root: File): List[Session_Entry] =
137 val toks = syntax.scan(Standard_System.read_file(root))
138 parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
139 case Success(result, _) => result
140 case bad => error(bad.toString)
148 private def sessions_root(dir: Path, root: File, sessions: Session.Queue): Session.Queue =
150 (sessions /: Parser.parse_entries(root))((sessions1, entry) =>
152 if (entry.name == "") error("Bad session name")
155 if (entry.name == "RAW" || entry.name == "Pure") {
156 if (entry.parent.isDefined) error("Illegal parent session")
161 case Some(parent_name) if sessions1.defined(parent_name) =>
162 if (entry.reset) entry.name
163 else parent_name + "-" + entry.name
164 case _ => error("Bad parent session")
169 case Some(p) => Path.explode(p)
170 case None => Path.basic(entry.name)
173 val key = Session.Key(full_name, entry.order)
174 val info = Session.Info(dir + path, entry.description, entry.options,
175 entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
177 sessions1 + (key, info, entry.parent)
181 error(msg + "\nThe error(s) above occurred in session entry " +
182 quote(entry.name) + " (file " + quote(root.toString) + ")")
186 private def sessions_dir(strict: Boolean, dir: Path, sessions: Session.Queue): Session.Queue =
188 val root = Isabelle_System.platform_file(dir + Path.basic("ROOT"))
189 if (root.isFile) sessions_root(dir, root, sessions)
190 else if (strict) error("Bad session root file: " + quote(root.toString))
194 private def sessions_catalog(dir: Path, catalog: File, sessions: Session.Queue): Session.Queue =
196 val dirs = split_lines(Standard_System.read_file(catalog)).filter(_ != "")
197 (sessions /: dirs)((sessions1, dir1) =>
199 val dir2 = dir + Path.explode(dir1)
200 if (Isabelle_System.platform_file(dir2).isDirectory) sessions_dir(true, dir2, sessions1)
201 else error("Bad session directory: " + dir2.toString)
205 error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
209 def find_sessions(more_dirs: List[Path]): Session.Queue =
211 var sessions = Session.Queue.empty
213 for (dir <- Isabelle_System.components()) {
214 sessions = sessions_dir(false, dir, sessions)
216 val catalog = Isabelle_System.platform_file(dir + Path.explode("etc/sessions"))
218 sessions = sessions_catalog(dir, catalog, sessions)
221 for (dir <- more_dirs) sessions = sessions_dir(true, dir, sessions)
230 def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
231 more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
233 println("more_dirs = " + more_dirs.toString)
234 println("options = " + options.toString)
235 println("sessions = " + sessions.toString)
237 for ((key, info) <- find_sessions(more_dirs).topological_order)
238 println(key.name + " in " + info.dir)
244 /* command line entry point */
246 def main(args: Array[String])
251 Properties.Value.Boolean(all_sessions) ::
252 Properties.Value.Boolean(build_images) ::
253 Properties.Value.Boolean(list_only) ::
254 Command_Line.Chunks(more_dirs, options, sessions) =>
255 build(all_sessions, build_images, list_only,
256 more_dirs.map(Path.explode), options, sessions)
257 case _ => error("Bad arguments:\n" + cat_lines(args))