1.1 --- a/src/Pure/System/build.scala	Wed Jul 25 19:49:40 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Wed Jul 25 22:25:07 2012 +0200
     1.3 @@ -292,7 +292,7 @@
     1.4    private def sleep(): Unit = Thread.sleep(500)
     1.5  
     1.6  
     1.7 -  /* dependencies */
     1.8 +  /* source dependencies */
     1.9  
    1.10    sealed case class Node(
    1.11      loaded_theories: Set[String],
    1.12 @@ -300,21 +300,9 @@
    1.13  
    1.14    sealed case class Deps(deps: Map[String, Node])
    1.15    {
    1.16 -    def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
    1.17 +    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    1.18    }
    1.19  
    1.20 -  private def read_deps(file: JFile): List[String] =
    1.21 -    if (file.isFile) {
    1.22 -      val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(file)))
    1.23 -      val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
    1.24 -      try {
    1.25 -        List(reader.readLine).filter(_.startsWith("sources:")) :::
    1.26 -        List(reader.readLine).filter(_.startsWith("heap:"))
    1.27 -      }
    1.28 -      finally { reader.close }
    1.29 -    }
    1.30 -    else Nil
    1.31 -
    1.32    def dependencies(verbose: Boolean, queue: Session.Queue): Deps =
    1.33      Deps((Map.empty[String, Node] /: queue.topological_order)(
    1.34        { case (deps, (name, info)) =>
    1.35 @@ -430,6 +418,42 @@
    1.36    }
    1.37  
    1.38  
    1.39 +  /* log files and corresponding heaps */
    1.40 +
    1.41 +  val LOG = Path.explode("log")
    1.42 +  def log(name: String): Path = LOG + Path.basic(name)
    1.43 +  def log_gz(name: String): Path = log(name).ext("gz")
    1.44 +
    1.45 +  def sources_stamp(digests: List[SHA1.Digest]): String =
    1.46 +    digests.map(_.toString).sorted.mkString("sources: ", " ", "")
    1.47 +
    1.48 +  def heap_stamp(output: Option[Path]): String =
    1.49 +  {
    1.50 +    "heap: " +
    1.51 +      (output match {
    1.52 +        case Some(path) =>
    1.53 +          val file = path.file
    1.54 +          if (file.isFile) file.length.toString + " " + file.lastModified.toString
    1.55 +          else "-"
    1.56 +        case None => "-"
    1.57 +      })
    1.58 +  }
    1.59 +
    1.60 +  def check_stamps(dir: Path, name: String): Option[(String, Boolean)] =
    1.61 +  {
    1.62 +    val file = (dir + log_gz(name)).file
    1.63 +    if (file.isFile) {
    1.64 +      val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(file)))
    1.65 +      val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
    1.66 +      val (s, h) = try { (reader.readLine, reader.readLine) } finally { reader.close }
    1.67 +      if (s != null && s.startsWith("sources: ") && h != null && h.startsWith("heap: ") &&
    1.68 +          h == heap_stamp(Some(dir + Path.basic(name)))) Some((s, h != "heap: -"))
    1.69 +      else None
    1.70 +    }
    1.71 +    else None
    1.72 +  }
    1.73 +
    1.74 +
    1.75    /* build */
    1.76  
    1.77    def build(all_sessions: Boolean, build_images: Boolean, max_jobs: Int,
    1.78 @@ -440,13 +464,22 @@
    1.79      val queue = find_sessions(options, all_sessions, sessions, more_dirs)
    1.80      val deps = dependencies(verbose, queue)
    1.81  
    1.82 -    val (output_dir, browser_info) =
    1.83 -      if (system_mode) (Path.explode("~~/heaps/$ML_IDENTIFIER"), Path.explode("~~/browser_info"))
    1.84 -      else (Path.explode("$ISABELLE_OUTPUT"), Path.explode("$ISABELLE_BROWSER_INFO"))
    1.85 +    def make_stamp(name: String): String =
    1.86 +      sources_stamp(queue(name).digest :: deps.sources(name))
    1.87 +
    1.88 +    val (input_dirs, output_dir, browser_info) =
    1.89 +      if (system_mode) {
    1.90 +        val output_dir = Path.explode("~~/heaps/$ML_IDENTIFIER")
    1.91 +        (List(output_dir), output_dir, Path.explode("~~/browser_info"))
    1.92 +      }
    1.93 +      else {
    1.94 +        val output_dir = Path.explode("$ISABELLE_OUTPUT")
    1.95 +        (output_dir :: Isabelle_System.find_logics_dirs(), output_dir,
    1.96 +         Path.explode("$ISABELLE_BROWSER_INFO"))
    1.97 +      }
    1.98  
    1.99      // prepare log dir
   1.100 -    val log_dir = output_dir + Path.explode("log")
   1.101 -    log_dir.file.mkdirs()
   1.102 +    (output_dir + LOG).file.mkdirs()
   1.103  
   1.104      // scheduler loop
   1.105      @tailrec def loop(
   1.106 @@ -455,46 +488,51 @@
   1.107        results: Map[String, Int]): Map[String, Int] =
   1.108      {
   1.109        if (pending.is_empty) results
   1.110 -      else if (running.exists({ case (_, job) => job.is_finished })) {
   1.111 +      else if (running.exists({ case (_, job) => job.is_finished }))
   1.112 +      { // finish job
   1.113          val (name, job) = running.find({ case (_, job) => job.is_finished }).get
   1.114  
   1.115          val (out, err, rc) = job.join
   1.116          echo(Library.trim_line(err))
   1.117  
   1.118 -        val log = log_dir + Path.basic(name)
   1.119          if (rc == 0) {
   1.120 -          val sources =
   1.121 -            (queue(name).digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
   1.122 -              .mkString("sources: ", " ", "\n")
   1.123 -          val heap =
   1.124 -            job.output_path.map(_.file) match {
   1.125 -              case Some(file) =>
   1.126 -                "heap: " + file.length.toString + " " + file.lastModified.toString + "\n"
   1.127 -              case None => ""
   1.128 -            }
   1.129 -          File.write_gzip(log.ext("gz"), sources + heap + out)
   1.130 +          val sources = make_stamp(name)
   1.131 +          val heap = heap_stamp(job.output_path)
   1.132 +          File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out)
   1.133          }
   1.134          else {
   1.135 -          File.write(log, out)
   1.136 +          File.write(output_dir + log(name), out)
   1.137            echo(name + " FAILED")
   1.138 -          echo("(see also " + log.file + ")")
   1.139 +          echo("(see also " + log(name).file.toString + ")")
   1.140            val lines = split_lines(out)
   1.141            val tail = lines.drop(lines.length - 20 max 0)
   1.142            echo("\n" + cat_lines(tail))
   1.143          }
   1.144          loop(pending - name, running - name, results + (name -> rc))
   1.145        }
   1.146 -      else if (running.size < (max_jobs max 1)) {
   1.147 +      else if (running.size < (max_jobs max 1))
   1.148 +      { // check/start next job
   1.149          pending.dequeue(running.isDefinedAt(_)) match {
   1.150            case Some((name, info)) =>
   1.151 -            if (no_build) {
   1.152 -              loop(pending - name, running, results + (name -> 0))
   1.153 +            val output =
   1.154 +              if (build_images || queue.is_inner(name))
   1.155 +                Some(output_dir + Path.basic(name))
   1.156 +              else None
   1.157 +
   1.158 +            val current =
   1.159 +            {
   1.160 +              input_dirs.find(dir => (dir + log_gz(name)).file.isFile) match {
   1.161 +                case Some(dir) =>
   1.162 +                  check_stamps(dir, name) match {
   1.163 +                    case Some((s, h)) => s == make_stamp(name) && (h || output.isEmpty)
   1.164 +                    case None => false
   1.165 +                  }
   1.166 +                case None => false
   1.167 +              }
   1.168              }
   1.169 +            if (current || no_build)
   1.170 +              loop(pending - name, running, results + (name -> (if (current) 0 else 1)))
   1.171              else if (info.parent.map(results(_)).forall(_ == 0)) {
   1.172 -              val output =
   1.173 -                if (build_images || queue.is_inner(name))
   1.174 -                  Some(output_dir + Path.basic(name))
   1.175 -                else None
   1.176                echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
   1.177                val job = start_job(name, info, output, info.options, timing, verbose, browser_info)
   1.178                loop(pending, running + (name -> job), results)
   1.179 @@ -511,7 +549,7 @@
   1.180  
   1.181      val results = loop(queue, Map.empty, Map.empty)
   1.182      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
   1.183 -    if (rc != 0) {
   1.184 +    if (rc != 0 && (verbose || !no_build)) {
   1.185        val unfinished = (for ((name, r) <- results.iterator if r != 0) yield name).toList.sorted
   1.186        echo("Unfinished session(s): " + commas(unfinished))
   1.187      }