clarified handling of output heap;
authorwenzelm
Sat May 19 14:47:54 2018 +0200 (14 months ago)
changeset 682173e90b88b0fc2
parent 68216 c0f86aee29db
child 68218 92050155593e
clarified handling of output heap;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat May 19 14:12:44 2018 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat May 19 14:47:54 2018 +0200
     1.3 @@ -1005,6 +1005,7 @@
     1.4  
     1.5      def prepare_output() { Isabelle_System.mkdirs(output_dir + Path.basic("log")) }
     1.6  
     1.7 +    def output_heap(name: String): Path = output_dir + Path.basic(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  
     2.1 --- a/src/Pure/Tools/build.scala	Sat May 19 14:12:44 2018 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Sat May 19 14:47:54 2018 +0200
     2.3 @@ -179,9 +179,6 @@
     2.4      val numa_node: Option[Int],
     2.5      command_timings: List[Properties.T])
     2.6    {
     2.7 -    val output = store.output_dir + Path.basic(name)
     2.8 -    def output_path: Option[Path] = if (do_output) Some(output) else None
     2.9 -
    2.10      val options =
    2.11        numa_node match {
    2.12          case None => info.options
    2.13 @@ -224,7 +221,8 @@
    2.14  
    2.15          def save_heap: String =
    2.16            (if (info.theories.isEmpty) "" else "ML_Heap.share_common_data (); ") +
    2.17 -            "ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(output))
    2.18 +            "ML_Heap.save_child " +
    2.19 +            ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))
    2.20  
    2.21          if (pide && !Sessions.is_pure(name)) {
    2.22            val resources = new Resources(deps(parent))
    2.23 @@ -311,19 +309,19 @@
    2.24        else None
    2.25      }
    2.26  
    2.27 -    def join: Process_Result =
    2.28 +    def join: (Process_Result, Option[String]) =
    2.29      {
    2.30 -      val result = future_result.join
    2.31 -      val export_result =
    2.32 +      val result0 = future_result.join
    2.33 +      val result1 =
    2.34          export_consumer.shutdown(close = true).map(Output.error_message_text(_)) match {
    2.35 -          case Nil => result
    2.36 -          case errs if result.ok => result.copy(rc = 1).errors(errs)
    2.37 -          case errs => result.errors(errs)
    2.38 +          case Nil => result0
    2.39 +          case errs if result0.ok => result0.copy(rc = 1).errors(errs)
    2.40 +          case errs => result0.errors(errs)
    2.41          }
    2.42  
    2.43        Isabelle_System.rm_tree(export_tmp_dir)
    2.44  
    2.45 -      if (export_result.ok)
    2.46 +      if (result1.ok)
    2.47          Present.finish(progress, store.browser_info, graph_file, info, name)
    2.48  
    2.49        graph_file.delete
    2.50 @@ -334,11 +332,19 @@
    2.51            case Some(request) => !request.cancel
    2.52          }
    2.53  
    2.54 -      if (export_result.interrupted) {
    2.55 -        if (was_timeout) export_result.error(Output.error_message_text("Timeout")).was_timeout
    2.56 -        else export_result.error(Output.error_message_text("Interrupt"))
    2.57 -      }
    2.58 -      else export_result
    2.59 +      val result2 =
    2.60 +        if (result1.interrupted) {
    2.61 +          if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout
    2.62 +          else result1.error(Output.error_message_text("Interrupt"))
    2.63 +        }
    2.64 +        else result1
    2.65 +
    2.66 +      val heap_digest =
    2.67 +        if (result2.ok && do_output && store.output_heap(name).is_file)
    2.68 +          Some(Sessions.write_heap_digest(store.output_heap(name)))
    2.69 +        else None
    2.70 +
    2.71 +      (result2, heap_digest)
    2.72      }
    2.73    }
    2.74  
    2.75 @@ -517,7 +523,7 @@
    2.76            case Some((name, (input_heaps, job))) =>
    2.77              //{{{ finish job
    2.78  
    2.79 -            val process_result = job.join
    2.80 +            val (process_result, heap_digest) = job.join
    2.81  
    2.82              val log_lines = process_result.out_lines.filterNot(_.startsWith("\f"))
    2.83              val process_result_tail =
    2.84 @@ -531,21 +537,10 @@
    2.85  
    2.86  
    2.87              // write log file
    2.88 -            val heap_digest =
    2.89 -              if (process_result.ok) {
    2.90 -                val heap_digest =
    2.91 -                  for (path <- job.output_path if path.is_file)
    2.92 -                    yield Sessions.write_heap_digest(path)
    2.93 -
    2.94 -                File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
    2.95 -
    2.96 -                heap_digest
    2.97 -              }
    2.98 -              else {
    2.99 -                File.write(store.output_log(name), terminate_lines(log_lines))
   2.100 -
   2.101 -                None
   2.102 -              }
   2.103 +            if (process_result.ok) {
   2.104 +              File.write_gzip(store.output_log_gz(name), terminate_lines(log_lines))
   2.105 +            }
   2.106 +            else File.write(store.output_log(name), terminate_lines(log_lines))
   2.107  
   2.108              // write database
   2.109              {