6 |
6 |
7 signature BASH = |
7 signature BASH = |
8 sig |
8 sig |
9 val string: string -> string |
9 val string: string -> string |
10 val strings: string list -> string |
10 val strings: string list -> string |
11 val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
11 val process: string -> {out: string, err: string, rc: int} |
12 end; |
12 end; |
13 |
13 |
14 structure Bash: sig val terminate: int option -> unit end = |
|
15 struct |
|
16 |
|
17 fun terminate NONE = () |
|
18 | terminate (SOME pid) = |
|
19 let |
|
20 val kill = Kill.kill_group pid; |
|
21 |
|
22 fun multi_kill count s = |
|
23 count = 0 orelse |
|
24 (kill s; kill Kill.SIGNONE) andalso |
|
25 (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
|
26 val _ = |
|
27 multi_kill 7 Kill.SIGINT andalso |
|
28 multi_kill 3 Kill.SIGTERM andalso |
|
29 multi_kill 1 Kill.SIGKILL; |
|
30 in () end; |
|
31 |
|
32 end; |
|
33 |
|
34 if ML_System.platform_is_windows then ML |
|
35 \<open> |
|
36 structure Bash: BASH = |
14 structure Bash: BASH = |
37 struct |
15 struct |
38 |
|
39 open Bash; |
|
40 |
16 |
41 val string = Bash_Syntax.string; |
17 val string = Bash_Syntax.string; |
42 val strings = Bash_Syntax.strings; |
18 val strings = Bash_Syntax.strings; |
43 |
19 |
44 val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => |
20 fun process script = |
45 let |
|
46 datatype result = Wait | Signal | Result of int; |
|
47 val result = Synchronized.var "bash_result" Wait; |
|
48 |
|
49 val id = serial_string (); |
|
50 val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
51 val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
|
52 val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
|
53 val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
|
54 |
|
55 fun cleanup_files () = |
|
56 (try File.rm script_path; |
|
57 try File.rm out_path; |
|
58 try File.rm err_path; |
|
59 try File.rm pid_path); |
|
60 val _ = cleanup_files (); |
|
61 |
|
62 val system_thread = |
|
63 Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
|
64 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
|
65 let |
|
66 val _ = File.write script_path script; |
|
67 val bash_script = |
|
68 "bash " ^ File.bash_path script_path ^ |
|
69 " > " ^ File.bash_path out_path ^ |
|
70 " 2> " ^ File.bash_path err_path; |
|
71 val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; |
|
72 val rc = |
|
73 Windows.simpleExecute ("", |
|
74 quote (ML_System.platform_path bash_process) ^ " " ^ |
|
75 quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) |
|
76 |> Windows.fromStatus |> SysWord.toInt; |
|
77 val res = if rc = 130 orelse rc = 512 then Signal else Result rc; |
|
78 in Synchronized.change result (K res) end |
|
79 handle exn => |
|
80 (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); |
|
81 |
|
82 fun read_pid 0 = NONE |
|
83 | read_pid count = |
|
84 (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of |
|
85 NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) |
|
86 | some => some); |
|
87 |
|
88 fun cleanup () = |
|
89 (Isabelle_Thread.interrupt_unsynchronized system_thread; |
|
90 cleanup_files ()); |
|
91 in |
|
92 let |
|
93 val _ = |
|
94 restore_attributes (fn () => |
|
95 Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
|
96 |
|
97 val out = the_default "" (try File.read out_path); |
|
98 val err = the_default "" (try File.read err_path); |
|
99 val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
|
100 val pid = read_pid 1; |
|
101 val _ = cleanup (); |
|
102 in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
|
103 handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) |
|
104 end); |
|
105 |
|
106 end; |
|
107 \<close> |
|
108 else ML |
|
109 \<open> |
|
110 structure Bash: BASH = |
|
111 struct |
|
112 |
|
113 open Bash; |
|
114 |
|
115 val string = Bash_Syntax.string; |
|
116 val strings = Bash_Syntax.strings; |
|
117 |
|
118 val process_ml = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => |
|
119 let |
|
120 datatype result = Wait | Signal | Result of int; |
|
121 val result = Synchronized.var "bash_result" Wait; |
|
122 |
|
123 val id = serial_string (); |
|
124 val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
125 val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
|
126 val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
|
127 val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
|
128 |
|
129 fun cleanup_files () = |
|
130 (try File.rm script_path; |
|
131 try File.rm out_path; |
|
132 try File.rm err_path; |
|
133 try File.rm pid_path); |
|
134 val _ = cleanup_files (); |
|
135 |
|
136 val system_thread = |
|
137 Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
|
138 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
|
139 let |
|
140 val _ = File.write script_path script; |
|
141 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
|
142 val status = |
|
143 OS.Process.system |
|
144 ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^ |
|
145 " bash " ^ File.bash_path script_path ^ |
|
146 " > " ^ File.bash_path out_path ^ |
|
147 " 2> " ^ File.bash_path err_path); |
|
148 val res = |
|
149 (case Posix.Process.fromStatus status of |
|
150 Posix.Process.W_EXITED => Result 0 |
|
151 | Posix.Process.W_EXITSTATUS 0wx82 => Signal |
|
152 | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
|
153 | Posix.Process.W_SIGNALED s => |
|
154 if s = Posix.Signal.int then Signal |
|
155 else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) |
|
156 | Posix.Process.W_STOPPED s => |
|
157 Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
|
158 in Synchronized.change result (K res) end |
|
159 handle exn => |
|
160 (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); |
|
161 |
|
162 fun read_pid 0 = NONE |
|
163 | read_pid count = |
|
164 (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of |
|
165 NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) |
|
166 | some => some); |
|
167 |
|
168 fun cleanup () = |
|
169 (Isabelle_Thread.interrupt_unsynchronized system_thread; |
|
170 cleanup_files ()); |
|
171 in |
|
172 let |
|
173 val _ = |
|
174 restore_attributes (fn () => |
|
175 Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
|
176 |
|
177 val out = the_default "" (try File.read out_path); |
|
178 val err = the_default "" (try File.read err_path); |
|
179 val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
|
180 val pid = read_pid 1; |
|
181 val _ = cleanup (); |
|
182 in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
|
183 handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) |
|
184 end); |
|
185 |
|
186 fun process_scala script = |
|
187 Scala.function_thread "bash_process" |
21 Scala.function_thread "bash_process" |
188 ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |
22 ("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |
189 |> YXML.parse_body |
23 |> YXML.parse_body |
190 |> |
24 |> |
191 let open XML.Decode in |
25 let open XML.Decode in |
192 variant |
26 variant |
193 [fn ([], []) => raise Exn.Interrupt, |
27 [fn ([], []) => raise Exn.Interrupt, |
194 fn ([], a) => error (YXML.string_of_body a), |
28 fn ([], a) => error (YXML.string_of_body a), |
195 fn ([a, b], c) => |
29 fn ([a], c) => |
196 let |
30 let |
197 val rc = int_atom a; |
31 val rc = int_atom a; |
198 val pid = int_atom b; |
|
199 val (out, err) = pair I I c |> apply2 YXML.string_of_body; |
32 val (out, err) = pair I I c |> apply2 YXML.string_of_body; |
200 in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end] |
33 in {out = out, err = err, rc = rc} end] |
201 end; |
34 end; |
202 |
35 |
203 fun process script = |
|
204 if ML_System.platform_is_rosetta () then process_scala script else process_ml script; |
|
205 |
|
206 end; |
36 end; |
207 \<close> |
|