# HG changeset patch # User wenzelm # Date 1613855356 -3600 # Node ID ad60214bef094fdadab92e90952aaca6b23261d6 # Parent 71b7a5775342f8b93eac77c9fb7a172a8055e00c more uniform Bash.process: always ask Isabelle/Scala; diff -r 71b7a5775342 -r ad60214bef09 src/Pure/ML/ml_system.ML --- a/src/Pure/ML/ml_system.ML Sat Feb 20 21:38:23 2021 +0100 +++ b/src/Pure/ML/ml_system.ML Sat Feb 20 22:09:16 2021 +0100 @@ -11,7 +11,6 @@ val platform_is_windows: bool val platform_is_64: bool val platform_is_arm: bool - val platform_is_rosetta: unit -> bool val platform_path: string -> string val standard_path: string -> string end; @@ -25,12 +24,6 @@ val platform_is_64 = String.isPrefix "x86_64-" platform; val platform_is_arm = String.isPrefix "arm64-" platform; -fun platform_is_rosetta () = - (case OS.Process.getEnv "ISABELLE_APPLE_PLATFORM64" of - NONE => false - | SOME "" => false - | SOME apple_platform => apple_platform <> platform); - val platform_path = if platform_is_windows then fn path => diff -r 71b7a5775342 -r ad60214bef09 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Feb 20 21:38:23 2021 +0100 +++ b/src/Pure/ROOT.ML Sat Feb 20 22:09:16 2021 +0100 @@ -294,7 +294,6 @@ (*Isabelle system*) ML_file "PIDE/protocol_command.ML"; ML_file "System/scala.ML"; -ML_file "System/kill.ML"; ML_file "System/bash.ML"; ML_file "System/isabelle_system.ML"; diff -r 71b7a5775342 -r ad60214bef09 src/Pure/System/bash.ML --- a/src/Pure/System/bash.ML Sat Feb 20 21:38:23 2021 +0100 +++ b/src/Pure/System/bash.ML Sat Feb 20 22:09:16 2021 +0100 @@ -8,182 +8,16 @@ sig val string: string -> string val strings: string list -> string - val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} + val process: string -> {out: string, err: string, rc: int} end; -structure Bash: sig val terminate: int option -> unit end = -struct - -fun terminate NONE = () - | terminate (SOME pid) = - let - val kill = Kill.kill_group pid; - - fun multi_kill count s = - count = 0 orelse - (kill s; kill Kill.SIGNONE) andalso - (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); - val _ = - multi_kill 7 Kill.SIGINT andalso - multi_kill 3 Kill.SIGTERM andalso - multi_kill 1 Kill.SIGKILL; - in () end; - -end; - -if ML_System.platform_is_windows then ML -\ structure Bash: BASH = struct -open Bash; - val string = Bash_Syntax.string; val strings = Bash_Syntax.strings; -val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => - let - datatype result = Wait | Signal | Result of int; - val result = Synchronized.var "bash_result" Wait; - - val id = serial_string (); - val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); - val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); - val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); - val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - - fun cleanup_files () = - (try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); - val _ = cleanup_files (); - - val system_thread = - Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => - Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => - let - val _ = File.write script_path script; - val bash_script = - "bash " ^ File.bash_path script_path ^ - " > " ^ File.bash_path out_path ^ - " 2> " ^ File.bash_path err_path; - val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; - val rc = - Windows.simpleExecute ("", - quote (ML_System.platform_path bash_process) ^ " " ^ - 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 - handle exn => - (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); - - fun read_pid 0 = NONE - | read_pid count = - (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of - NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) - | some => some); - - fun cleanup () = - (Isabelle_Thread.interrupt_unsynchronized system_thread; - cleanup_files ()); - in - let - val _ = - restore_attributes (fn () => - Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); - - val out = the_default "" (try File.read out_path); - val err = the_default "" (try File.read err_path); - val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = read_pid 1; - val _ = cleanup (); - in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) - end); - -end; -\ -else ML -\ -structure Bash: BASH = -struct - -open Bash; - -val string = Bash_Syntax.string; -val strings = Bash_Syntax.strings; - -val process_ml = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => - let - datatype result = Wait | Signal | Result of int; - val result = Synchronized.var "bash_result" Wait; - - val id = serial_string (); - val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); - val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); - val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); - val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); - - fun cleanup_files () = - (try File.rm script_path; - try File.rm out_path; - try File.rm err_path; - try File.rm pid_path); - val _ = cleanup_files (); - - val system_thread = - Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => - Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => - let - val _ = File.write script_path script; - val _ = getenv_strict "ISABELLE_BASH_PROCESS"; - val status = - OS.Process.system - ("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); - val res = - (case Posix.Process.fromStatus status of - Posix.Process.W_EXITED => Result 0 - | Posix.Process.W_EXITSTATUS 0wx82 => Signal - | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) - | Posix.Process.W_SIGNALED s => - if s = Posix.Signal.int then Signal - else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) - | Posix.Process.W_STOPPED s => - Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); - in Synchronized.change result (K res) end - handle exn => - (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); - - fun read_pid 0 = NONE - | read_pid count = - (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of - NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) - | some => some); - - fun cleanup () = - (Isabelle_Thread.interrupt_unsynchronized system_thread; - cleanup_files ()); - in - let - val _ = - restore_attributes (fn () => - Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); - - val out = the_default "" (try File.read out_path); - val err = the_default "" (try File.read err_path); - val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); - val pid = read_pid 1; - val _ = cleanup (); - in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end - handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) - end); - -fun process_scala script = +fun process script = Scala.function_thread "bash_process" ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |> YXML.parse_body @@ -192,16 +26,11 @@ variant [fn ([], []) => raise Exn.Interrupt, fn ([], a) => error (YXML.string_of_body a), - fn ([a, b], c) => + fn ([a], c) => let val rc = int_atom a; - val pid = int_atom b; val (out, err) = pair I I c |> apply2 YXML.string_of_body; - in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end] + in {out = out, err = err, rc = rc} end] end; -fun process script = - if ML_System.platform_is_rosetta () then process_scala script else process_ml script; - end; -\ \ No newline at end of file diff -r 71b7a5775342 -r ad60214bef09 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Sat Feb 20 21:38:23 2021 +0100 +++ b/src/Pure/System/bash.scala Sat Feb 20 22:09:16 2021 +0100 @@ -211,30 +211,25 @@ val here = Scala_Project.here def apply(script: String): String = { - val result = - Exn.capture { - val proc = process(script) - val res = proc.result() - (res, proc.pid) - } + val result = Exn.capture { Isabelle_System.bash(script) } val is_interrupt = result match { - case Exn.Res((res, _)) => res.rc == Exn.Interrupt.return_code + case Exn.Res(res) => res.rc == Exn.Interrupt.return_code case Exn.Exn(exn) => Exn.is_interrupt(exn) } - val encode: XML.Encode.T[Exn.Result[(Process_Result, String)]] = + val encode: XML.Encode.T[Exn.Result[Process_Result]] = { import XML.Encode._ val string = XML.Encode.string variant(List( { case _ if is_interrupt => (Nil, Nil) }, { case Exn.Exn(exn) => (Nil, string(Exn.message(exn))) }, - { case Exn.Res((res, pid)) => + { case Exn.Res(res) => val out = Library.terminate_lines(res.out_lines) val err = Library.terminate_lines(res.err_lines) - (List(int_atom(res.rc), pid), pair(string, string)(out, err)) })) + (List(int_atom(res.rc)), pair(string, string)(out, err)) })) } YXML.string_of_body(encode(result)) }