# HG changeset patch # User wenzelm # Date 1457531691 -3600 # Node ID 5db10482f4cfb45d1188f0fab9831977105fc43c # Parent 3541bc1e97d2fc0021cd2a1615d5a6a1bfbcf617 bash process with builtin timing; diff -r 3541bc1e97d2 -r 5db10482f4cf Admin/components/components.sha1 --- a/Admin/components/components.sha1 Wed Mar 09 14:24:16 2016 +0100 +++ b/Admin/components/components.sha1 Wed Mar 09 14:54:51 2016 +0100 @@ -1,5 +1,6 @@ fbe83b522cb37748ac1b3c943ad71704fdde2f82 bash_process-1.1.1.tar.gz bb9ef498cd594b4289221b96146d529c899da209 bash_process-1.1.tar.gz +9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz 70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz a5e02b5e990da4275dc5d4480c3b72fc73160c28 cvc4-1.5pre-1.tar.gz diff -r 3541bc1e97d2 -r 5db10482f4cf Admin/components/main --- a/Admin/components/main Wed Mar 09 14:24:16 2016 +0100 +++ b/Admin/components/main Wed Mar 09 14:54:51 2016 +0100 @@ -1,5 +1,5 @@ #main components for everyday use, without big impact on overall build time -bash_process-1.1.1 +bash_process-1.2 csdp-6.x cvc4-1.5pre-3 e-1.8 diff -r 3541bc1e97d2 -r 5db10482f4cf src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Wed Mar 09 14:24:16 2016 +0100 +++ b/src/Pure/Concurrent/bash.ML Wed Mar 09 14:54:51 2016 +0100 @@ -38,7 +38,7 @@ val _ = getenv_strict "ISABELLE_BASH_PROCESS"; val status = OS.Process.system - ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ + ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^ " bash " ^ File.bash_path script_path ^ " > " ^ File.bash_path out_path ^ " 2> " ^ File.bash_path err_path); diff -r 3541bc1e97d2 -r 5db10482f4cf src/Pure/Concurrent/bash.scala --- a/src/Pure/Concurrent/bash.scala Wed Mar 09 14:24:16 2016 +0100 +++ b/src/Pure/Concurrent/bash.scala Wed Mar 09 14:54:51 2016 +0100 @@ -34,13 +34,16 @@ script: String, cwd: JFile, env: Map[String, String], redirect: Boolean) extends Prover.System_Process { - val script_file = Isabelle_System.tmp_file("bash_script") + private val timing_file = Isabelle_System.tmp_file("bash_script") + private val timing = Synchronized[Option[Timing]](None) + + private val script_file = Isabelle_System.tmp_file("bash_script") File.write(script_file, script) private val proc = Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect, File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", - "bash", File.standard_path(script_file)) + File.standard_path(timing_file), "bash", File.standard_path(script_file)) // channels @@ -105,6 +108,19 @@ script_file.delete + timing.change { + case None => + val t = + Word.explode(File.read(timing_file)) match { + case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) => + Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) + case _ => Timing.zero + } + timing_file.delete + Some(t) + case some => some + } + rc } @@ -130,7 +146,7 @@ catch { case Exn.Interrupt() => terminate; Exn.Interrupt.return_code } if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() - Process_Result(rc, out_lines.join, err_lines.join) + Process_Result(rc, out_lines.join, err_lines.join, false, timing.value.get) } } } diff -r 3541bc1e97d2 -r 5db10482f4cf src/Pure/Concurrent/bash_windows.ML --- a/src/Pure/Concurrent/bash_windows.ML Wed Mar 09 14:24:16 2016 +0100 +++ b/src/Pure/Concurrent/bash_windows.ML Wed Mar 09 14:54:51 2016 +0100 @@ -43,7 +43,7 @@ val rc = Windows.simpleExecute ("", quote (ML_System.platform_path bash_process) ^ " " ^ - quote (File.platform_path pid_path) ^ " bash -c " ^ quote bash_script) + quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) |> Windows.fromStatus |> SysWord.toInt; val res = if rc = 130 orelse rc = 512 then Signal else Result rc; in Synchronized.change result (K res) end diff -r 3541bc1e97d2 -r 5db10482f4cf src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Wed Mar 09 14:24:16 2016 +0100 +++ b/src/Pure/System/process_result.scala Wed Mar 09 14:54:51 2016 +0100 @@ -10,13 +10,14 @@ rc: Int, out_lines: List[String] = Nil, err_lines: List[String] = Nil, - timeout: Option[Time] = None) + timeout: Boolean = false, + timing: Timing = Timing.zero) { def out: String = cat_lines(out_lines) def err: String = cat_lines(err_lines) def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s)) - def set_timeout(t: Time): Process_Result = copy(rc = 1, timeout = Some(t)) + def was_timeout: Process_Result = copy(rc = 1, timeout = true) def ok: Boolean = rc == 0 def interrupted: Boolean = rc == Exn.Interrupt.return_code diff -r 3541bc1e97d2 -r 5db10482f4cf src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Mar 09 14:24:16 2016 +0100 +++ b/src/Pure/Tools/build.scala Wed Mar 09 14:54:51 2016 +0100 @@ -624,13 +624,11 @@ def terminate: Unit = result.cancel def is_finished: Boolean = result.is_finished - @volatile private var was_timeout: Option[Time] = None + @volatile private var was_timeout = false private val timeout_request: Option[Event_Timer.Request] = { - val timeout = info.timeout - val t0 = Time.now() - if (timeout > Time.zero) - Some(Event_Timer.request(t0 + timeout) { terminate; was_timeout = Some(Time.now() - t0) }) + if (info.timeout > Time.zero) + Some(Event_Timer.request(Time.now() + info.timeout) { terminate; was_timeout = true }) else None } @@ -646,10 +644,8 @@ timeout_request.foreach(_.cancel) if (res.interrupted) { - was_timeout match { - case Some(t) => res.error(Output.error_text("Timeout")).set_timeout(t) - case None => res.error(Output.error_text("Interrupt")) - } + if (was_timeout) res.error(Output.error_text("Timeout")).was_timeout + else res.error(Output.error_text("Interrupt")) } else res }