bash process with builtin timing;
authorwenzelm
Wed Mar 09 14:54:51 2016 +0100 (2016-03-09)
changeset 625695db10482f4cf
parent 62568 3541bc1e97d2
child 62570 f4c96158a3b8
bash process with builtin timing;
Admin/components/components.sha1
Admin/components/main
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash.scala
src/Pure/Concurrent/bash_windows.ML
src/Pure/System/process_result.scala
src/Pure/Tools/build.scala
     1.1 --- a/Admin/components/components.sha1	Wed Mar 09 14:24:16 2016 +0100
     1.2 +++ b/Admin/components/components.sha1	Wed Mar 09 14:54:51 2016 +0100
     1.3 @@ -1,5 +1,6 @@
     1.4  fbe83b522cb37748ac1b3c943ad71704fdde2f82  bash_process-1.1.1.tar.gz
     1.5  bb9ef498cd594b4289221b96146d529c899da209  bash_process-1.1.tar.gz
     1.6 +9e21f447bfa0431ae5097301d553dd6df3c58218  bash_process-1.2.tar.gz
     1.7  70105fd6fbfd1a868383fc510772b95234325d31  csdp-6.x.tar.gz
     1.8  2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7  cvc3-2.4.1.tar.gz
     1.9  a5e02b5e990da4275dc5d4480c3b72fc73160c28  cvc4-1.5pre-1.tar.gz
     2.1 --- a/Admin/components/main	Wed Mar 09 14:24:16 2016 +0100
     2.2 +++ b/Admin/components/main	Wed Mar 09 14:54:51 2016 +0100
     2.3 @@ -1,5 +1,5 @@
     2.4  #main components for everyday use, without big impact on overall build time
     2.5 -bash_process-1.1.1
     2.6 +bash_process-1.2
     2.7  csdp-6.x
     2.8  cvc4-1.5pre-3
     2.9  e-1.8
     3.1 --- a/src/Pure/Concurrent/bash.ML	Wed Mar 09 14:24:16 2016 +0100
     3.2 +++ b/src/Pure/Concurrent/bash.ML	Wed Mar 09 14:54:51 2016 +0100
     3.3 @@ -38,7 +38,7 @@
     3.4              val _ = getenv_strict "ISABELLE_BASH_PROCESS";
     3.5              val status =
     3.6                OS.Process.system
     3.7 -                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^
     3.8 +                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
     3.9                    " bash " ^ File.bash_path script_path ^
    3.10                    " > " ^ File.bash_path out_path ^
    3.11                    " 2> " ^ File.bash_path err_path);
     4.1 --- a/src/Pure/Concurrent/bash.scala	Wed Mar 09 14:24:16 2016 +0100
     4.2 +++ b/src/Pure/Concurrent/bash.scala	Wed Mar 09 14:54:51 2016 +0100
     4.3 @@ -34,13 +34,16 @@
     4.4        script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
     4.5      extends Prover.System_Process
     4.6    {
     4.7 -    val script_file = Isabelle_System.tmp_file("bash_script")
     4.8 +    private val timing_file = Isabelle_System.tmp_file("bash_script")
     4.9 +    private val timing = Synchronized[Option[Timing]](None)
    4.10 +
    4.11 +    private val script_file = Isabelle_System.tmp_file("bash_script")
    4.12      File.write(script_file, script)
    4.13  
    4.14      private val proc =
    4.15        Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
    4.16          File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
    4.17 -          "bash", File.standard_path(script_file))
    4.18 +          File.standard_path(timing_file), "bash", File.standard_path(script_file))
    4.19  
    4.20  
    4.21      // channels
    4.22 @@ -105,6 +108,19 @@
    4.23  
    4.24        script_file.delete
    4.25  
    4.26 +      timing.change {
    4.27 +        case None =>
    4.28 +          val t =
    4.29 +            Word.explode(File.read(timing_file)) match {
    4.30 +              case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
    4.31 +                Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
    4.32 +              case _ => Timing.zero
    4.33 +            }
    4.34 +          timing_file.delete
    4.35 +          Some(t)
    4.36 +        case some => some
    4.37 +      }
    4.38 +
    4.39        rc
    4.40      }
    4.41  
    4.42 @@ -130,7 +146,7 @@
    4.43          catch { case Exn.Interrupt() => terminate; Exn.Interrupt.return_code }
    4.44        if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    4.45  
    4.46 -      Process_Result(rc, out_lines.join, err_lines.join)
    4.47 +      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value.get)
    4.48      }
    4.49    }
    4.50  }
     5.1 --- a/src/Pure/Concurrent/bash_windows.ML	Wed Mar 09 14:24:16 2016 +0100
     5.2 +++ b/src/Pure/Concurrent/bash_windows.ML	Wed Mar 09 14:54:51 2016 +0100
     5.3 @@ -43,7 +43,7 @@
     5.4              val rc =
     5.5                Windows.simpleExecute ("",
     5.6                  quote (ML_System.platform_path bash_process) ^ " " ^
     5.7 -                quote (File.platform_path pid_path) ^ " bash -c " ^ quote bash_script)
     5.8 +                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
     5.9                |> Windows.fromStatus |> SysWord.toInt;
    5.10              val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
    5.11            in Synchronized.change result (K res) end
     6.1 --- a/src/Pure/System/process_result.scala	Wed Mar 09 14:24:16 2016 +0100
     6.2 +++ b/src/Pure/System/process_result.scala	Wed Mar 09 14:54:51 2016 +0100
     6.3 @@ -10,13 +10,14 @@
     6.4    rc: Int,
     6.5    out_lines: List[String] = Nil,
     6.6    err_lines: List[String] = Nil,
     6.7 -  timeout: Option[Time] = None)
     6.8 +  timeout: Boolean = false,
     6.9 +  timing: Timing = Timing.zero)
    6.10  {
    6.11    def out: String = cat_lines(out_lines)
    6.12    def err: String = cat_lines(err_lines)
    6.13    def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
    6.14  
    6.15 -  def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t))
    6.16 +  def was_timeout: Process_Result = copy(rc = 1, timeout = true)
    6.17  
    6.18    def ok: Boolean = rc == 0
    6.19    def interrupted: Boolean = rc == Exn.Interrupt.return_code
     7.1 --- a/src/Pure/Tools/build.scala	Wed Mar 09 14:24:16 2016 +0100
     7.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 09 14:54:51 2016 +0100
     7.3 @@ -624,13 +624,11 @@
     7.4      def terminate: Unit = result.cancel
     7.5      def is_finished: Boolean = result.is_finished
     7.6  
     7.7 -    @volatile private var was_timeout: Option[Time] = None
     7.8 +    @volatile private var was_timeout = false
     7.9      private val timeout_request: Option[Event_Timer.Request] =
    7.10      {
    7.11 -      val timeout = info.timeout
    7.12 -      val t0 = Time.now()
    7.13 -      if (timeout > Time.zero)
    7.14 -        Some(Event_Timer.request(t0 + timeout) { terminate; was_timeout = Some(Time.now() - t0) })
    7.15 +      if (info.timeout > Time.zero)
    7.16 +        Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true })
    7.17        else None
    7.18      }
    7.19  
    7.20 @@ -646,10 +644,8 @@
    7.21        timeout_request.foreach(_.cancel)
    7.22  
    7.23        if (res.interrupted) {
    7.24 -        was_timeout match {
    7.25 -          case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t)
    7.26 -          case None => res.error(Output.error_text("Interrupt"))
    7.27 -        }
    7.28 +        if (was_timeout) res.error(Output.error_text("Timeout")).was_timeout
    7.29 +        else res.error(Output.error_text("Interrupt"))
    7.30        }
    7.31        else res
    7.32      }