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