cleanup session output before starting build job;
authorwenzelm
Sat May 05 13:56:51 2018 +0200 (12 months ago)
changeset 680869e1c670301b8
parent 68082 b25ccd85b1fd
child 68087 dac267cd51fe
cleanup session output before starting build job;
tuned signature;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri May 04 22:26:25 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 05 13:56:51 2018 +0200
     1.3 @@ -1003,6 +1003,10 @@
     1.4  
     1.5      def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
     1.6  
     1.7 +    def output_database(name: String): Path = output_dir + database(name)
     1.8 +    def output_log(name: String): Path = output_dir + log(name)
     1.9 +    def output_log_gz(name: String): Path = output_dir + log_gz(name)
    1.10 +
    1.11  
    1.12      /* input */
    1.13  
    1.14 @@ -1028,6 +1032,15 @@
    1.15  
    1.16      /* session info */
    1.17  
    1.18 +    def init_session_info(db: SQL.Database, name: String)
    1.19 +    {
    1.20 +      db.transaction {
    1.21 +        db.create_table(Session_Info.table)
    1.22 +        db.using_statement(
    1.23 +          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    1.24 +      }
    1.25 +    }
    1.26 +
    1.27      def write_session_info(
    1.28        db: SQL.Database,
    1.29        name: String,
    1.30 @@ -1035,9 +1048,6 @@
    1.31        build: Build.Session_Info)
    1.32      {
    1.33        db.transaction {
    1.34 -        db.create_table(Session_Info.table)
    1.35 -        db.using_statement(
    1.36 -          Session_Info.table.delete(Session_Info.session_name.where_equal(name)))(_.execute)
    1.37          db.using_statement(Session_Info.table.insert())(stmt =>
    1.38          {
    1.39            stmt.string(1) = name
     2.1 --- a/src/Pure/Tools/build.scala	Fri May 04 22:26:25 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sat May 05 13:56:51 2018 +0200
     2.3 @@ -32,10 +32,11 @@
     2.4  
     2.5    private object Queue
     2.6    {
     2.7 -    def load_timings(progress: Progress, store: Sessions.Store, name: String)
     2.8 -      : (List[Properties.T], Double) =
     2.9 +    type Timings = (List[Properties.T], Double)
    2.10 +
    2.11 +    def load_timings(progress: Progress, store: Sessions.Store, name: String): Timings =
    2.12      {
    2.13 -      val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
    2.14 +      val no_timings: Timings = (Nil, 0.0)
    2.15  
    2.16        store.find_database(name) match {
    2.17          case None => no_timings
    2.18 @@ -184,7 +185,6 @@
    2.19    {
    2.20      val output = store.output_dir + Path.basic(name)
    2.21      def output_path: Option[Path] = if (do_output) Some(output) else None
    2.22 -    output.file.delete
    2.23  
    2.24      val options =
    2.25        numa_node match {
    2.26 @@ -448,14 +448,19 @@
    2.27  
    2.28      store.prepare_output()
    2.29  
    2.30 -    // optional cleanup
    2.31 +    // cleanup
    2.32 +    def cleanup(name: String, echo: Boolean = false)
    2.33 +    {
    2.34 +      val files =
    2.35 +        List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    2.36 +          map(store.output_dir + _).filter(_.is_file)
    2.37 +      if (files.nonEmpty) progress.echo_if(echo, "Cleaning " + name + " ...")
    2.38 +      val res = files.map(p => p.file.delete)
    2.39 +      if (!res.forall(ok => ok)) progress.echo_if(echo, name + " FAILED to delete")
    2.40 +    }
    2.41      if (clean_build) {
    2.42        for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) {
    2.43 -        val files =
    2.44 -          List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    2.45 -            map(store.output_dir + _).filter(_.is_file)
    2.46 -        if (files.nonEmpty) progress.echo("Cleaning " + name + " ...")
    2.47 -        if (!files.forall(p => p.file.delete)) progress.echo(name + " FAILED to delete")
    2.48 +        cleanup(name, echo = true)
    2.49        }
    2.50      }
    2.51  
    2.52 @@ -507,7 +512,7 @@
    2.53                val tail = job.info.options.int("process_output_tail")
    2.54                process_result.copy(
    2.55                  out_lines =
    2.56 -                  "(see also " + (store.output_dir + store.log(name)).file.toString + ")" ::
    2.57 +                  "(see also " + store.output_log(name).file.toString + ")" ::
    2.58                    (if (tail == 0) log_lines else log_lines.drop(log_lines.length - tail max 0)))
    2.59              }
    2.60  
    2.61 @@ -515,29 +520,22 @@
    2.62              // write log file
    2.63              val heap_stamp =
    2.64                if (process_result.ok) {
    2.65 -                (store.output_dir + store.log(name)).file.delete
    2.66                  val heap_stamp =
    2.67                    for (path <- job.output_path if path.is_file)
    2.68                      yield Sessions.write_heap_digest(path)
    2.69  
    2.70 -                File.write_gzip(store.output_dir + store.log_gz(name), terminate_lines(log_lines))
    2.71 +                File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
    2.72  
    2.73                  heap_stamp
    2.74                }
    2.75                else {
    2.76 -                (store.output_dir + Path.basic(name)).file.delete
    2.77 -                (store.output_dir + store.log_gz(name)).file.delete
    2.78 -
    2.79 -                File.write(store.output_dir + store.log(name), terminate_lines(log_lines))
    2.80 +                File.write(store.output_log(name), terminate_lines(log_lines))
    2.81  
    2.82                  None
    2.83                }
    2.84  
    2.85              // write database
    2.86              {
    2.87 -              val database = store.output_dir + store.database(name)
    2.88 -              database.file.delete
    2.89 -
    2.90                val build_log =
    2.91                  Build_Log.Log_File(name, process_result.out_lines).
    2.92                    parse_session_info(
    2.93 @@ -546,7 +544,7 @@
    2.94                      ml_statistics = true,
    2.95                      task_statistics = true)
    2.96  
    2.97 -              using(SQLite.open_database(database))(db =>
    2.98 +              using(SQLite.open_database(store.output_database(name)))(db =>
    2.99                  store.write_session_info(db, name,
   2.100                    build_log =
   2.101                      if (process_result.timeout) build_log.error("Timeout") else build_log,
   2.102 @@ -609,8 +607,13 @@
   2.103                      results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
   2.104                  }
   2.105                  else if (ancestor_results.forall(_.ok) && !progress.stopped) {
   2.106 +                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   2.107 +
   2.108 +                  cleanup(name)
   2.109 +                  using(SQLite.open_database(store.output_database(name)))(db =>
   2.110 +                    store.init_session_info(db, name))
   2.111 +
   2.112                    val numa_node = numa_nodes.next(used_node(_))
   2.113 -                  progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
   2.114                    val job =
   2.115                      new Job(progress, name, info, selected_sessions, deps, store, do_output,
   2.116                        verbose, pide, numa_node, queue.command_timings(name))