1 (* Title: Pure/System/bash_windows.ML |
|
2 Author: Makarius |
|
3 |
|
4 GNU bash processes, with propagation of interrupts -- Windows version. |
|
5 *) |
|
6 |
|
7 signature BASH = |
|
8 sig |
|
9 val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
|
10 end; |
|
11 |
|
12 structure Bash: BASH = |
|
13 struct |
|
14 |
|
15 val process = uninterruptible (fn restore_attributes => fn script => |
|
16 let |
|
17 datatype result = Wait | Signal | Result of int; |
|
18 val result = Synchronized.var "bash_result" Wait; |
|
19 |
|
20 val id = serial_string (); |
|
21 val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
22 val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
|
23 val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
|
24 val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
|
25 |
|
26 fun cleanup_files () = |
|
27 (try File.rm script_path; |
|
28 try File.rm out_path; |
|
29 try File.rm err_path; |
|
30 try File.rm pid_path); |
|
31 val _ = cleanup_files (); |
|
32 |
|
33 val system_thread = |
|
34 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
|
35 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
|
36 let |
|
37 val _ = File.write script_path script; |
|
38 val bash_script = |
|
39 "bash " ^ File.bash_path script_path ^ |
|
40 " > " ^ File.bash_path out_path ^ |
|
41 " 2> " ^ File.bash_path err_path; |
|
42 val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; |
|
43 val rc = |
|
44 Windows.simpleExecute ("", |
|
45 quote (ML_System.platform_path bash_process) ^ " " ^ |
|
46 quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) |
|
47 |> Windows.fromStatus |> SysWord.toInt; |
|
48 val res = if rc = 130 orelse rc = 512 then Signal else Result rc; |
|
49 in Synchronized.change result (K res) end |
|
50 handle exn => |
|
51 (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); |
|
52 |
|
53 fun read_pid 0 = NONE |
|
54 | read_pid count = |
|
55 (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of |
|
56 NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) |
|
57 | some => some); |
|
58 |
|
59 fun terminate NONE = () |
|
60 | terminate (SOME pid) = |
|
61 let |
|
62 fun kill s = |
|
63 let |
|
64 val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe"; |
|
65 val arg = "kill -" ^ s ^ " -" ^ string_of_int pid; |
|
66 in |
|
67 OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg)) |
|
68 handle OS.SysErr _ => false |
|
69 end; |
|
70 |
|
71 fun multi_kill count s = |
|
72 count = 0 orelse |
|
73 (kill s; kill "0") andalso |
|
74 (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
|
75 val _ = |
|
76 multi_kill 10 "INT" andalso |
|
77 multi_kill 10 "TERM" andalso |
|
78 multi_kill 10 "KILL"; |
|
79 in () end; |
|
80 |
|
81 fun cleanup () = |
|
82 (Standard_Thread.interrupt_unsynchronized system_thread; |
|
83 cleanup_files ()); |
|
84 in |
|
85 let |
|
86 val _ = |
|
87 restore_attributes (fn () => |
|
88 Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
|
89 |
|
90 val out = the_default "" (try File.read out_path); |
|
91 val err = the_default "" (try File.read err_path); |
|
92 val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
|
93 val pid = read_pid 1; |
|
94 val _ = cleanup (); |
|
95 in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
|
96 handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) |
|
97 end); |
|
98 |
|
99 end; |
|