clarified no_build vs. verbose;
1 /* Title: Pure/System/build.scala
4 Build and manage Isabelle sessions.
10 import java.io.{File => JFile}
12 import scala.collection.mutable
13 import scala.annotation.tailrec
18 /** session information **/
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
44 sealed case class Info(
47 parent: Option[String],
50 theories: List[(Options, List[Path])],
59 val empty: Queue = new Queue()
62 final class Queue private(
63 keys: Map[String, Key] = Map.empty,
64 graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
66 def is_empty: Boolean = graph.is_empty
68 def apply(name: String): Info = graph.get_node(keys(name))
69 def defined(name: String): Boolean = keys.isDefinedAt(name)
70 def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
72 def + (key: Key, info: Info): Queue =
75 if (defined(key.name)) error("Duplicate session: " + quote(key.name))
76 else keys + (key.name -> key)
80 graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_)))
83 case exn: Graph.Cycles[_] =>
84 error(cat_lines(exn.cycles.map(cycle =>
85 "Cyclic session dependency of " +
86 cycle.map(key => quote(key.toString)).mkString(" via "))))
88 new Queue(keys1, graph1)
91 def - (name: String): Queue = new Queue(keys - name, graph.del_node(keys(name)))
93 def required(names: List[String]): Queue =
95 val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
96 val keys1 = keys -- keys.keySet.filter(name => !req(name))
97 val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
98 new Queue(keys1, graph1)
101 def dequeue(skip: String => Boolean): Option[(String, Info)] =
103 val it = graph.entries.dropWhile(
104 { case (key, (_, (deps, _))) => !deps.isEmpty || skip(key.name) })
105 if (it.hasNext) { val (key, (info, _)) = it.next; Some((key.name, info)) }
109 def topological_order: List[(String, Info)] =
110 graph.topological_order.map(key => (key.name, graph.get_node(key)))
117 private case class Session_Entry(
121 path: Option[String],
122 parent: Option[String],
124 options: List[Options.Spec],
125 theories: List[(List[Options.Spec], List[String])],
128 private object Parser extends Parse.Parser
130 val SESSION = "session"
132 val DESCRIPTION = "description"
133 val OPTIONS = "options"
134 val THEORIES = "theories"
138 Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
139 SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
141 val session_entry: Parser[Session_Entry] =
143 val session_name = atom("session name", _.is_name)
144 val theory_name = atom("theory name", _.is_name)
147 name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
148 val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
151 keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
152 { case _ ~ (x ~ y) => (x, y) }
154 ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
155 (keyword("!") ^^^ true | success(false)) ~
156 (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
157 (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
158 (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
159 (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
160 (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
162 (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
163 { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
166 def parse_entries(root: JFile): List[Session_Entry] =
168 val toks = syntax.scan(File.read(root))
169 parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
170 case Success(result, _) => result
171 case bad => error(bad.toString)
179 private val ROOT = Path.explode("ROOT")
180 private val SESSIONS = Path.explode("etc/sessions")
182 private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
184 private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
187 (queue /: Parser.parse_entries(root))((queue1, entry) =>
189 if (entry.name == "") error("Bad session name")
192 if (is_pure(entry.name)) {
193 if (entry.parent.isDefined) error("Illegal parent session")
198 case Some(parent_name) if queue1.defined(parent_name) =>
199 if (entry.this_name) entry.name
200 else parent_name + "-" + entry.name
201 case _ => error("Bad parent session")
206 case Some(p) => Path.explode(p)
207 case None => Path.basic(entry.name)
210 val key = Session.Key(full_name, entry.order)
212 val session_options = options ++ entry.options
215 entry.theories.map({ case (opts, thys) =>
216 (session_options ++ opts, thys.map(Path.explode(_))) })
217 val files = entry.files.map(Path.explode(_))
218 val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
221 Session.Info(entry.name, dir + path, entry.parent,
222 entry.description, session_options, theories, files, digest)
228 error(msg + "\nThe error(s) above occurred in session entry " +
229 quote(entry.name) + Position.str_of(Position.file(root)))
233 private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
236 val root = (dir + ROOT).file
237 if (root.isFile) sessions_root(options, dir, root, queue)
238 else if (strict) error("Bad session root file: " + quote(root.toString))
242 private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
246 split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
247 (queue /: dirs)((queue1, dir1) =>
249 val dir2 = dir + Path.explode(dir1)
250 if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
251 else error("Bad session directory: " + dir2.toString)
255 error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
259 def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
260 more_dirs: List[Path]): Session.Queue =
262 var queue = Session.Queue.empty
264 for (dir <- Isabelle_System.components()) {
265 queue = sessions_dir(options, false, dir, queue)
267 val catalog = (dir + SESSIONS).file
269 queue = sessions_catalog(options, dir, catalog, queue)
272 for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
274 sessions.filter(name => !queue.defined(name)) match {
276 case bad => error("Undefined session(s): " + commas_quote(bad))
279 if (all_sessions) queue else queue.required(sessions)
288 sealed case class Node(
289 loaded_theories: Set[String],
290 sources: List[(Path, SHA1.Digest)])
292 sealed case class Deps(deps: Map[String, Node])
294 def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
297 def dependencies(queue: Session.Queue): Deps =
298 Deps((Map.empty[String, Node] /: queue.topological_order)(
299 { case (deps, (name, info)) =>
302 case None => Set.empty[String]
303 case Some(parent) => deps(parent).loaded_theories
305 val thy_info = new Thy_Info(new Thy_Load(preloaded))
308 thy_info.dependencies(
309 info.theories.map(_._2).flatten.
310 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
312 val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
315 thy_deps.map({ case (n, h) =>
316 val thy = Path.explode(n.node).expand
320 d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
324 }).flatten ::: info.files.map(file => info.dir + file)
325 val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList
327 deps + (name -> Node(loaded_theories, sources))
333 private class Job(cwd: JFile, env: Map[String, String], script: String, args: String)
335 private val args_file = File.tmp_file("args")
336 private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
337 File.write(args_file, args)
339 private val (thread, result) =
340 Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
342 def terminate: Unit = thread.interrupt
343 def is_finished: Boolean = result.is_finished
344 def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
347 private def start_job(name: String, info: Session.Info, output: Option[String],
348 options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
350 // global browser info dir
351 if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).file.isFile)
353 browser_info.file.mkdirs()
354 File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
355 browser_info + Path.explode("isabelle.gif"))
356 File.write(browser_info + Path.explode("index.html"),
357 File.read(Path.explode("~~/lib/html/library_index_header.template")) +
358 File.read(Path.explode("~~/lib/html/library_index_content.template")) +
359 File.read(Path.explode("~~/lib/html/library_index_footer.template")))
362 val parent = info.parent.getOrElse("")
364 val cwd = info.dir.file
365 val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
367 if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
370 . "$ISABELLE_HOME/lib/scripts/timestart.bash"
372 (if (output.isDefined)
373 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
375 """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
379 . "$ISABELLE_HOME/lib/scripts/timestop.bash"
381 if [ "$RC" -eq 0 ]; then
382 echo "Finished $TARGET ($TIMES_REPORT)" >&2
391 pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
392 pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
393 (output.isDefined, (options, (timing, (verbose, (browser_info, (parent,
394 (name, (info.base_name, info.theories)))))))))
396 new Job(cwd, env, script, YXML.string_of_body(args_xml))
402 private def echo(msg: String) { java.lang.System.out.println(msg) }
403 private def sleep(): Unit = Thread.sleep(500)
405 def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
406 no_build: Boolean, system_mode: Boolean, timing: Boolean, verbose: Boolean,
407 more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
409 val options = (Options.init() /: more_options)(_.define_simple(_))
410 val queue = find_sessions(options, all_sessions, sessions, more_dirs)
411 val deps = dependencies(queue)
413 val (output_dir, browser_info) =
414 if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
415 else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
418 val log_dir = output_dir + Path.explode("log")
419 log_dir.file.mkdirs()
423 pending: Session.Queue,
424 running: Map[String, Job],
425 results: Map[String, Int]): Map[String, Int] =
427 if (pending.is_empty) results
428 else if (running.exists({ case (_, job) => job.is_finished })) {
429 val (name, job) = running.find({ case (_, job) => job.is_finished }).get
431 val (out, err, rc) = job.join
432 echo(Library.trim_line(err))
434 val log = log_dir + Path.basic(name)
437 (queue(name).digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
438 .mkString("sources: ", " ", "\n")
439 File.write_zip(log.ext("gz"), sources + out)
443 echo(name + " FAILED")
444 echo("(see also " + log.file + ")")
445 val lines = split_lines(out)
446 val tail = lines.drop(lines.length - 20 max 0)
447 echo("\n" + cat_lines(tail))
449 loop(pending - name, running - name, results + (name -> rc))
451 else if (running.size < (max_jobs max 1)) {
452 pending.dequeue(running.isDefinedAt(_)) match {
453 case Some((name, info)) =>
455 if (verbose) echo(name + " in " + info.dir)
456 loop(pending - name, running, results + (name -> 0))
458 else if (info.parent.map(results(_)).forall(_ == 0)) {
460 if (build_images || queue.is_inner(name))
461 Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
463 echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
464 val job = start_job(name, info, output, info.options, timing, verbose, browser_info)
465 loop(pending, running + (name -> job), results)
468 echo(name + " CANCELLED")
469 loop(pending - name, running, results + (name -> 1))
471 case None => sleep(); loop(pending, running, results)
474 else { sleep(); loop(pending, running, results) }
477 (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 })
481 /* command line entry point */
483 def main(args: Array[String])
488 Properties.Value.Boolean(all_sessions) ::
489 Properties.Value.Boolean(build_images) ::
490 Properties.Value.Int(max_jobs) ::
491 Properties.Value.Boolean(no_build) ::
492 Properties.Value.Boolean(system_mode) ::
493 Properties.Value.Boolean(timing) ::
494 Properties.Value.Boolean(verbose) ::
495 Command_Line.Chunks(more_dirs, options, sessions) =>
496 build(all_sessions, build_images, max_jobs, no_build, system_mode, timing,
497 verbose, more_dirs.map(Path.explode), options, sessions)
498 case _ => error("Bad arguments:\n" + cat_lines(args))