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