src/Pure/System/build.scala
author wenzelm
Tue Aug 14 11:37:58 2012 +0200 (2012-08-14)
changeset 48791 9e8f30bfbdca
parent 48739 3a6c03b15916
child 48794 8d2a026e576b
permissions -rw-r--r--
added jedit option -d;
     1 /*  Title:      Pure/System/build.scala
     2     Author:     Makarius
     3 
     4 Build and manage Isabelle sessions.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.util.{Timer, TimerTask}
    11 import java.io.{BufferedInputStream, FileInputStream,
    12   BufferedReader, InputStreamReader, IOException}
    13 import java.util.zip.GZIPInputStream
    14 
    15 import scala.collection.SortedSet
    16 import scala.annotation.tailrec
    17 
    18 
    19 object Build
    20 {
    21   /** session information **/
    22 
    23   // external version
    24   sealed case class Session_Entry(
    25     pos: Position.T,
    26     name: String,
    27     groups: List[String],
    28     path: String,
    29     parent: Option[String],
    30     description: String,
    31     options: List[Options.Spec],
    32     theories: List[(List[Options.Spec], List[String])],
    33     files: List[String])
    34 
    35   // internal version
    36   sealed case class Session_Info(
    37     select: Boolean,
    38     pos: Position.T,
    39     groups: List[String],
    40     dir: Path,
    41     parent: Option[String],
    42     description: String,
    43     options: Options,
    44     theories: List[(Options, List[Path])],
    45     files: List[Path],
    46     entry_digest: SHA1.Digest)
    47 
    48   def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    49 
    50   def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
    51       : (String, Session_Info) =
    52     try {
    53       val name = entry.name
    54 
    55       if (name == "") error("Bad session name")
    56       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    57       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    58 
    59       val session_options = options ++ entry.options
    60 
    61       val theories =
    62         entry.theories.map({ case (opts, thys) =>
    63           (session_options ++ opts, thys.map(Path.explode(_))) })
    64       val files = entry.files.map(Path.explode(_))
    65       val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
    66 
    67       val info =
    68         Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
    69           entry.parent, entry.description, session_options, theories, files, entry_digest)
    70 
    71       (name, info)
    72     }
    73     catch {
    74       case ERROR(msg) =>
    75         error(msg + "\nThe error(s) above occurred in session entry " +
    76           quote(entry.name) + Position.str_of(entry.pos))
    77     }
    78 
    79 
    80   /* session tree */
    81 
    82   object Session_Tree
    83   {
    84     def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
    85     {
    86       val graph1 =
    87         (Graph.string[Session_Info] /: infos) {
    88           case (graph, (name, info)) =>
    89             if (graph.defined(name))
    90               error("Duplicate session " + quote(name) + Position.str_of(info.pos))
    91             else graph.new_node(name, info)
    92         }
    93       val graph2 =
    94         (graph1 /: graph1.entries) {
    95           case (graph, (name, (info, _))) =>
    96             info.parent match {
    97               case None => graph
    98               case Some(parent) =>
    99                 if (!graph.defined(parent))
   100                   error("Bad parent session " + quote(parent) + " for " +
   101                     quote(name) + Position.str_of(info.pos))
   102 
   103                 try { graph.add_edge_acyclic(parent, name) }
   104                 catch {
   105                   case exn: Graph.Cycles[_] =>
   106                     error(cat_lines(exn.cycles.map(cycle =>
   107                       "Cyclic session dependency of " +
   108                         cycle.map(c => quote(c.toString)).mkString(" via "))) +
   109                           Position.str_of(info.pos))
   110                 }
   111             }
   112         }
   113       new Session_Tree(graph2)
   114     }
   115   }
   116 
   117   final class Session_Tree private(val graph: Graph[String, Session_Info])
   118     extends PartialFunction[String, Session_Info]
   119   {
   120     def apply(name: String): Session_Info = graph.get_node(name)
   121     def isDefinedAt(name: String): Boolean = graph.defined(name)
   122 
   123     def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
   124       : (List[String], Session_Tree) =
   125     {
   126       val bad_sessions = sessions.filterNot(isDefinedAt(_))
   127       if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
   128 
   129       val selected =
   130       {
   131         if (all_sessions) graph.keys.toList
   132         else {
   133           val select_group = session_groups.toSet
   134           val select = sessions.toSet
   135           (for {
   136             (name, (info, _)) <- graph.entries
   137             if info.select || select(name) || apply(name).groups.exists(select_group)
   138           } yield name).toList
   139         }
   140       }
   141       val descendants = graph.all_succs(selected)
   142       val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
   143       (descendants, tree1)
   144     }
   145 
   146     def topological_order: List[(String, Session_Info)] =
   147       graph.topological_order.map(name => (name, apply(name)))
   148   }
   149 
   150 
   151   /* parser */
   152 
   153   private val SESSION = "session"
   154   private val IN = "in"
   155   private val DESCRIPTION = "description"
   156   private val OPTIONS = "options"
   157   private val THEORIES = "theories"
   158   private val FILES = "files"
   159 
   160   lazy val root_syntax =
   161     Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   162       (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   163 
   164   private object Parser extends Parse.Parser
   165   {
   166     def session_entry(pos: Position.T): Parser[Session_Entry] =
   167     {
   168       val session_name = atom("session name", _.is_name)
   169 
   170       val option =
   171         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   172       val options = keyword("[") ~> repsep(option, keyword(",")) <~ keyword("]")
   173 
   174       val theories =
   175         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
   176           { case _ ~ (x ~ y) => (x, y) }
   177 
   178       ((command(SESSION) ~! session_name) ^^ { case _ ~ x => x }) ~
   179         (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
   180         (keyword(IN) ~! path ^^ { case _ ~ x => x } | success(".")) ~
   181         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
   182         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
   183         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
   184         rep(theories) ~
   185         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   186           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(pos, a, b, c, d, e, f, g, h) }
   187     }
   188 
   189     def parse_entries(root: Path): List[Session_Entry] =
   190     {
   191       val toks = root_syntax.scan(File.read(root))
   192       parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
   193         case Success(result, _) => result
   194         case bad => error(bad.toString)
   195       }
   196     }
   197   }
   198 
   199 
   200   /* find sessions within certain directories */
   201 
   202   private val ROOT = Path.explode("ROOT")
   203   private val ROOTS = Path.explode("ROOTS")
   204 
   205   private def is_session_dir(dir: Path): Boolean =
   206     (dir + ROOT).is_file || (dir + ROOTS).is_file
   207 
   208   private def check_session_dir(dir: Path): Path =
   209     if (is_session_dir(dir)) dir
   210     else error("Bad session root directory: " + dir.toString)
   211 
   212   def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
   213   {
   214     def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
   215       find_root(select, dir) ::: find_roots(select, dir)
   216 
   217     def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
   218     {
   219       val root = dir + ROOT
   220       if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
   221       else Nil
   222     }
   223 
   224     def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
   225     {
   226       val roots = dir + ROOTS
   227       if (roots.is_file) {
   228         for {
   229           line <- split_lines(File.read(roots))
   230           if !(line == "" || line.startsWith("#"))
   231           dir1 =
   232             try { check_session_dir(dir + Path.explode(line)) }
   233             catch {
   234               case ERROR(msg) =>
   235                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   236             }
   237           info <- find_dir(select, dir1)
   238         } yield info
   239       }
   240       else Nil
   241     }
   242 
   243     val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
   244 
   245     more_dirs foreach { case (_, dir) => check_session_dir(dir) }
   246 
   247     Session_Tree(
   248       for {
   249         (select, dir) <- default_dirs ::: more_dirs
   250         info <- find_dir(select, dir)
   251       } yield info)
   252   }
   253 
   254 
   255 
   256   /** build **/
   257 
   258   private def echo(msg: String) { java.lang.System.out.println(msg) }
   259   private def sleep(): Unit = Thread.sleep(500)
   260 
   261 
   262   /* queue */
   263 
   264   object Queue
   265   {
   266     def apply(tree: Session_Tree): Queue =
   267     {
   268       val graph = tree.graph
   269 
   270       def outdegree(name: String): Int = graph.imm_succs(name).size
   271       def timeout(name: String): Double = tree(name).options.real("timeout")
   272 
   273       object Ordering extends scala.math.Ordering[String]
   274       {
   275         def compare(name1: String, name2: String): Int =
   276           outdegree(name2) compare outdegree(name1) match {
   277             case 0 =>
   278               timeout(name2) compare timeout(name1) match {
   279                 case 0 => name1 compare name2
   280                 case ord => ord
   281               }
   282             case ord => ord
   283           }
   284       }
   285 
   286       new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
   287     }
   288   }
   289 
   290   final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
   291   {
   292     def is_inner(name: String): Boolean = !graph.is_maximal(name)
   293 
   294     def is_empty: Boolean = graph.is_empty
   295 
   296     def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
   297 
   298     def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
   299     {
   300       val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
   301       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   302       else None
   303     }
   304   }
   305 
   306 
   307   /* source dependencies and static content */
   308 
   309   sealed case class Session_Content(
   310     loaded_theories: Set[String],
   311     syntax: Outer_Syntax,
   312     sources: List[(Path, SHA1.Digest)])
   313 
   314   sealed case class Deps(deps: Map[String, Session_Content])
   315   {
   316     def is_empty: Boolean = deps.isEmpty
   317     def apply(name: String): Session_Content = deps(name)
   318     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   319   }
   320 
   321   def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
   322     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   323       { case (deps, (name, info)) =>
   324           val (preloaded, parent_syntax) =
   325             info.parent match {
   326               case Some(parent) => (deps(parent).loaded_theories, deps(parent).syntax)
   327               case None =>
   328                 (Set.empty[String],
   329                   Outer_Syntax.init() +
   330                     // FIXME avoid hardwired stuff!?
   331                     ("theory", Keyword.THY_BEGIN) +
   332                     ("hence", Keyword.PRF_ASM_GOAL, "then have") +
   333                     ("thus", Keyword.PRF_ASM_GOAL, "then show"))
   334             }
   335           val thy_info = new Thy_Info(new Thy_Load(preloaded))
   336 
   337           if (verbose) {
   338             val groups =
   339               if (info.groups.isEmpty) ""
   340               else info.groups.mkString(" (", " ", ")")
   341             echo("Session " + name + groups)
   342           }
   343 
   344           val thy_deps =
   345             thy_info.dependencies(
   346               info.theories.map(_._2).flatten.
   347                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
   348 
   349           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
   350           val syntax = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
   351 
   352           val all_files =
   353             thy_deps.map({ case (n, h) =>
   354               val thy = Path.explode(n.node).expand
   355               val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
   356               thy :: uses
   357             }).flatten ::: info.files.map(file => info.dir + file)
   358           val sources =
   359             try { all_files.map(p => (p, SHA1.digest(p))) }
   360             catch {
   361               case ERROR(msg) =>
   362                 error(msg + "\nThe error(s) above occurred in session " +
   363                   quote(name) + Position.str_of(info.pos))
   364             }
   365 
   366           deps + (name -> Session_Content(loaded_theories, syntax, sources))
   367       }))
   368 
   369   def session_content(dirs: List[Path], session: String): Session_Content =
   370   {
   371     val (_, tree) =
   372       find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
   373     dependencies(false, tree)(session)
   374   }
   375 
   376   def outer_syntax(session: String): Outer_Syntax = session_content(Nil, session).syntax
   377 
   378 
   379   /* jobs */
   380 
   381   private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
   382     verbose: Boolean, browser_info: Path)
   383   {
   384     // global browser info dir
   385     if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   386     {
   387       browser_info.file.mkdirs()
   388       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   389         browser_info + Path.explode("isabelle.gif"))
   390       File.write(browser_info + Path.explode("index.html"),
   391         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
   392         File.read(Path.explode("~~/lib/html/library_index_content.template")) +
   393         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
   394     }
   395 
   396     def output_path: Option[Path] = if (do_output) Some(output) else None
   397 
   398     private val parent = info.parent.getOrElse("")
   399 
   400     private val args_file = File.tmp_file("args")
   401     File.write(args_file, YXML.string_of_body(
   402       if (is_pure(name)) Options.encode(info.options)
   403       else
   404         {
   405           import XML.Encode._
   406               pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   407                 pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   408               (do_output, (info.options, (verbose, (browser_info, (parent,
   409                 (name, info.theories)))))))
   410         }))
   411 
   412     private val env =
   413       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
   414         (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
   415           Isabelle_System.posix_path(args_file.getPath))
   416 
   417     private val script =
   418       if (is_pure(name)) {
   419         if (do_output) "./build " + name + " \"$OUTPUT\""
   420         else """ rm -f "$OUTPUT"; ./build """ + name
   421       }
   422       else {
   423         """
   424         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   425         """ +
   426           (if (do_output)
   427             """
   428             "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
   429             """
   430           else
   431             """
   432             rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
   433             """) +
   434         """
   435         RC="$?"
   436 
   437         . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   438 
   439         if [ "$RC" -eq 0 ]; then
   440           echo "Finished $TARGET ($TIMES_REPORT)" >&2
   441         fi
   442 
   443         exit "$RC"
   444         """
   445       }
   446 
   447     private val (thread, result) =
   448       Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
   449 
   450     def terminate: Unit = thread.interrupt
   451     def is_finished: Boolean = result.is_finished
   452 
   453     @volatile private var timeout = false
   454     private val time = Time.seconds(info.options.real("timeout"))
   455     private val timer: Option[Timer] =
   456       if (time.seconds > 0.0) {
   457         val t = new Timer("build", true)
   458         t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
   459         Some(t)
   460       }
   461       else None
   462 
   463     def join: (String, String, Int) = {
   464       val (out, err, rc) = result.join
   465       args_file.delete
   466       timer.map(_.cancel())
   467 
   468       val err1 =
   469         if (rc == 130)
   470           (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
   471           (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
   472         else err
   473       (out, err1, rc)
   474     }
   475   }
   476 
   477 
   478   /* log files and corresponding heaps */
   479 
   480   private val LOG = Path.explode("log")
   481   private def log(name: String): Path = LOG + Path.basic(name)
   482   private def log_gz(name: String): Path = log(name).ext("gz")
   483 
   484   private def sources_stamp(digests: List[SHA1.Digest]): String =
   485     digests.map(_.toString).sorted.mkString("sources: ", " ", "")
   486 
   487   private val no_heap: String = "heap: -"
   488 
   489   private def heap_stamp(heap: Option[Path]): String =
   490   {
   491     "heap: " +
   492       (heap match {
   493         case Some(path) =>
   494           val file = path.file
   495           if (file.isFile) file.length.toString + " " + file.lastModified.toString
   496           else "-"
   497         case None => "-"
   498       })
   499   }
   500 
   501   private def read_stamps(path: Path): Option[(String, String, String)] =
   502     if (path.is_file) {
   503       val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
   504       val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   505       val (s, h1, h2) =
   506         try { (reader.readLine, reader.readLine, reader.readLine) }
   507         finally { reader.close }
   508       if (s != null && s.startsWith("sources: ") &&
   509           h1 != null && h1.startsWith("heap: ") &&
   510           h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
   511       else None
   512     }
   513     else None
   514 
   515 
   516   /* build */
   517 
   518   def build(
   519     all_sessions: Boolean = false,
   520     build_heap: Boolean = false,
   521     clean_build: Boolean = false,
   522     more_dirs: List[(Boolean, Path)] = Nil,
   523     session_groups: List[String] = Nil,
   524     max_jobs: Int = 1,
   525     no_build: Boolean = false,
   526     build_options: List[String] = Nil,
   527     system_mode: Boolean = false,
   528     verbose: Boolean = false,
   529     sessions: List[String] = Nil): Int =
   530   {
   531     val options = (Options.init() /: build_options)(_.define_simple(_))
   532     val (descendants, tree) =
   533       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
   534     val deps = dependencies(verbose, tree)
   535     val queue = Queue(tree)
   536 
   537     def make_stamp(name: String): String =
   538       sources_stamp(tree(name).entry_digest :: deps.sources(name))
   539 
   540     val (input_dirs, output_dir, browser_info) =
   541       if (system_mode) {
   542         val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
   543         (List(output_dir), output_dir, Path.explode("~~/browser_info"))
   544       }
   545       else {
   546         val output_dir = Path.explode("$ISABELLE_OUTPUT")
   547         (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
   548          Path.explode("$ISABELLE_BROWSER_INFO"))
   549       }
   550 
   551     // prepare log dir
   552     (output_dir + LOG).file.mkdirs()
   553 
   554     // optional cleanup
   555     if (clean_build) {
   556       for (name <- descendants) {
   557         val files =
   558           List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   559         if (!files.isEmpty) echo("Cleaning " + name + " ...")
   560         if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
   561       }
   562     }
   563 
   564     // scheduler loop
   565     case class Result(current: Boolean, heap: String, rc: Int)
   566 
   567     @tailrec def loop(
   568       pending: Queue,
   569       running: Map[String, (String, Job)],
   570       results: Map[String, Result]): Map[String, Result] =
   571     {
   572       if (pending.is_empty) results
   573       else
   574         running.find({ case (_, (_, job)) => job.is_finished }) match {
   575           case Some((name, (parent_heap, job))) =>
   576             // finish job
   577 
   578             val (out, err, rc) = job.join
   579             echo(Library.trim_line(err))
   580 
   581             val heap =
   582               if (rc == 0) {
   583                 (output_dir + log(name)).file.delete
   584 
   585                 val sources = make_stamp(name)
   586                 val heap = heap_stamp(job.output_path)
   587                 File.write_gzip(output_dir + log_gz(name),
   588                   sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
   589 
   590                 heap
   591               }
   592               else {
   593                 (output_dir + Path.basic(name)).file.delete
   594                 (output_dir + log_gz(name)).file.delete
   595 
   596                 File.write(output_dir + log(name), out)
   597                 echo(name + " FAILED")
   598                 if (rc != 130) {
   599                   echo("(see also " + (output_dir + log(name)).file.toString + ")")
   600                   val lines = split_lines(out)
   601                   val tail = lines.drop(lines.length - 20 max 0)
   602                   echo("\n" + cat_lines(tail))
   603                 }
   604 
   605                 no_heap
   606               }
   607             loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
   608 
   609           case None if (running.size < (max_jobs max 1)) =>
   610             // check/start next job
   611             pending.dequeue(running.isDefinedAt(_)) match {
   612               case Some((name, info)) =>
   613                 val parent_result =
   614                   info.parent match {
   615                     case None => Result(true, no_heap, 0)
   616                     case Some(parent) => results(parent)
   617                   }
   618                 val output = output_dir + Path.basic(name)
   619                 val do_output = build_heap || queue.is_inner(name)
   620 
   621                 val (current, heap) =
   622                 {
   623                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   624                     case Some(dir) =>
   625                       read_stamps(dir + log_gz(name)) match {
   626                         case Some((s, h1, h2)) =>
   627                           val heap = heap_stamp(Some(dir + Path.basic(name)))
   628                           (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
   629                             !(do_output && heap == no_heap), heap)
   630                         case None => (false, no_heap)
   631                       }
   632                     case None => (false, no_heap)
   633                   }
   634                 }
   635                 val all_current = current && parent_result.current
   636 
   637                 if (all_current)
   638                   loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   639                 else if (no_build) {
   640                   if (verbose) echo("Skipping " + name + " ...")
   641                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   642                 }
   643                 else if (parent_result.rc == 0) {
   644                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   645                   val job = new Job(name, info, output, do_output, verbose, browser_info)
   646                   loop(pending, running + (name -> (parent_result.heap, job)), results)
   647                 }
   648                 else {
   649                   echo(name + " CANCELLED")
   650                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   651                 }
   652               case None => sleep(); loop(pending, running, results)
   653             }
   654           case None => sleep(); loop(pending, running, results)
   655         }
   656     }
   657 
   658     val results =
   659       if (deps.is_empty) {
   660         echo("### Nothing to build")
   661         Map.empty
   662       }
   663       else loop(queue, Map.empty, Map.empty)
   664 
   665     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   666     if (rc != 0 && (verbose || !no_build)) {
   667       val unfinished =
   668         (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
   669       echo("Unfinished session(s): " + commas(unfinished))
   670     }
   671     rc
   672   }
   673 
   674 
   675   /* command line entry point */
   676 
   677   def main(args: Array[String])
   678   {
   679     Command_Line.tool {
   680       args.toList match {
   681         case
   682           Properties.Value.Boolean(all_sessions) ::
   683           Properties.Value.Boolean(build_heap) ::
   684           Properties.Value.Boolean(clean_build) ::
   685           Properties.Value.Int(max_jobs) ::
   686           Properties.Value.Boolean(no_build) ::
   687           Properties.Value.Boolean(system_mode) ::
   688           Properties.Value.Boolean(verbose) ::
   689           Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
   690             val dirs =
   691               select_dirs.map(d => (true, Path.explode(d))) :::
   692               include_dirs.map(d => (false, Path.explode(d)))
   693             build(all_sessions, build_heap, clean_build, dirs, session_groups,
   694               max_jobs, no_build, build_options, system_mode, verbose, sessions)
   695         case _ => error("Bad arguments:\n" + cat_lines(args))
   696       }
   697     }
   698   }
   699 }
   700