tuned;
authorwenzelm
Fri May 18 21:08:24 2018 +0200 (14 months ago)
changeset 68213bb93511c7e8f
parent 68212 5a59fded83c7
child 68214 b0e2a19df95b
tuned;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Fri May 18 21:05:10 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri May 18 21:08:24 2018 +0200
     1.3 @@ -483,7 +483,7 @@
     1.4      // scheduler loop
     1.5      case class Result(
     1.6        current: Boolean,
     1.7 -      heap_stamp: Option[String],
     1.8 +      heap_digest: Option[String],
     1.9        process: Option[Process_Result],
    1.10        info: Sessions.Info)
    1.11      {
    1.12 @@ -534,15 +534,15 @@
    1.13  
    1.14  
    1.15              // write log file
    1.16 -            val heap_stamp =
    1.17 +            val heap_digest =
    1.18                if (process_result.ok) {
    1.19 -                val heap_stamp =
    1.20 +                val heap_digest =
    1.21                    for (path <- job.output_path if path.is_file)
    1.22                      yield Sessions.write_heap_digest(path)
    1.23  
    1.24                  File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
    1.25  
    1.26 -                heap_stamp
    1.27 +                heap_digest
    1.28                }
    1.29                else {
    1.30                  File.write(store.output_log(name), terminate_lines(log_lines))
    1.31 @@ -565,7 +565,7 @@
    1.32                    build_log =
    1.33                      if (process_result.timeout) build_log.error("Timeout") else build_log,
    1.34                    build =
    1.35 -                    Session_Info(sources_stamp(deps, name), input_heaps, heap_stamp,
    1.36 +                    Session_Info(sources_stamp(deps, name), input_heaps, heap_digest,
    1.37                        process_result.rc)))
    1.38              }
    1.39  
    1.40 @@ -580,7 +580,7 @@
    1.41              }
    1.42  
    1.43              loop(pending - name, running - name,
    1.44 -              results + (name -> Result(false, heap_stamp, Some(process_result_tail), job.info)))
    1.45 +              results + (name -> Result(false, heap_digest, Some(process_result_tail), job.info)))
    1.46              //}}}
    1.47            case None if running.size < (max_jobs max 1) =>
    1.48              //{{{ check/start next job
    1.49 @@ -589,26 +589,26 @@
    1.50                  val ancestor_results =
    1.51                    deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
    1.52                      map(results(_))
    1.53 -                val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    1.54 +                val ancestor_heaps = ancestor_results.flatMap(_.heap_digest)
    1.55  
    1.56                  val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
    1.57  
    1.58 -                val (current, heap_stamp) =
    1.59 +                val (current, heap_digest) =
    1.60                  {
    1.61                    store.try_open_database(name) match {
    1.62                      case Some(db) =>
    1.63                        try {
    1.64                          store.read_build(db, name) match {
    1.65                            case Some(build) =>
    1.66 -                            val heap_stamp = store.find_heap_digest(name)
    1.67 +                            val heap_digest = store.find_heap_digest(name)
    1.68                              val current =
    1.69                                !fresh_build &&
    1.70                                build.ok &&
    1.71                                build.sources == sources_stamp(deps, name) &&
    1.72                                build.input_heaps == ancestor_heaps &&
    1.73 -                              build.output_heap == heap_stamp &&
    1.74 -                              !(do_output && heap_stamp.isEmpty)
    1.75 -                            (current, heap_stamp)
    1.76 +                              build.output_heap == heap_digest &&
    1.77 +                              !(do_output && heap_digest.isEmpty)
    1.78 +                            (current, heap_digest)
    1.79                            case None => (false, None)
    1.80                          }
    1.81                        } finally { db.close }
    1.82 @@ -619,11 +619,11 @@
    1.83  
    1.84                  if (all_current)
    1.85                    loop(pending - name, running,
    1.86 -                    results + (name -> Result(true, heap_stamp, Some(Process_Result(0)), info)))
    1.87 +                    results + (name -> Result(true, heap_digest, Some(Process_Result(0)), info)))
    1.88                  else if (no_build) {
    1.89                    if (verbose) progress.echo("Skipping " + name + " ...")
    1.90                    loop(pending - name, running,
    1.91 -                    results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
    1.92 +                    results + (name -> Result(false, heap_digest, Some(Process_Result(1)), info)))
    1.93                  }
    1.94                  else if (ancestor_results.forall(_.ok) && !progress.stopped) {
    1.95                    progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
    1.96 @@ -641,7 +641,7 @@
    1.97                  else {
    1.98                    progress.echo(name + " CANCELLED")
    1.99                    loop(pending - name, running,
   1.100 -                    results + (name -> Result(false, heap_stamp, None, info)))
   1.101 +                    results + (name -> Result(false, heap_digest, None, info)))
   1.102                  }
   1.103                case None => sleep(); loop(pending, running, results)
   1.104              }