src/Pure/System/build.scala
author wenzelm
Tue Aug 21 12:15:25 2012 +0200 (2012-08-21)
changeset 48870 4accee106f0f
parent 48867 e9beabf045ab
child 48872 6124e0d1120a
permissions -rw-r--r--
clarified initialization of Thy_Load, Thy_Info, Session;
     1 /*  Title:      Pure/System/build.scala
     2     Author:     Makarius
     3 
     4 Build and manage Isabelle sessions.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.util.{Timer, TimerTask}
    11 import java.io.{BufferedInputStream, FileInputStream,
    12   BufferedReader, InputStreamReader, IOException}
    13 import java.util.zip.GZIPInputStream
    14 
    15 import scala.collection.SortedSet
    16 import scala.annotation.tailrec
    17 
    18 
    19 object Build
    20 {
    21   /** session information **/
    22 
    23   // external version
    24   sealed case class Session_Entry(
    25     pos: Position.T,
    26     name: String,
    27     groups: List[String],
    28     path: String,
    29     parent: Option[String],
    30     description: String,
    31     options: List[Options.Spec],
    32     theories: List[(List[Options.Spec], List[String])],
    33     files: List[String])
    34 
    35   // internal version
    36   sealed case class Session_Info(
    37     select: Boolean,
    38     pos: Position.T,
    39     groups: List[String],
    40     dir: Path,
    41     parent: Option[String],
    42     description: String,
    43     options: Options,
    44     theories: List[(Options, List[Path])],
    45     files: List[Path],
    46     entry_digest: SHA1.Digest)
    47 
    48   def is_pure(name: String): Boolean = name == "RAW" || name == "Pure"
    49 
    50   def session_info(options: Options, select: Boolean, dir: Path, entry: Session_Entry)
    51       : (String, Session_Info) =
    52     try {
    53       val name = entry.name
    54 
    55       if (name == "") error("Bad session name")
    56       if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
    57       if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
    58 
    59       val session_options = options ++ entry.options
    60 
    61       val theories =
    62         entry.theories.map({ case (opts, thys) =>
    63           (session_options ++ opts, thys.map(Path.explode(_))) })
    64       val files = entry.files.map(Path.explode(_))
    65       val entry_digest = SHA1.digest((name, entry.parent, entry.options, entry.theories).toString)
    66 
    67       val info =
    68         Session_Info(select, entry.pos, entry.groups, dir + Path.explode(entry.path),
    69           entry.parent, entry.description, session_options, theories, files, entry_digest)
    70 
    71       (name, info)
    72     }
    73     catch {
    74       case ERROR(msg) =>
    75         error(msg + "\nThe error(s) above occurred in session entry " +
    76           quote(entry.name) + Position.str_of(entry.pos))
    77     }
    78 
    79 
    80   /* session tree */
    81 
    82   object Session_Tree
    83   {
    84     def apply(infos: Seq[(String, Session_Info)]): Session_Tree =
    85     {
    86       val graph1 =
    87         (Graph.string[Session_Info] /: infos) {
    88           case (graph, (name, info)) =>
    89             if (graph.defined(name))
    90               error("Duplicate session " + quote(name) + Position.str_of(info.pos))
    91             else graph.new_node(name, info)
    92         }
    93       val graph2 =
    94         (graph1 /: graph1.entries) {
    95           case (graph, (name, (info, _))) =>
    96             info.parent match {
    97               case None => graph
    98               case Some(parent) =>
    99                 if (!graph.defined(parent))
   100                   error("Bad parent session " + quote(parent) + " for " +
   101                     quote(name) + Position.str_of(info.pos))
   102 
   103                 try { graph.add_edge_acyclic(parent, name) }
   104                 catch {
   105                   case exn: Graph.Cycles[_] =>
   106                     error(cat_lines(exn.cycles.map(cycle =>
   107                       "Cyclic session dependency of " +
   108                         cycle.map(c => quote(c.toString)).mkString(" via "))) +
   109                           Position.str_of(info.pos))
   110                 }
   111             }
   112         }
   113       new Session_Tree(graph2)
   114     }
   115   }
   116 
   117   final class Session_Tree private(val graph: Graph[String, Session_Info])
   118     extends PartialFunction[String, Session_Info]
   119   {
   120     def apply(name: String): Session_Info = graph.get_node(name)
   121     def isDefinedAt(name: String): Boolean = graph.defined(name)
   122 
   123     def required(all_sessions: Boolean, session_groups: List[String], sessions: List[String])
   124       : (List[String], Session_Tree) =
   125     {
   126       val bad_sessions = sessions.filterNot(isDefinedAt(_))
   127       if (!bad_sessions.isEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
   128 
   129       val selected =
   130       {
   131         if (all_sessions) graph.keys.toList
   132         else {
   133           val select_group = session_groups.toSet
   134           val select = sessions.toSet
   135           (for {
   136             (name, (info, _)) <- graph.entries
   137             if info.select || select(name) || apply(name).groups.exists(select_group)
   138           } yield name).toList
   139         }
   140       }
   141       val descendants = graph.all_succs(selected)
   142       val tree1 = new Session_Tree(graph.restrict(graph.all_preds(selected).toSet))
   143       (descendants, tree1)
   144     }
   145 
   146     def topological_order: List[(String, Session_Info)] =
   147       graph.topological_order.map(name => (name, apply(name)))
   148 
   149     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) ~! session_name) ^^ { case _ ~ x => x }) ~
   181         (keyword("(") ~! (rep1(name) <~ keyword(")")) ^^ { case _ ~ x => x } | success(Nil)) ~
   182         (keyword(IN) ~! path ^^ { case _ ~ x => x } | success(".")) ~
   183         (keyword("=") ~> opt(session_name <~ keyword("+"))) ~
   184         (keyword(DESCRIPTION) ~! text ^^ { case _ ~ x => x } | success("")) ~
   185         (keyword(OPTIONS) ~! options ^^ { case _ ~ x => x } | success(Nil)) ~
   186         rep(theories) ~
   187         (keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x } | success(Nil)) ^^
   188           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h => Session_Entry(pos, a, b, c, d, e, f, g, h) }
   189     }
   190 
   191     def parse_entries(root: Path): List[Session_Entry] =
   192     {
   193       val toks = root_syntax.scan(File.read(root))
   194       parse_all(rep(session_entry(root.position)), Token.reader(toks, root.implode)) match {
   195         case Success(result, _) => result
   196         case bad => error(bad.toString)
   197       }
   198     }
   199   }
   200 
   201 
   202   /* find sessions within certain directories */
   203 
   204   private val ROOT = Path.explode("ROOT")
   205   private val ROOTS = Path.explode("ROOTS")
   206 
   207   private def is_session_dir(dir: Path): Boolean =
   208     (dir + ROOT).is_file || (dir + ROOTS).is_file
   209 
   210   private def check_session_dir(dir: Path): Path =
   211     if (is_session_dir(dir)) dir
   212     else error("Bad session root directory: " + dir.toString)
   213 
   214   def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
   215   {
   216     def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
   217       find_root(select, dir) ::: find_roots(select, dir)
   218 
   219     def find_root(select: Boolean, dir: Path): List[(String, Session_Info)] =
   220     {
   221       val root = dir + ROOT
   222       if (root.is_file) Parser.parse_entries(root).map(session_info(options, select, dir, _))
   223       else Nil
   224     }
   225 
   226     def find_roots(select: Boolean, dir: Path): List[(String, Session_Info)] =
   227     {
   228       val roots = dir + ROOTS
   229       if (roots.is_file) {
   230         for {
   231           line <- split_lines(File.read(roots))
   232           if !(line == "" || line.startsWith("#"))
   233           dir1 =
   234             try { check_session_dir(dir + Path.explode(line)) }
   235             catch {
   236               case ERROR(msg) =>
   237                 error(msg + "\nThe error(s) above occurred in session catalog " + roots.toString)
   238             }
   239           info <- find_dir(select, dir1)
   240         } yield info
   241       }
   242       else Nil
   243     }
   244 
   245     val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
   246 
   247     more_dirs foreach { case (_, dir) => check_session_dir(dir) }
   248 
   249     Session_Tree(
   250       for {
   251         (select, dir) <- default_dirs ::: more_dirs
   252         info <- find_dir(select, dir)
   253       } yield info)
   254   }
   255 
   256 
   257 
   258   /** build **/
   259 
   260   private def echo(msg: String) { java.lang.System.out.println(msg) }
   261   private def sleep(): Unit = Thread.sleep(500)
   262 
   263 
   264   /* queue */
   265 
   266   object Queue
   267   {
   268     def apply(tree: Session_Tree): Queue =
   269     {
   270       val graph = tree.graph
   271 
   272       def outdegree(name: String): Int = graph.imm_succs(name).size
   273       def timeout(name: String): Double = tree(name).options.real("timeout")
   274 
   275       object Ordering extends scala.math.Ordering[String]
   276       {
   277         def compare(name1: String, name2: String): Int =
   278           outdegree(name2) compare outdegree(name1) match {
   279             case 0 =>
   280               timeout(name2) compare timeout(name1) match {
   281                 case 0 => name1 compare name2
   282                 case ord => ord
   283               }
   284             case ord => ord
   285           }
   286       }
   287 
   288       new Queue(graph, SortedSet(graph.keys.toList: _*)(Ordering))
   289     }
   290   }
   291 
   292   final class Queue private(graph: Graph[String, Session_Info], order: SortedSet[String])
   293   {
   294     def is_inner(name: String): Boolean = !graph.is_maximal(name)
   295 
   296     def is_empty: Boolean = graph.is_empty
   297 
   298     def - (name: String): Queue = new Queue(graph.del_node(name), order - name)
   299 
   300     def dequeue(skip: String => Boolean): Option[(String, Session_Info)] =
   301     {
   302       val it = order.iterator.dropWhile(name => skip(name) || !graph.is_minimal(name))
   303       if (it.hasNext) { val name = it.next; Some((name, graph.get_node(name))) }
   304       else None
   305     }
   306   }
   307 
   308 
   309   /* source dependencies and static content */
   310 
   311   sealed case class Session_Content(
   312     loaded_theories: Set[String],
   313     syntax: Outer_Syntax,
   314     sources: List[(Path, SHA1.Digest)],
   315     errors: List[String])
   316   {
   317     def check_errors: Session_Content =
   318     {
   319       if (errors.isEmpty) this
   320       else error(cat_lines(errors))
   321     }
   322   }
   323 
   324   sealed case class Deps(deps: Map[String, Session_Content])
   325   {
   326     def is_empty: Boolean = deps.isEmpty
   327     def apply(name: String): Session_Content = deps(name)
   328     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   329   }
   330 
   331   def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
   332     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   333       { case (deps, (name, info)) =>
   334           val (preloaded, parent_syntax, parent_errors) =
   335             info.parent match {
   336               case None =>
   337                 (Set.empty[String], Outer_Syntax.init_pure(), Nil)
   338               case Some(parent_name) =>
   339                 val parent = deps(parent_name)
   340                 (parent.loaded_theories, parent.syntax, parent.errors)
   341             }
   342           val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
   343 
   344           if (verbose) {
   345             val groups =
   346               if (info.groups.isEmpty) ""
   347               else info.groups.mkString(" (", " ", ")")
   348             echo("Session " + name + groups)
   349           }
   350 
   351           val thy_deps =
   352             thy_info.dependencies(
   353               info.theories.map(_._2).flatten.
   354                 map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
   355 
   356           val loaded_theories = preloaded ++ thy_deps.map(_._1.theory)
   357           val syntax0 = (parent_syntax /: thy_deps) { case (syn, (_, h)) => syn.add_keywords(h) }
   358           val syntax =
   359             // FIXME avoid hardwired stuff!?
   360             // FIXME broken?!
   361             if (name == "Pure")
   362               syntax0 +
   363                 ("hence", (Keyword.PRF_ASM_GOAL, Nil), "then have") +
   364                 ("thus", (Keyword.PRF_ASM_GOAL, Nil), "then show")
   365             else syntax0
   366 
   367           val all_files =
   368             thy_deps.map({ case (n, h) =>
   369               val thy = Path.explode(n.node).expand
   370               val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
   371               thy :: uses
   372             }).flatten ::: info.files.map(file => info.dir + file)
   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.str_of(info.pos))
   379             }
   380           val errors = parent_errors ::: thy_deps.map(d => d._2.errors).flatten
   381 
   382           deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
   383       }))
   384 
   385   def session_content(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(false, tree)(session)
   390   }
   391 
   392   def outer_syntax(session: String): Outer_Syntax =
   393     session_content(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     no_build: Boolean = false,
   543     build_options: List[String] = Nil,
   544     system_mode: Boolean = false,
   545     verbose: Boolean = false,
   546     sessions: List[String] = Nil): Int =
   547   {
   548     val options = (Options.init() /: build_options)(_ + _)
   549     val (descendants, tree) =
   550       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
   551     val deps = dependencies(verbose, tree)
   552     val queue = Queue(tree)
   553 
   554     def make_stamp(name: String): String =
   555       sources_stamp(tree(name).entry_digest :: deps.sources(name))
   556 
   557     val (input_dirs, output_dir, browser_info) =
   558       if (system_mode) {
   559         val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
   560         (List(output_dir), output_dir, Path.explode("~~/browser_info"))
   561       }
   562       else {
   563         val output_dir = Path.explode("$ISABELLE_OUTPUT")
   564         (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
   565          Path.explode("$ISABELLE_BROWSER_INFO"))
   566       }
   567 
   568     // prepare log dir
   569     (output_dir + LOG).file.mkdirs()
   570 
   571     // optional cleanup
   572     if (clean_build) {
   573       for (name <- descendants) {
   574         val files =
   575           List(Path.basic(name), log(name), log_gz(name)).map(output_dir + _).filter(_.is_file)
   576         if (!files.isEmpty) echo("Cleaning " + name + " ...")
   577         if (!files.forall(p => p.file.delete)) echo(name + " FAILED to delete")
   578       }
   579     }
   580 
   581     // scheduler loop
   582     case class Result(current: Boolean, heap: String, rc: Int)
   583 
   584     @tailrec def loop(
   585       pending: Queue,
   586       running: Map[String, (String, Job)],
   587       results: Map[String, Result]): Map[String, Result] =
   588     {
   589       if (pending.is_empty) results
   590       else
   591         running.find({ case (_, (_, job)) => job.is_finished }) match {
   592           case Some((name, (parent_heap, job))) =>
   593             // finish job
   594 
   595             val (out, err, rc) = job.join
   596             echo(Library.trim_line(err))
   597 
   598             val heap =
   599               if (rc == 0) {
   600                 (output_dir + log(name)).file.delete
   601 
   602                 val sources = make_stamp(name)
   603                 val heap = heap_stamp(job.output_path)
   604                 File.write_gzip(output_dir + log_gz(name),
   605                   sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
   606 
   607                 heap
   608               }
   609               else {
   610                 (output_dir + Path.basic(name)).file.delete
   611                 (output_dir + log_gz(name)).file.delete
   612 
   613                 File.write(output_dir + log(name), out)
   614                 echo(name + " FAILED")
   615                 if (rc != 130) {
   616                   echo("(see also " + (output_dir + log(name)).file.toString + ")")
   617                   val lines = split_lines(out)
   618                   val tail = lines.drop(lines.length - 20 max 0)
   619                   echo("\n" + cat_lines(tail))
   620                 }
   621 
   622                 no_heap
   623               }
   624             loop(pending - name, running - name, results + (name -> Result(false, heap, rc)))
   625 
   626           case None if (running.size < (max_jobs max 1)) =>
   627             // check/start next job
   628             pending.dequeue(running.isDefinedAt(_)) match {
   629               case Some((name, info)) =>
   630                 val parent_result =
   631                   info.parent match {
   632                     case None => Result(true, no_heap, 0)
   633                     case Some(parent) => results(parent)
   634                   }
   635                 val output = output_dir + Path.basic(name)
   636                 val do_output = build_heap || queue.is_inner(name)
   637 
   638                 val (current, heap) =
   639                 {
   640                   input_dirs.find(dir => (dir + log_gz(name)).is_file) match {
   641                     case Some(dir) =>
   642                       read_stamps(dir + log_gz(name)) match {
   643                         case Some((s, h1, h2)) =>
   644                           val heap = heap_stamp(Some(dir + Path.basic(name)))
   645                           (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap &&
   646                             !(do_output && heap == no_heap), heap)
   647                         case None => (false, no_heap)
   648                       }
   649                     case None => (false, no_heap)
   650                   }
   651                 }
   652                 val all_current = current && parent_result.current
   653 
   654                 if (all_current)
   655                   loop(pending - name, running, results + (name -> Result(true, heap, 0)))
   656                 else if (no_build) {
   657                   if (verbose) echo("Skipping " + name + " ...")
   658                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   659                 }
   660                 else if (parent_result.rc == 0) {
   661                   echo((if (do_output) "Building " else "Running ") + name + " ...")
   662                   val job = new Job(name, info, output, do_output, verbose, browser_info)
   663                   loop(pending, running + (name -> (parent_result.heap, job)), results)
   664                 }
   665                 else {
   666                   echo(name + " CANCELLED")
   667                   loop(pending - name, running, results + (name -> Result(false, heap, 1)))
   668                 }
   669               case None => sleep(); loop(pending, running, results)
   670             }
   671           case None => sleep(); loop(pending, running, results)
   672         }
   673     }
   674 
   675     val results =
   676       if (deps.is_empty) {
   677         echo("### Nothing to build")
   678         Map.empty
   679       }
   680       else loop(queue, Map.empty, Map.empty)
   681 
   682     val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc })
   683     if (rc != 0 && (verbose || !no_build)) {
   684       val unfinished =
   685         (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted
   686       echo("Unfinished session(s): " + commas(unfinished))
   687     }
   688     rc
   689   }
   690 
   691 
   692   /* command line entry point */
   693 
   694   def main(args: Array[String])
   695   {
   696     Command_Line.tool {
   697       args.toList match {
   698         case
   699           Properties.Value.Boolean(all_sessions) ::
   700           Properties.Value.Boolean(build_heap) ::
   701           Properties.Value.Boolean(clean_build) ::
   702           Properties.Value.Int(max_jobs) ::
   703           Properties.Value.Boolean(no_build) ::
   704           Properties.Value.Boolean(system_mode) ::
   705           Properties.Value.Boolean(verbose) ::
   706           Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
   707             val dirs =
   708               select_dirs.map(d => (true, Path.explode(d))) :::
   709               include_dirs.map(d => (false, Path.explode(d)))
   710             build(all_sessions, build_heap, clean_build, dirs, session_groups,
   711               max_jobs, no_build, build_options, system_mode, verbose, sessions)
   712         case _ => error("Bad arguments:\n" + cat_lines(args))
   713       }
   714     }
   715   }
   716 }
   717