read/write dependency information;
authorwenzelm
Tue Jul 24 23:01:55 2012 +0200 (2012-07-24)
changeset 4849400eb5be9e76b
parent 48493 142ab4ff8fa8
child 48495 bf5b45870110
read/write dependency information;
tuned signature;
src/Pure/General/file.scala
src/Pure/System/build.scala
     1.1 --- a/src/Pure/General/file.scala	Tue Jul 24 22:00:12 2012 +0200
     1.2 +++ b/src/Pure/General/file.scala	Tue Jul 24 23:01:55 2012 +0200
     1.3 @@ -37,10 +37,10 @@
     1.4  
     1.5    /* write */
     1.6  
     1.7 -  private def write_file(file: JFile, text: CharSequence, zip: Boolean)
     1.8 +  private def write_file(file: JFile, text: CharSequence, gzip: Boolean)
     1.9    {
    1.10      val stream1 = new FileOutputStream(file)
    1.11 -    val stream2 = if (zip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
    1.12 +    val stream2 = if (gzip) new GZIPOutputStream(new BufferedOutputStream(stream1)) else stream1
    1.13      val writer = new BufferedWriter(new OutputStreamWriter(stream2, Standard_System.charset))
    1.14      try { writer.append(text) }
    1.15      finally { writer.close }
    1.16 @@ -49,8 +49,8 @@
    1.17    def write(file: JFile, text: CharSequence): Unit = write_file(file, text, false)
    1.18    def write(path: Path, text: CharSequence): Unit = write(path.file, text)
    1.19  
    1.20 -  def write_zip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
    1.21 -  def write_zip(path: Path, text: CharSequence): Unit = write_zip(path.file, text)
    1.22 +  def write_gzip(file: JFile, text: CharSequence): Unit = write_file(file, text, true)
    1.23 +  def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
    1.24  
    1.25  
    1.26    /* copy */
     2.1 --- a/src/Pure/System/build.scala	Tue Jul 24 22:00:12 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Tue Jul 24 23:01:55 2012 +0200
     2.3 @@ -7,7 +7,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 -import java.io.{File => JFile}
     2.8 +import java.io.{File => JFile, BufferedInputStream, FileInputStream,
     2.9 +  BufferedReader, InputStreamReader, IOException}
    2.10 +import java.util.zip.GZIPInputStream
    2.11  
    2.12  import scala.collection.mutable
    2.13  import scala.annotation.tailrec
    2.14 @@ -301,6 +303,18 @@
    2.15      def sources(name: String): List[(Path, SHA1.Digest)] = deps(name).sources
    2.16    }
    2.17  
    2.18 +  private def read_deps(file: JFile): List[String] =
    2.19 +    if (file.isFile) {
    2.20 +      val stream = new GZIPInputStream (new BufferedInputStream(new FileInputStream(file)))
    2.21 +      val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
    2.22 +      try {
    2.23 +        List(reader.readLine).filter(_.startsWith("sources:")) :::
    2.24 +        List(reader.readLine).filter(_.startsWith("heap:"))
    2.25 +      }
    2.26 +      finally { reader.close }
    2.27 +    }
    2.28 +    else Nil
    2.29 +
    2.30    def dependencies(verbose: Boolean, queue: Session.Queue): Deps =
    2.31      Deps((Map.empty[String, Node] /: queue.topological_order)(
    2.32        { case (deps, (name, info)) =>
    2.33 @@ -344,7 +358,8 @@
    2.34  
    2.35    /* jobs */
    2.36  
    2.37 -  private class Job(cwd: JFile, env: Map[String, String], script: String, args: String)
    2.38 +  private class Job(cwd: JFile, env: Map[String, String], script: String, args: String,
    2.39 +    val output_path: Option[Path])
    2.40    {
    2.41      private val args_file = File.tmp_file("args")
    2.42      private val env1 = env + ("ARGS_FILE" -> Isabelle_System.posix_path(args_file.getPath))
    2.43 @@ -358,7 +373,7 @@
    2.44      def join: (String, String, Int) = { val res = result.join; args_file.delete; res }
    2.45    }
    2.46  
    2.47 -  private def start_job(name: String, info: Session.Info, output: Option[String],
    2.48 +  private def start_job(name: String, info: Session.Info, output_path: Option[Path],
    2.49      options: Options, timing: Boolean, verbose: Boolean, browser_info: Path): Job =
    2.50    {
    2.51      // global browser info dir
    2.52 @@ -376,15 +391,18 @@
    2.53      val parent = info.parent.getOrElse("")
    2.54      val parent_base_name = info.parent_base_name.getOrElse("")
    2.55  
    2.56 +    val output =
    2.57 +      output_path match { case Some(p) => Isabelle_System.standard_path(p) case None => "" }
    2.58 +
    2.59      val cwd = info.dir.file
    2.60 -    val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output.getOrElse(""))
    2.61 +    val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output)
    2.62      val script =
    2.63        if (is_pure(name)) "./build " + name + " \"$OUTPUT\""
    2.64        else {
    2.65          """
    2.66          . "$ISABELLE_HOME/lib/scripts/timestart.bash"
    2.67          """ +
    2.68 -          (if (output.isDefined)
    2.69 +          (if (output_path.isDefined)
    2.70              """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -q -w "$INPUT" "$OUTPUT" """
    2.71            else
    2.72              """ "$ISABELLE_PROCESS" -e "Build.build \"$ARGS_FILE\";" -r -q "$INPUT" """) +
    2.73 @@ -405,10 +423,10 @@
    2.74        import XML.Encode._
    2.75            pair(bool, pair(Options.encode, pair(bool, pair(bool, pair(Path.encode, pair(string,
    2.76              pair(string, pair(string, list(pair(Options.encode, list(Path.encode)))))))))))(
    2.77 -          (output.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
    2.78 +          (output_path.isDefined, (options, (timing, (verbose, (browser_info, (parent_base_name,
    2.79              (name, (info.base_name, info.theories)))))))))
    2.80      }
    2.81 -    new Job(cwd, env, script, YXML.string_of_body(args_xml))
    2.82 +    new Job(cwd, env, script, YXML.string_of_body(args_xml), output_path)
    2.83    }
    2.84  
    2.85  
    2.86 @@ -448,7 +466,13 @@
    2.87            val sources =
    2.88              (queue(name).digest :: deps.sources(name).map(_._2)).map(_.toString).sorted
    2.89                .mkString("sources: ", " ", "\n")
    2.90 -          File.write_zip(log.ext("gz"), sources + out)
    2.91 +          val heap =
    2.92 +            job.output_path.map(_.file) match {
    2.93 +              case Some(file) =>
    2.94 +                "heap: " + file.length.toString + " " + file.lastModified.toString + "\n"
    2.95 +              case None => ""
    2.96 +            }
    2.97 +          File.write_gzip(log.ext("gz"), sources + heap + out)
    2.98          }
    2.99          else {
   2.100            File.write(log, out)
   2.101 @@ -469,7 +493,7 @@
   2.102              else if (info.parent.map(results(_)).forall(_ == 0)) {
   2.103                val output =
   2.104                  if (build_images || queue.is_inner(name))
   2.105 -                  Some(Isabelle_System.standard_path(output_dir + Path.basic(name)))
   2.106 +                  Some(output_dir + Path.basic(name))
   2.107                  else None
   2.108                echo((if (output.isDefined) "Building " else "Running ") + name + " ...")
   2.109                val job = start_job(name, info, output, info.options, timing, verbose, browser_info)