src/Pure/Tools/build.scala
changeset 68086 9e1c670301b8
parent 67852 f701a1d5d852
child 68088 0763d4eb3ebc
     1.1 --- a/src/Pure/Tools/build.scala	Fri May 04 22:26:25 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Sat May 05 13:56:51 2018 +0200
     1.3 @@ -32,10 +32,11 @@
     1.4  
     1.5    private object Queue
     1.6    {
     1.7 -    def load_timings(progress: Progress, store: Sessions.Store, name: String)
     1.8 -      : (List[Properties.T], Double) =
     1.9 +    type Timings = (List[Properties.T], Double)
    1.10 +
    1.11 +    def load_timings(progress: Progress, store: Sessions.Store, name: String): Timings =
    1.12      {
    1.13 -      val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
    1.14 +      val no_timings: Timings = (Nil, 0.0)
    1.15  
    1.16        store.find_database(name) match {
    1.17          case None => no_timings
    1.18 @@ -184,7 +185,6 @@
    1.19    {
    1.20      val output = store.output_dir + Path.basic(name)
    1.21      def output_path: Option[Path] = if (do_output) Some(output) else None
    1.22 -    output.file.delete
    1.23  
    1.24      val options =
    1.25        numa_node match {
    1.26 @@ -448,14 +448,19 @@
    1.27  
    1.28      store.prepare_output()
    1.29  
    1.30 -    // optional cleanup
    1.31 +    // cleanup
    1.32 +    def cleanup(name: String, echo: Boolean = false)
    1.33 +    {
    1.34 +      val files =
    1.35 +        List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    1.36 +          map(store.output_dir + _).filter(_.is_file)
    1.37 +      if (files.nonEmpty) progress.echo_if(echo, "Cleaning " + name + " ...")
    1.38 +      val res = files.map(p => p.file.delete)
    1.39 +      if (!res.forall(ok => ok)) progress.echo_if(echo, name + " FAILED to delete")
    1.40 +    }
    1.41      if (clean_build) {
    1.42        for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
    1.43 -        val files =
    1.44 -          List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    1.45 -            map(store.output_dir + _).filter(_.is_file)
    1.46 -        if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
    1.47 -        if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
    1.48 +        cleanup(name, echo = true)
    1.49        }
    1.50      }
    1.51  
    1.52 @@ -507,7 +512,7 @@
    1.53                val tail = job.info.options.int("process_output_tail")
    1.54                process_result.copy(
    1.55                  out_lines =
    1.56 -                  "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
    1.57 +                  "(see also " + store.output_log(name).file.toString + ")" ::
    1.58                    (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
    1.59              }
    1.60  
    1.61 @@ -515,29 +520,22 @@
    1.62              // write log file
    1.63              val heap_stamp =
    1.64                if (process_result.ok) {
    1.65 -                (store.output_dir + store.log(name)).file.delete
    1.66                  val heap_stamp =
    1.67                    for (path <- job.output_path if path.is_file)
    1.68                      yield Sessions.write_heap_digest(path)
    1.69  
    1.70 -                File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
    1.71 +                File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
    1.72  
    1.73                  heap_stamp
    1.74                }
    1.75                else {
    1.76 -                (store.output_dir + Path.basic(name)).file.delete
    1.77 -                (store.output_dir + store.log_gz(name)).file.delete
    1.78 -
    1.79 -                File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
    1.80 +                File.write(store.output_log(name), terminate_lines(log_lines))
    1.81  
    1.82                  None
    1.83                }
    1.84  
    1.85              // write database
    1.86              {
    1.87 -              val database = store.output_dir + store.database(name)
    1.88 -              database.file.delete
    1.89 -
    1.90                val build_log =
    1.91                  Build_Log.Log_File(name, process_result.out_lines).
    1.92                    parse_session_info(
    1.93 @@ -546,7 +544,7 @@
    1.94                      ml_statistics = true,
    1.95                      task_statistics = true)
    1.96  
    1.97 -              using(SQLite.open_database(database))(db =>
    1.98 +              using(SQLite.open_database(store.output_database(name)))(db =>
    1.99                  store.write_session_info(db, name,
   1.100                    build_log =
   1.101                      if (process_result.timeout) build_log.error("Timeout") else build_log,
   1.102 @@ -609,8 +607,13 @@
   1.103                      results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   1.104                  }
   1.105                  else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   1.106 +                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   1.107 +
   1.108 +                  cleanup(name)
   1.109 +                  using(SQLite.open_database(store.output_database(name)))(db =>
   1.110 +                    store.init_session_info(db, name))
   1.111 +
   1.112                    val numa_node = numa_nodes.next(used_node(_))
   1.113 -                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   1.114                    val job =
   1.115                      new Job(progress, name, info, selected_sessions, deps, store, do_output,
   1.116                        verbose, pide, numa_node, queue.command_timings(name))