# HG changeset patch # User wenzelm # Date 1343851914 -7200 # Node ID 675988e64bf921bced107052e60ae594b10466d8 # Parent 22d65e375c01e3d5c59c1dbcff531783fac4c7d0 store parent heap stamp as well -- needs to be propagated through the build hierarchy; misc tuning; diff -r 22d65e375c01 -r 675988e64bf9 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Wed Aug 01 19:53:20 2012 +0200 +++ b/src/Pure/System/build.scala Wed Aug 01 22:11:54 2012 +0200 @@ -330,7 +330,7 @@ /* jobs */ private class Job(dir: Path, env: Map[String, String], script: String, args: String, - output: Path, do_output: Boolean) + val parent_heap: String, output: Path, do_output: Boolean) { private val args_file = File.tmp_file("args") private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath)) @@ -345,8 +345,8 @@ def output_path: Option[Path] = if (do_output) Some(output) else None } - private def start_job(name: String, info: Session.Info, output: Path, do_output: Boolean, - options: Options, verbose: Boolean, browser_info: Path): Job = + private def start_job(name: String, info: Session.Info, parent_heap: String, + output: Path, do_output: Boolean, options: Options, verbose: Boolean, browser_info: Path): Job = { // global browser info dir if (options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file) @@ -401,7 +401,7 @@ (do_output, (options, (verbose, (browser_info, (parent, (name, info.theories))))))) } - new Job(info.dir, env, script, YXML.string_of_body(args_xml), output, do_output) + new Job(info.dir, env, script, YXML.string_of_body(args_xml), parent_heap, output, do_output) } @@ -414,10 +414,12 @@ private def sources_stamp(digests: List[SHA1.Digest]): String = digests.map(_.toString).sorted.mkString("sources: ", " ", "") - private def heap_stamp(output: Option[Path]): String = + private val no_heap: String = "heap: -" + + private def heap_stamp(heap: Option[Path]): String = { "heap: " + - (output match { + (heap match { case Some(path) => val file = path.file if (file.isFile) file.length.toString + " " + file.lastModified.toString @@ -426,19 +428,19 @@ }) } - private def check_stamps(dir: Path, name: String): Option[(String, Boolean)] = - { - val file = (dir + log_gz(name)).file - if (file.isFile) { - val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(file))) + private def read_stamps(path: Path): Option[(String, String, String)] = + if (path.is_file) { + val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(path.file))) val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset)) - val (s, h) = try { (reader.readLine, reader.readLine) } finally { reader.close } - if (s != null && s.startsWith("sources: ") && h != null && h.startsWith("heap: ") && - h == heap_stamp(Some(dir + Path.basic(name)))) Some((s, h != "heap: -")) + val (s, h1, h2) = + try { (reader.readLine, reader.readLine, reader.readLine) } + finally { reader.close } + if (s != null && s.startsWith("sources: ") && + h1 != null && h1.startsWith("heap: ") && + h2 != null && h2.startsWith("heap: ")) Some((s, h1, h2)) else None } else None - } /* build */ @@ -489,10 +491,12 @@ } // scheduler loop + case class Result(current: Boolean, heap: String, rc: Int) + @tailrec def loop( pending: Session.Queue, running: Map[String, Job], - results: Map[String, (Boolean, Int)]): Map[String, (Boolean, Int)] = + results: Map[String, Result]): Map[String, Result] = { if (pending.is_empty) results else @@ -503,60 +507,74 @@ val (out, err, rc) = job.join echo(Library.trim_line(err)) - if (rc == 0) { - val sources = make_stamp(name) - val heap = heap_stamp(job.output_path) - (output_dir + log(name)).file.delete - File.write_gzip(output_dir + log_gz(name), sources + "\n" + heap + "\n" + out) - } - else { - (output_dir + log_gz(name)).file.delete - File.write(output_dir + log(name), out) - echo(name + " FAILED") - echo("(see also " + (output_dir + log(name)).file.toString + ")") - val lines = split_lines(out) - val tail = lines.drop(lines.length - 20 max 0) - echo("\n" + cat_lines(tail)) - } - loop(pending - name, running - name, results + (name -> (false, rc))) + val heap = + if (rc == 0) { + (output_dir + log(name)).file.delete + + val sources = make_stamp(name) + val heap = heap_stamp(job.output_path) + File.write_gzip(output_dir + log_gz(name), + sources + "\n" + job.parent_heap + "\n" + heap + "\n" + out) + + heap + } + else { + (output_dir + Path.basic(name)).file.delete + (output_dir + log_gz(name)).file.delete + + File.write(output_dir + log(name), out) + echo(name + " FAILED") + echo("(see also " + (output_dir + log(name)).file.toString + ")") + val lines = split_lines(out) + val tail = lines.drop(lines.length - 20 max 0) + echo("\n" + cat_lines(tail)) + + no_heap + } + loop(pending - name, running - name, results + (name -> Result(false, heap, rc))) case None if (running.size < (max_jobs max 1)) => // check/start next job pending.dequeue(running.isDefinedAt(_)) match { case Some((name, info)) => - val parent_result = info.parent.map(results(_)) - val parent_current = parent_result.forall(_._1) - val parent_ok = parent_result.forall(_._2 == 0) - + val parent_result = + info.parent match { + case None => Result(true, no_heap, 0) + case Some(parent) => results(parent) + } val output = output_dir + Path.basic(name) val do_output = build_heap || queue.is_inner(name) - val current = + val (current, heap) = { input_dirs.find(dir => (dir + log_gz(name)).is_file) match { case Some(dir) => - check_stamps(dir, name) match { - case Some((s, h)) => s == make_stamp(name) && (h || !do_output) - case None => false + read_stamps(dir + log_gz(name)) match { + case Some((s, h1, h2)) => + val heap = heap_stamp(Some(dir + Path.basic(name))) + (s == make_stamp(name) && h1 == parent_result.heap && h2 == heap && + !(do_output && heap == no_heap), heap) + case None => (false, no_heap) } - case None => false + case None => (false, no_heap) } } - val all_current = current && parent_current + val all_current = current && parent_result.current if (all_current) - loop(pending - name, running, results + (name -> (true, 0))) + loop(pending - name, running, results + (name -> Result(true, heap, 0))) else if (no_build) - loop(pending - name, running, results + (name -> (false, 1))) - else if (parent_ok) { + loop(pending - name, running, results + (name -> Result(false, heap, 1))) + else if (parent_result.rc == 0) { echo((if (do_output) "Building " else "Running ") + name + " ...") val job = - start_job(name, info, output, do_output, info.options, verbose, browser_info) + start_job(name, info, parent_result.heap, output, do_output, + info.options, verbose, browser_info) loop(pending, running + (name -> job), results) } else { echo(name + " CANCELLED") - loop(pending - name, running, results + (name -> (false, 1))) + loop(pending - name, running, results + (name -> Result(false, heap, 1))) } case None => sleep(); loop(pending, running, results) } @@ -571,10 +589,10 @@ } else loop(queue, Map.empty, Map.empty) - val rc = (0 /: results)({ case (rc1, (_, (_, rc2))) => rc1 max rc2 }) + val rc = (0 /: results)({ case (rc1, (_, res)) => rc1 max res.rc }) if (rc != 0 && (verbose || !no_build)) { val unfinished = - (for ((name, (_, r)) <- results.iterator if r != 0) yield name).toList.sorted + (for ((name, res) <- results.iterator if res.rc != 0) yield name).toList.sorted echo("Unfinished session(s): " + commas(unfinished)) } rc