src/Pure/System/build.scala
author wenzelm
Mon Sep 03 21:30:34 2012 +0200 (2012-09-03)
changeset 49098 673e0ed547af
parent 48992 0518bf89c777
child 49131 aa1e2ba3c697
permissions -rw-r--r--
bypass slow check for inlined files, where it is not really required;
     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.here(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.here(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.here(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.here(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     override def toString: String = graph.entries.map(_._1).toList.sorted.mkString(",")
   150   }
   151 
   152 
   153   /* parser */
   154 
   155   private val SESSION = "session"
   156   private val IN = "in"
   157   private val DESCRIPTION = "description"
   158   private val OPTIONS = "options"
   159   private val THEORIES = "theories"
   160   private val FILES = "files"
   161 
   162   lazy val root_syntax =
   163     Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
   164       (SESSION, Keyword.THY_DECL) + IN + DESCRIPTION + OPTIONS + THEORIES + FILES
   165 
   166   private object Parser extends Parse.Parser
   167   {
   168     def session_entry(pos: Position.T): Parser[Session_Entry] =
   169     {
   170       val session_name = atom("session name", _.is_name)
   171 
   172       val option =
   173         name ~ opt(keyword("=") ~! name ^^ { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
   174       val options = keyword("[") ~> rep1sep(option, keyword(",")) <~ keyword("]")
   175 
   176       val theories =
   177         keyword(THEORIES) ~! ((options | success(Nil)) ~ rep(theory_name)) ^^
   178           { case _ ~ (x ~ y) => (x, y) }
   179 
   180       command(SESSION) ~!
   181         (session_name ~
   182           ((keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
   183           ((keyword(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
   184           (keyword("=") ~!
   185             (opt(session_name ~! keyword("+") ^^ { case x ~ _ => x }) ~
   186               ((keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
   187               ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
   188               rep1(theories) ~
   189               ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^
   190         { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) =>
   191             Session_Entry(pos, a, b, c, d, e, f, g, h) }
   192     }
   193 
   194     def parse_entries(root: Path): List[Session_Entry] =
   195     {
   196       val toks = root_syntax.scan(File.read(root))
   197       parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
   198         case Success(result, _) => result
   199         case bad => error(bad.toString)
   200       }
   201     }
   202   }
   203 
   204 
   205   /* find sessions within certain directories */
   206 
   207   private val ROOT = Path.explode("ROOT")
   208   private val ROOTS = Path.explode("ROOTS")
   209 
   210   private def is_session_dir(dir: Path): Boolean =
   211     (dir + ROOT).is_file || (dir + ROOTS).is_file
   212 
   213   private def check_session_dir(dir: Path): Path =
   214     if (is_session_dir(dir)) dir
   215     else error("Bad session root directory: " + dir.toString)
   216 
   217   def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
   218   {
   219     def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
   220       find_root(select, dir) ::: find_roots(select, dir)
   221 
   222     def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
   223     {
   224       val root = dir + ROOT
   225       if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
   226       else Nil
   227     }
   228 
   229     def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
   230     {
   231       val roots = dir + ROOTS
   232       if (roots.is_file) {
   233         for {
   234           line <- split_lines(File.read(roots))
   235           if !(line == "" || line.startsWith("#"))
   236           dir1 =
   237             try { check_session_dir(dir + Path.explode(line)) }
   238             catch {
   239               case ERROR(msg) =>
   240                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   241             }
   242           info <- find_dir(select, dir1)
   243         } yield info
   244       }
   245       else Nil
   246     }
   247 
   248     val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
   249 
   250     more_dirs foreach { case (_, dir) => check_session_dir(dir) }
   251 
   252     Session_Tree(
   253       for {
   254         (select, dir) <- default_dirs ::: more_dirs
   255         info <- find_dir(select, dir)
   256       } yield info)
   257   }
   258 
   259 
   260 
   261   /** build **/
   262 
   263   private def echo(msg: String) { java.lang.System.out.println(msg) }
   264   private def sleep(): Unit = Thread.sleep(500)
   265 
   266 
   267   /* queue */
   268 
   269   object Queue
   270   {
   271     def apply(tree: Session_Tree): Queue =
   272     {
   273       val graph = tree.graph
   274 
   275       def outdegree(name: String): Int = graph.imm_succs(name).size
   276       def timeout(name: String): Double = tree(name).options.real("timeout")
   277 
   278       object Ordering extends scala.math.Ordering[String]
   279       {
   280         def compare(name1: String, name2: String): Int =
   281           outdegree(name2) compare outdegree(name1) match {
   282             case 0 =>
   283               timeout(name2) compare timeout(name1) match {
   284                 case 0 => name1 compare name2
   285                 case ord => ord
   286               }
   287             case ord => ord
   288           }
   289       }
   290 
   291       new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
   292     }
   293   }
   294 
   295   final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
   296   {
   297     def is_inner(name: String): Boolean = !graph.is_maximal(name)
   298 
   299     def is_empty: Boolean = graph.is_empty
   300 
   301     def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
   302 
   303     def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
   304     {
   305       val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
   306       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   307       else None
   308     }
   309   }
   310 
   311 
   312   /* source dependencies and static content */
   313 
   314   sealed case class Session_Content(
   315     loaded_theories: Set[String],
   316     syntax: Outer_Syntax,
   317     sources: List[(Path, SHA1.Digest)],
   318     errors: List[String])
   319   {
   320     def check_errors: Session_Content =
   321     {
   322       if (errors.isEmpty) this
   323       else error(cat_lines(errors))
   324     }
   325   }
   326 
   327   sealed case class Deps(deps: Map[String, Session_Content])
   328   {
   329     def is_empty: Boolean = deps.isEmpty
   330     def apply(name: String): Session_Content = deps(name)
   331     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   332   }
   333 
   334   def dependencies(inlined_files: Boolean, verbose: Boolean, list_files: Boolean,
   335       tree: Session_Tree): Deps =
   336     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   337       { case (deps, (name, info)) =>
   338           val (preloaded, parent_syntax, parent_errors) =
   339             info.parent match {
   340               case None =>
   341                 (Set.empty[String], Outer_Syntax.init_pure(), Nil)
   342               case Some(parent_name) =>
   343                 val parent = deps(parent_name)
   344                 (parent.loaded_theories, parent.syntax, parent.errors)
   345             }
   346           val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
   347 
   348           if (verbose || list_files) {
   349             val groups =
   350               if (info.groups.isEmpty) ""
   351               else info.groups.mkString(" (", " ", ")")
   352             echo("Session " + name + groups)
   353           }
   354 
   355           val thy_deps =
   356             thy_info.dependencies(inlined_files,
   357               info.theories.map(_._2).flatten.
   358                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
   359 
   360           val loaded_theories = thy_deps.loaded_theories
   361           val syntax = thy_deps.make_syntax
   362 
   363           val all_files =
   364             (thy_deps.deps.map({ case (n, h) =>
   365               val thy = Path.explode(n.node)
   366               val uses = h.uses.map(p => Path.explode(n.dir) + Path.explode(p._1))
   367               thy :: uses
   368             }).flatten ::: info.files.map(file => info.dir + file)).map(_.expand)
   369 
   370           if (list_files)
   371             echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
   372 
   373           val sources =
   374             try { all_files.map(p => (p, SHA1.digest(p))) }
   375             catch {
   376               case ERROR(msg) =>
   377                 error(msg + "\nThe error(s) above occurred in session " +
   378                   quote(name) + Position.here(info.pos))
   379             }
   380           val errors = parent_errors ::: thy_deps.deps.map(d => d._2.errors).flatten
   381 
   382           deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
   383       }))
   384 
   385   def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
   386   {
   387     val (_, tree) =
   388       find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
   389     dependencies(inlined_files, false, false, tree)(session)
   390   }
   391 
   392   def outer_syntax(session: String): Outer_Syntax =
   393     session_content(false, Nil, session).check_errors.syntax
   394 
   395 
   396   /* jobs */
   397 
   398   private class Job(name: String, info: Session_Info, output: Path, do_output: Boolean,
   399     verbose: Boolean, browser_info: Path)
   400   {
   401     // global browser info dir
   402     if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
   403     {
   404       browser_info.file.mkdirs()
   405       File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
   406         browser_info + Path.explode("isabelle.gif"))
   407       File.write(browser_info + Path.explode("index.html"),
   408         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
   409         File.read(Path.explode("~~/lib/html/library_index_content.template")) +
   410         File.read(Path.explode("~~/lib/html/library_index_footer.template")))
   411     }
   412 
   413     def output_path: Option[Path] = if (do_output) Some(output) else None
   414 
   415     private val parent = info.parent.getOrElse("")
   416 
   417     private val args_file = File.tmp_file("args")
   418     File.write(args_file, YXML.string_of_body(
   419       if (is_pure(name)) Options.encode(info.options)
   420       else
   421         {
   422           import XML.Encode._
   423               pair(bool, pair(Options.encode, pair(bool, pair(Path.encode, pair(string,
   424                 pair(string, list(pair(Options.encode, list(Path.encode)))))))))(
   425               (do_output, (info.options, (verbose, (browser_info, (parent,
   426                 (name, info.theories)))))))
   427         }))
   428 
   429     private val env =
   430       Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
   431         (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
   432           Isabelle_System.posix_path(args_file.getPath))
   433 
   434     private val script =
   435       if (is_pure(name)) {
   436         if (do_output) "./build " + name + " \"$OUTPUT\""
   437         else """ rm -f "$OUTPUT"; ./build """ + name
   438       }
   439       else {
   440         """
   441         . "$ISABELLE_HOME/lib/scripts/timestart.bash"
   442         """ +
   443           (if (do_output)
   444             """
   445             "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT"
   446             """
   447           else
   448             """
   449             rm -f "$OUTPUT"; "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT"
   450             """) +
   451         """
   452         RC="$?"
   453 
   454         . "$ISABELLE_HOME/lib/scripts/timestop.bash"
   455 
   456         if [ "$RC" -eq 0 ]; then
   457           echo "Finished $TARGET ($TIMES_REPORT)" >&2
   458         fi
   459 
   460         exit "$RC"
   461         """
   462       }
   463 
   464     private val (thread, result) =
   465       Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
   466 
   467     def terminate: Unit = thread.interrupt
   468     def is_finished: Boolean = result.is_finished
   469 
   470     @volatile private var timeout = false
   471     private val time = Time.seconds(info.options.real("timeout"))
   472     private val timer: Option[Timer] =
   473       if (time.seconds > 0.0) {
   474         val t = new Timer("build", true)
   475         t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
   476         Some(t)
   477       }
   478       else None
   479 
   480     def join: (String, String, Int) = {
   481       val (out, err, rc) = result.join
   482       args_file.delete
   483       timer.map(_.cancel())
   484 
   485       val err1 =
   486         if (rc == 130)
   487           (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
   488           (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
   489         else err
   490       (out, err1, rc)
   491     }
   492   }
   493 
   494 
   495   /* log files and corresponding heaps */
   496 
   497   private val LOG = Path.explode("log")
   498   private def log(name: String): Path = LOG + Path.basic(name)
   499   private def log_gz(name: String): Path = log(name).ext("gz")
   500 
   501   private def sources_stamp(digests: List[SHA1.Digest]): String =
   502     digests.map(_.toString).sorted.mkString("sources: ", " ", "")
   503 
   504   private val no_heap: String = "heap: -"
   505 
   506   private def heap_stamp(heap: Option[Path]): String =
   507   {
   508     "heap: " +
   509       (heap match {
   510         case Some(path) =>
   511           val file = path.file
   512           if (file.isFile) file.length.toString + " " + file.lastModified.toString
   513           else "-"
   514         case None => "-"
   515       })
   516   }
   517 
   518   private def read_stamps(path: Path): Option[(String, String, String)] =
   519     if (path.is_file) {
   520       val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file)))
   521       val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   522       val (s, h1, h2) =
   523         try { (reader.readLine, reader.readLine, reader.readLine) }
   524         finally { reader.close }
   525       if (s != null && s.startsWith("sources: ") &&
   526           h1 != null && h1.startsWith("heap: ") &&
   527           h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2))
   528       else None
   529     }
   530     else None
   531 
   532 
   533   /* build */
   534 
   535   def build(
   536     all_sessions: Boolean = false,
   537     build_heap: Boolean = false,
   538     clean_build: Boolean = false,
   539     more_dirs: List[(Boolean, Path)] = Nil,
   540     session_groups: List[String] = Nil,
   541     max_jobs: Int = 1,
   542     list_files: Boolean = false,
   543     no_build: Boolean = false,
   544     build_options: List[String] = Nil,
   545     system_mode: Boolean = false,
   546     verbose: Boolean = false,
   547     sessions: List[String] = Nil): Int =
   548   {
   549     val options = (Options.init() /: build_options)(_ + _)
   550     val (descendants, tree) =
   551       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
   552     val deps = dependencies(true, verbose, list_files, tree)
   553     val queue = Queue(tree)
   554 
   555     def make_stamp(name: String): String =
   556       sources_stamp(tree(name).entry_digest :: deps.sources(name))
   557 
   558     val (input_dirs, output_dir, browser_info) =
   559       if (system_mode) {
   560         val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
   561         (List(output_dir), output_dir, Path.explode("~~/browser_info"))
   562       }
   563       else {
   564         val output_dir = Path.explode("$ISABELLE_OUTPUT")
   565         (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
   566          Path.explode("$ISABELLE_BROWSER_INFO"))
   567       }
   568 
   569     // prepare log dir
   570     (output_dir + LOG).file.mkdirs()
   571 
   572     // optional cleanup
   573     if (clean_build) {
   574       for (name <- descendants) {
   575         val files =
   576           List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   577         if (!files.isEmpty) echo("Cleaning " + name + " ...")
   578         if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
   579       }
   580     }
   581 
   582     // scheduler loop
   583     case class Result(current: Boolean, heap: String, rc: Int)
   584 
   585     @tailrec def loop(
   586       pending: Queue,
   587       running: Map[String, (String, Job)],
   588       results: Map[String, Result]): Map[String, Result] =
   589     {
   590       if (pending.is_empty) results
   591       else
   592         running.find({ case (_, (_, job)) => job.is_finished }) match {
   593           case Some((name, (parent_heap, job))) =>
   594             // finish job
   595 
   596             val (out, err, rc) = job.join
   597             echo(Library.trim_line(err))
   598 
   599             val heap =
   600               if (rc == 0) {
   601                 (output_dir + log(name)).file.delete
   602 
   603                 val sources = make_stamp(name)
   604                 val heap = heap_stamp(job.output_path)
   605                 File.write_gzip(output_dir + log_gz(name),
   606                   sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
   607 
   608                 heap
   609               }
   610               else {
   611                 (output_dir + Path.basic(name)).file.delete
   612                 (output_dir + log_gz(name)).file.delete
   613 
   614                 File.write(output_dir + log(name), out)
   615                 echo(name + " FAILED")
   616                 if (rc != 130) {
   617                   echo("(see also " + (output_dir + log(name)).file.toString + ")")
   618                   val lines = split_lines(out)
   619                   val tail = lines.drop(lines.length - 20 max 0)
   620                   echo("\n" + cat_lines(tail))
   621                 }
   622 
   623                 no_heap
   624               }
   625             loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
   626 
   627           case None if (running.size < (max_jobs max 1)) =>
   628             // check/start next job
   629             pending.dequeue(running.isDefinedAt(_)) match {
   630               case Some((name, info)) =>
   631                 val parent_result =
   632                   info.parent match {
   633                     case None => Result(true, no_heap, 0)
   634                     case Some(parent) => results(parent)
   635                   }
   636                 val output = output_dir + Path.basic(name)
   637                 val do_output = build_heap || queue.is_inner(name)
   638 
   639                 val (current, heap) =
   640                 {
   641                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   642                     case Some(dir) =>
   643                       read_stamps(dir + log_gz(name)) match {
   644                         case Some((s, h1, h2)) =>
   645                           val heap = heap_stamp(Some(dir + Path.basic(name)))
   646                           (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
   647                             !(do_output && heap == no_heap), heap)
   648                         case None => (false, no_heap)
   649                       }
   650                     case None => (false, no_heap)
   651                   }
   652                 }
   653                 val all_current = current && parent_result.current
   654 
   655                 if (all_current)
   656                   loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   657                 else if (no_build) {
   658                   if (verbose) echo("Skipping " + name + " ...")
   659                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   660                 }
   661                 else if (parent_result.rc == 0) {
   662                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   663                   val job = new Job(name, info, output, do_output, verbose, browser_info)
   664                   loop(pending, running + (name -> (parent_result.heap, job)), results)
   665                 }
   666                 else {
   667                   echo(name + " CANCELLED")
   668                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   669                 }
   670               case None => sleep(); loop(pending, running, results)
   671             }
   672           case None => sleep(); loop(pending, running, results)
   673         }
   674     }
   675 
   676     val results =
   677       if (deps.is_empty) {
   678         echo("### Nothing to build")
   679         Map.empty
   680       }
   681       else loop(queue, Map.empty, Map.empty)
   682 
   683     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   684     if (rc != 0 && (verbose || !no_build)) {
   685       val unfinished =
   686         (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
   687       echo("Unfinished session(s): " + commas(unfinished))
   688     }
   689     rc
   690   }
   691 
   692 
   693   /* command line entry point */
   694 
   695   def main(args: Array[String])
   696   {
   697     Command_Line.tool {
   698       args.toList match {
   699         case
   700           Properties.Value.Boolean(all_sessions) ::
   701           Properties.Value.Boolean(build_heap) ::
   702           Properties.Value.Boolean(clean_build) ::
   703           Properties.Value.Int(max_jobs) ::
   704           Properties.Value.Boolean(list_files) ::
   705           Properties.Value.Boolean(no_build) ::
   706           Properties.Value.Boolean(system_mode) ::
   707           Properties.Value.Boolean(verbose) ::
   708           Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
   709             val dirs =
   710               select_dirs.map(d => (true, Path.explode(d))) :::
   711               include_dirs.map(d => (false, Path.explode(d)))
   712             build(all_sessions, build_heap, clean_build, dirs, session_groups,
   713               max_jobs, list_files, no_build, build_options, system_mode, verbose, sessions)
   714         case _ => error("Bad arguments:\n" + cat_lines(args))
   715       }
   716     }
   717   }
   718 }
   719