wenzelm@49291: /*  Title:      Pure/System/build.scala
wenzelm@49291:     Author:     Makarius
wenzelm@49291: 
wenzelm@49291: Build and manage Isabelle sessions.
wenzelm@49291: */
wenzelm@49291: 
wenzelm@49291: package isabelle
wenzelm@49291: 
wenzelm@49291: 
wenzelm@49424: import java.io.{File => JFile}
wenzelm@49350: 
wenzelm@49352: import scala.collection.mutable
wenzelm@49355: import scala.annotation.tailrec
wenzelm@49352: 
wenzelm@49350: 
wenzelm@49291: object Build
wenzelm@49291: {
wenzelm@49352:   /** session information **/
wenzelm@49349: 
wenzelm@49364:   object Session
wenzelm@49364:   {
wenzelm@49436:     /* Key */
wenzelm@49436: 
wenzelm@49364:     object Key
wenzelm@49364:     {
wenzelm@49364:       object Ordering extends scala.math.Ordering[Key]
wenzelm@49364:       {
wenzelm@49364:         def compare(key1: Key, key2: Key): Int =
wenzelm@49365:           key1.order compare key2.order match {
wenzelm@49364:             case 0 => key1.name compare key2.name
wenzelm@49364:             case ord => ord
wenzelm@49364:           }
wenzelm@49364:       }
wenzelm@49364:     }
wenzelm@49364: 
wenzelm@49364:     sealed case class Key(name: String, order: Int)
wenzelm@49364:     {
wenzelm@49364:       override def toString: String = name
wenzelm@49364:     }
wenzelm@49364: 
wenzelm@49436: 
wenzelm@49436:     /* Info */
wenzelm@49436: 
wenzelm@49364:     sealed case class Info(
wenzelm@49364:       dir: Path,
wenzelm@49433:       parent: Option[String],
wenzelm@49364:       description: String,
wenzelm@49364:       options: Options,
wenzelm@49436:       theories: List[(Options, List[Path])],
wenzelm@49436:       files: List[Path],
wenzelm@49439:       digest: SHA1.Digest)
wenzelm@49436: 
wenzelm@49436: 
wenzelm@49436:     /* Queue */
wenzelm@49364: 
wenzelm@49364:     object Queue
wenzelm@49364:     {
wenzelm@49364:       val empty: Queue = new Queue()
wenzelm@49364:     }
wenzelm@49364: 
wenzelm@49364:     final class Queue private(
wenzelm@49364:       keys: Map[String, Key] = Map.empty,
wenzelm@49364:       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
wenzelm@49364:     {
wenzelm@49440:       def is_empty: Boolean = graph.is_empty
wenzelm@49440: 
wenzelm@49440:       def apply(name: String): Info = graph.get_node(keys(name))
wenzelm@49366:       def defined(name: String): Boolean = keys.isDefinedAt(name)
wenzelm@49434:       def is_inner(name: String): Boolean = !graph.is_maximal(keys(name))
wenzelm@49434: 
wenzelm@49433:       def + (key: Key, info: Info): Queue =
wenzelm@49364:       {
wenzelm@49364:         val keys1 =
wenzelm@49366:           if (defined(key.name)) error("Duplicate session: " + quote(key.name))
wenzelm@49366:           else keys + (key.name -> key)
wenzelm@49364: 
wenzelm@49364:         val graph1 =
wenzelm@49364:           try {
wenzelm@49433:             graph.new_node(key, info).add_deps_acyclic(key, info.parent.toList.map(keys(_)))
wenzelm@49364:           }
wenzelm@49364:           catch {
wenzelm@49364:             case exn: Graph.Cycles[_] =>
wenzelm@49364:               error(cat_lines(exn.cycles.map(cycle =>
wenzelm@49364:                 "Cyclic session dependency of " +
wenzelm@49364:                   cycle.map(key => quote(key.toString)).mkString(" via "))))
wenzelm@49364:           }
wenzelm@49364:         new Queue(keys1, graph1)
wenzelm@49364:       }
wenzelm@49364: 
wenzelm@49440:       def - (name: String): Queue = new Queue(keys - name, graph.del_node(keys(name)))
wenzelm@49440: 
wenzelm@49378:       def required(names: List[String]): Queue =
wenzelm@49378:       {
wenzelm@49378:         val req = graph.all_preds(names.map(keys(_))).map(_.name).toSet
wenzelm@49378:         val keys1 = keys -- keys.keySet.filter(name => !req(name))
wenzelm@49378:         val graph1 = graph.restrict(key => keys1.isDefinedAt(key.name))
wenzelm@49378:         new Queue(keys1, graph1)
wenzelm@49378:       }
wenzelm@49378: 
wenzelm@49440:       def dequeue(skip: String => Boolean): Option[(String, Info)] =
wenzelm@49440:       {
wenzelm@49440:         val it = graph.entries.dropWhile(
wenzelm@49440:           { case (key, (_, (deps, _))) => !deps.isEmpty || skip(key.name) })
wenzelm@49440:         if (it.hasNext) { val (key, (info, _)) = it.next; Some((key.name, info)) }
wenzelm@49440:         else None
wenzelm@49440:       }
wenzelm@49440: 
wenzelm@49437:       def topological_order: List[(String, Info)] =
wenzelm@49437:         graph.topological_order.map(key => (key.name, graph.get_node(key)))
wenzelm@49364:     }
wenzelm@49364:   }
wenzelm@49295: 
wenzelm@49352: 
wenzelm@49352:   /* parsing */
wenzelm@49352: 
wenzelm@49352:   private case class Session_Entry(
wenzelm@49352:     name: String,
wenzelm@49352:     reset: Boolean,
wenzelm@49364:     order: Int,
wenzelm@49352:     path: Option[String],
wenzelm@49362:     parent: Option[String],
wenzelm@49352:     description: String,
wenzelm@49436:     options: List[Options.Spec],
wenzelm@49436:     theories: List[(List[Options.Spec], List[String])],
wenzelm@49352:     files: List[String])
wenzelm@49352: 
wenzelm@49349:   private object Parser extends Parse.Parser
wenzelm@49349:   {
wenzelm@49349:     val SESSION = "session"
wenzelm@49349:     val IN = "in"
wenzelm@49349:     val DESCRIPTION = "description"
wenzelm@49349:     val OPTIONS = "options"
wenzelm@49349:     val THEORIES = "theories"
wenzelm@49349:     val FILES = "files"
wenzelm@49349: 
wenzelm@49349:     val syntax =
wenzelm@49351:       Outer_Syntax.empty + "!" + "(" + ")" + "+" + "," + "=" + "[" + "]" +
wenzelm@49351:         SESSION + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
wenzelm@49349: 
wenzelm@49352:     val session_entry: Parser[Session_Entry] =
wenzelm@49349:     {
wenzelm@49349:       val session_name = atom("session name", _.is_name)
wenzelm@49349:       val theory_name = atom("theory name", _.is_name)
wenzelm@49349: 
wenzelm@49349:       val option =
wenzelm@49349:         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
wenzelm@49352:       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
wenzelm@49349: 
wenzelm@49349:       val theories =
wenzelm@49349:         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep1(theory_name)) ^^
wenzelm@49349:           { case _ ~ (x ~ y) => (x, y) }
wenzelm@49349: 
wenzelm@49349:       ((keyword(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
wenzelm@49351:         (keyword("!") ^^^ true | success(false)) ~
wenzelm@49364:         (keyword("(") ~! (nat <~ keyword(")")) ^^ { case _ ~ x => x } | success(Integer.MAX_VALUE)) ~
wenzelm@49352:         (opt(keyword(IN) ~! string ^^ { case _ ~ x => x })) ~
wenzelm@49362:         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
wenzelm@49349:         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
wenzelm@49349:         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
wenzelm@49362:         rep(theories) ~
wenzelm@49351:         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
wenzelm@49364:           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h ~ i => Session_Entry(a, b, c, d, e, f, g, h, i) }
wenzelm@49349:     }
wenzelm@49349: 
wenzelm@49424:     def parse_entries(root: JFile): List[Session_Entry] =
wenzelm@49349:     {
wenzelm@49426:       val toks = syntax.scan(File.read(root))
wenzelm@49352:       parse_all(rep(session_entry), Token.reader(toks, root.toString)) match {
wenzelm@49349:         case Success(result, _) => result
wenzelm@49349:         case bad => error(bad.toString)
wenzelm@49349:       }
wenzelm@49349:     }
wenzelm@49349:   }
wenzelm@49295: 
wenzelm@49352: 
wenzelm@49356:   /* find sessions */
wenzelm@49352: 
wenzelm@49376:   private val ROOT = Path.explode("ROOT")
wenzelm@49376:   private val SESSIONS = Path.explode("etc/sessions")
wenzelm@49376: 
wenzelm@49379:   private def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
wenzelm@49379: 
wenzelm@49436:   private def sessions_root(options: Options, dir: Path, root: JFile, queue: Session.Queue)
wenzelm@49436:     : Session.Queue =
wenzelm@49295:   {
wenzelm@49376:     (queue /: Parser.parse_entries(root))((queue1, entry) =>
wenzelm@49352:       try {
wenzelm@49362:         if (entry.name == "") error("Bad session name")
wenzelm@49362: 
wenzelm@49352:         val full_name =
wenzelm@49379:           if (is_pure(entry.name)) {
wenzelm@49362:             if (entry.parent.isDefined) error("Illegal parent session")
wenzelm@49362:             else entry.name
wenzelm@49362:           }
wenzelm@49362:           else
wenzelm@49362:             entry.parent match {
wenzelm@49376:               case Some(parent_name) if queue1.defined(parent_name) =>
wenzelm@49362:                 if (entry.reset) entry.name
wenzelm@49366:                 else parent_name + "-" + entry.name
wenzelm@49366:               case _ => error("Bad parent session")
wenzelm@49362:             }
wenzelm@49354: 
wenzelm@49352:         val path =
wenzelm@49352:           entry.path match {
wenzelm@49352:             case Some(p) => Path.explode(p)
wenzelm@49352:             case None => Path.basic(entry.name)
wenzelm@49352:           }
wenzelm@49354: 
wenzelm@49366:         val key = Session.Key(full_name, entry.order)
wenzelm@49436: 
wenzelm@49436:         val theories =
wenzelm@49436:           entry.theories.map({ case (opts, thys) => (options ++ opts, thys.map(Path.explode(_))) })
wenzelm@49436:         val files = entry.files.map(Path.explode(_))
wenzelm@49438:         val digest = SHA1.digest((full_name, entry.parent, entry.options, entry.theories).toString)
wenzelm@49438: 
wenzelm@49433:         val info =
wenzelm@49433:           Session.Info(dir + path, entry.parent,
wenzelm@49438:             entry.description, options ++ entry.options, theories, files, digest)
wenzelm@49366: 
wenzelm@49433:         queue1 + (key, info)
wenzelm@49352:       }
wenzelm@49352:       catch {
wenzelm@49352:         case ERROR(msg) =>
wenzelm@49352:           error(msg + "\nThe error(s) above occurred in session entry " +
wenzelm@49385:             quote(entry.name) + Position.str_of(Position.file(root)))
wenzelm@49367:       })
wenzelm@49367:   }
wenzelm@49367: 
wenzelm@49436:   private def sessions_dir(options: Options, strict: Boolean, dir: Path, queue: Session.Queue)
wenzelm@49436:     : Session.Queue =
wenzelm@49367:   {
wenzelm@49388:     val root = (dir + ROOT).file
wenzelm@49436:     if (root.isFile) sessions_root(options, dir, root, queue)
wenzelm@49367:     else if (strict) error("Bad session root file: " + quote(root.toString))
wenzelm@49376:     else queue
wenzelm@49367:   }
wenzelm@49367: 
wenzelm@49436:   private def sessions_catalog(options: Options, dir: Path, catalog: JFile, queue: Session.Queue)
wenzelm@49436:     : Session.Queue =
wenzelm@49367:   {
wenzelm@49369:     val dirs =
wenzelm@49426:       split_lines(File.read(catalog)).filterNot(line => line == "" || line.startsWith("#"))
wenzelm@49376:     (queue /: dirs)((queue1, dir1) =>
wenzelm@49367:       try {
wenzelm@49367:         val dir2 = dir + Path.explode(dir1)
wenzelm@49436:         if (dir2.file.isDirectory) sessions_dir(options, true, dir2, queue1)
wenzelm@49367:         else error("Bad session directory: " + dir2.toString)
wenzelm@49352:       }
wenzelm@49367:       catch {
wenzelm@49367:         case ERROR(msg) =>
wenzelm@49367:           error(msg + "\nThe error(s) above occurred in session catalog " + quote(catalog.toString))
wenzelm@49367:       })
wenzelm@49367:   }
wenzelm@49367: 
wenzelm@49436:   def find_sessions(options: Options, all_sessions: Boolean, sessions: List[String],
wenzelm@49434:     more_dirs: List[Path]): Session.Queue =
wenzelm@49367:   {
wenzelm@49376:     var queue = Session.Queue.empty
wenzelm@49367: 
wenzelm@49367:     for (dir <- Isabelle_System.components()) {
wenzelm@49436:       queue = sessions_dir(options, false, dir, queue)
wenzelm@49367: 
wenzelm@49388:       val catalog = (dir + SESSIONS).file
wenzelm@49367:       if (catalog.isFile)
wenzelm@49436:         queue = sessions_catalog(options, dir, catalog, queue)
wenzelm@49352:     }
wenzelm@49367: 
wenzelm@49436:     for (dir <- more_dirs) queue = sessions_dir(options, true, dir, queue)
wenzelm@49367: 
wenzelm@49434:     sessions.filter(name => !queue.defined(name)) match {
wenzelm@49434:       case Nil =>
wenzelm@49434:       case bad => error("Undefined session(s): " + commas_quote(bad))
wenzelm@49434:     }
wenzelm@49434: 
wenzelm@49434:     if (all_sessions) queue else queue.required(sessions)
wenzelm@49295:   }
wenzelm@49356: 
wenzelm@49356: 
wenzelm@49439: 
wenzelm@49439:   /** build **/
wenzelm@49439: 
wenzelm@49437:   /* dependencies */
wenzelm@49437: 
wenzelm@49437:   sealed case class Node(
wenzelm@49437:     loaded_theories: Set[String],
wenzelm@49438:     sources: List[(Path, SHA1.Digest)])
wenzelm@49437: 
wenzelm@49438:   sealed case class Deps(deps: Map[String, Node])
wenzelm@49438:   {
wenzelm@49438:     def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
wenzelm@49438:   }
wenzelm@49438: 
wenzelm@49438:   def dependencies(queue: Session.Queue): Deps =
wenzelm@49438:     Deps((Map.empty[String, Node] /: queue.topological_order)(
wenzelm@49437:       { case (deps, (name, info)) =>
wenzelm@49437:           val preloaded =
wenzelm@49437:             info.parent match {
wenzelm@49437:               case None => Set.empty[String]
wenzelm@49437:               case Some(parent) => deps(parent).loaded_theories
wenzelm@49437:             }
wenzelm@49437:           val thy_info = new Thy_Info(new Thy_Load(preloaded))
wenzelm@49437: 
wenzelm@49437:           val thy_deps =
wenzelm@49437:             thy_info.dependencies(
wenzelm@49437:               info.theories.map(_._2).flatten.
wenzelm@49437:                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
wenzelm@49437: 
wenzelm@49437:           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
wenzelm@49438: 
wenzelm@49438:           val all_files =
wenzelm@49437:             thy_deps.map({ case (n, h) =>
wenzelm@49437:               val thy = Path.explode(n.node).expand
wenzelm@49437:               val uses =
wenzelm@49437:                 h match {
wenzelm@49437:                   case Exn.Res(d) =>
wenzelm@49437:                     d.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
wenzelm@49437:                   case _ => Nil
wenzelm@49437:                 }
wenzelm@49437:               thy :: uses
wenzelm@49437:             }).flatten ::: info.files.map(file => info.dir + file)
wenzelm@49438:           val sources = all_files.par.map(p => (p, SHA1.digest(p))).toList
wenzelm@49437: 
wenzelm@49437:           deps + (name -> Node(loaded_theories, sources))
wenzelm@49438:       }))
wenzelm@49437: 
wenzelm@49437: 
wenzelm@49439:   /* jobs */
wenzelm@49356: 
wenzelm@49439:   private class Job(cwd: JFile, env: Map[String, String], script: String, args: String)
wenzelm@49379:   {
wenzelm@49433:     private val args_file = File.tmp_file("args")
wenzelm@49433:     private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
wenzelm@49433:     File.write(args_file, args)
wenzelm@49433: 
wenzelm@49439:     private val (thread, result) =
wenzelm@49439:       Simple_Thread.future("build") { Isabelle_System.bash_env(cwd, env1, script) }
wenzelm@49433: 
wenzelm@49433:     def terminate: Unit = thread.interrupt
wenzelm@49433:     def is_finished: Boolean = result.is_finished
wenzelm@49440:     def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
wenzelm@49433:   }
wenzelm@49433: 
wenzelm@49439:   private def start_job(save: Boolean, name: String, info: Session.Info): Job =
wenzelm@49433:   {
wenzelm@49433:     val parent = info.parent.getOrElse("")
wenzelm@49433: 
wenzelm@49388:     val cwd = info.dir.file
wenzelm@49433:     val env = Map("INPUT" -> parent, "TARGET" -> name)
wenzelm@49379:     val script =
wenzelm@49434:       if (is_pure(name)) "./build " + (if (save) "-b " else "") + name
wenzelm@49433:       else {
wenzelm@49433:         """
wenzelm@49433:         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
wenzelm@49433:         """ +
wenzelm@49434:           (if (save)
wenzelm@49433:             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$TARGET" """
wenzelm@49433:           else
wenzelm@49433:             """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
wenzelm@49433:         """
wenzelm@49433:         RC="$?"
wenzelm@49433: 
wenzelm@49433:         . "$ISABELLE_HOME/lib/scripts/timestop.bash"
wenzelm@49433: 
wenzelm@49433:         if [ "$RC" -eq 0 ]; then
wenzelm@49433:           echo "Finished $TARGET ($TIMES_REPORT)" >&2
wenzelm@49433:         fi
wenzelm@49433: 
wenzelm@49433:         exit "$RC"
wenzelm@49433:         """
wenzelm@49433:       }
wenzelm@49433:     val args_xml =
wenzelm@49433:     {
wenzelm@49433:       import XML.Encode._
wenzelm@49436:       pair(bool, pair(string, pair(string, list(string))))(
wenzelm@49436:         save, (parent, (name, info.theories.map(_._2).flatten.map(_.implode))))
wenzelm@49433:     }
wenzelm@49439:     new Job(cwd, env, script, YXML.string_of_body(args_xml))
wenzelm@49379:   }
wenzelm@49379: 
wenzelm@49439: 
wenzelm@49440:   /* build */
wenzelm@49439: 
wenzelm@49439:   private def echo(msg: String) { java.lang.System.out.println(msg) }
wenzelm@49440:   private def sleep(): Unit = Thread.sleep(500)
wenzelm@49439: 
wenzelm@49440:   def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
wenzelm@49440:     list_only: Boolean, verbose: Boolean,
wenzelm@49434:     more_dirs: List[Path], more_options: List[String], sessions: List[String]): Int =
wenzelm@49356:   {
wenzelm@49434:     val options = (Options.init() /: more_options)(_.define_simple(_))
wenzelm@49436:     val queue = find_sessions(options, all_sessions, sessions, more_dirs)
wenzelm@49438:     val deps = dependencies(queue)
wenzelm@49383: 
wenzelm@49378: 
wenzelm@49388:     // prepare browser info dir
wenzelm@49434:     if (options.bool("browser_info") &&
wenzelm@49388:       !Path.explode("$ISABELLE_BROWSER_INFO/index.html").file.isFile)
wenzelm@49388:     {
wenzelm@49388:       Path.explode("$ISABELLE_BROWSER_INFO").file.mkdirs()
wenzelm@49426:       File.copy(Path.explode("$ISABELLE_HOME/lib/logo/isabelle.gif"),
wenzelm@49426:         Path.explode("$ISABELLE_BROWSER_INFO/isabelle.gif"))
wenzelm@49426:       File.write(Path.explode("$ISABELLE_BROWSER_INFO/index.html"),
wenzelm@49426:         File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_header.template")) +
wenzelm@49426:         File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_content.template")) +
wenzelm@49426:         File.read(Path.explode("$ISABELLE_HOME/lib/html/library_index_footer.template")))
wenzelm@49379:     }
wenzelm@49356: 
wenzelm@49388:     // prepare log dir
wenzelm@49388:     val log_dir = Path.explode("$ISABELLE_OUTPUT/log")
wenzelm@49388:     log_dir.file.mkdirs()
wenzelm@49388: 
wenzelm@49440:     // scheduler loop
wenzelm@49440:     @tailrec def loop(
wenzelm@49440:       pending: Session.Queue,
wenzelm@49440:       running: Map[String, Job],
wenzelm@49440:       results: Map[String, Int]): Map[String, Int] =
wenzelm@49440:     {
wenzelm@49440:       if (pending.is_empty) results
wenzelm@49440:       else if (running.exists({ case (_, job) => job.is_finished })) {
wenzelm@49440:         val (name, job) = running.find({ case (_, job) => job.is_finished }).get
wenzelm@49439: 
wenzelm@49440:         val (out, err, rc) = job.join
wenzelm@49440:         echo(Library.trim_line(err))
wenzelm@49440: 
wenzelm@49440:         val log = log_dir + Path.basic(name)
wenzelm@49440:         if (rc == 0) {
wenzelm@49440:           val sources =
wenzelm@49440:             (queue(name).digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
wenzelm@49440:               .mkString("sources: ", " ", "\n")
wenzelm@49440:           File.write_zip(log.ext("gz"), sources + out)
wenzelm@49440:         }
wenzelm@49388:         else {
wenzelm@49440:           File.write(log, out)
wenzelm@49440:           echo(name + " FAILED")
wenzelm@49440:           echo("(see also " + log.file + ")")
wenzelm@49440:           val lines = split_lines(out)
wenzelm@49440:           val tail = lines.drop(lines.length - 20 max 0)
wenzelm@49440:           echo("\n" + cat_lines(tail))
wenzelm@49440:         }
wenzelm@49440:         loop(pending - name, running - name, results + (name -> rc))
wenzelm@49440:       }
wenzelm@49440:       else if (running.size < (max_jobs max 1)) {
wenzelm@49440:         pending.dequeue(running.isDefinedAt(_)) match {
wenzelm@49440:           case Some((name, info)) =>
wenzelm@49440:             if (list_only) {
wenzelm@49440:               echo(name + " in " + info.dir)
wenzelm@49440:               loop(pending - name, running, results + (name -> 0))
wenzelm@49440:             }
wenzelm@49440:             else if (info.parent.map(results(_)).forall(_ == 0)) {
wenzelm@49440:               val save = build_images || queue.is_inner(name)
wenzelm@49440:               echo((if (save) "Building " else "Running ") + name + " ...")
wenzelm@49440:               val job = start_job(save, name, info)
wenzelm@49440:               loop(pending, running + (name -> job), results)
wenzelm@49440:             }
wenzelm@49440:             else {
wenzelm@49440:               echo(name + " CANCELLED")
wenzelm@49440:               loop(pending - name, running, results + (name -> 1))
wenzelm@49440:             }
wenzelm@49440:           case None => sleep(); loop(pending, running, results)
wenzelm@49388:         }
wenzelm@49388:       }
wenzelm@49440:       else { sleep(); loop(pending, running, results) }
wenzelm@49440:     }
wenzelm@49440: 
wenzelm@49440:     (0 /: loop(queue, Map.empty, Map.empty))({ case (rc1, (_, rc2)) => rc1 max rc2 })
wenzelm@49356:   }
wenzelm@49356: 
wenzelm@49356: 
wenzelm@49361:   /* command line entry point */
wenzelm@49356: 
wenzelm@49356:   def main(args: Array[String])
wenzelm@49356:   {
wenzelm@49361:     Command_Line.tool {
wenzelm@49361:       args.toList match {
wenzelm@49361:         case
wenzelm@49361:           Properties.Value.Boolean(all_sessions) ::
wenzelm@49361:           Properties.Value.Boolean(build_images) ::
wenzelm@49440:           Properties.Value.Int(max_jobs) ::
wenzelm@49361:           Properties.Value.Boolean(list_only) ::
wenzelm@49440:           Properties.Value.Boolean(verbose) ::
wenzelm@49361:           Command_Line.Chunks(more_dirs, options, sessions) =>
wenzelm@49440:             build(all_sessions, build_images, max_jobs, list_only, verbose,
wenzelm@49361:               more_dirs.map(Path.explode), options, sessions)
wenzelm@49361:         case _ => error("Bad arguments:\n" + cat_lines(args))
wenzelm@49356:       }
wenzelm@49361:     }
wenzelm@49356:   }
wenzelm@49291: }
wenzelm@49291: