author | wenzelm |
Tue, 09 Feb 2021 14:55:36 +0100 | |
changeset 73244 | 5bded25065f8 |
parent 73234 | da0ee7fbc068 |
child 73263 | ad60214bef09 |
permissions | -rw-r--r-- |
62584 | 1 |
(* Title: Pure/System/bash.ML |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
3 |
|
62879
4764473c9b8d
back to static conditional compilation -- simplified bootstrap;
wenzelm
parents:
62850
diff
changeset
|
4 |
GNU bash processes, with propagation of interrupts -- POSIX version. |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
5 |
*) |
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
6 |
|
44054 | 7 |
signature BASH = |
8 |
sig |
|
64304 | 9 |
val string: string -> string |
10 |
val strings: string list -> string |
|
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
11 |
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
44054 | 12 |
end; |
13 |
||
73227 | 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 _ = |
|
73234 | 27 |
multi_kill 7 Kill.SIGINT andalso |
28 |
multi_kill 3 Kill.SIGTERM andalso |
|
29 |
multi_kill 1 Kill.SIGKILL; |
|
73227 | 30 |
in () end; |
31 |
||
32 |
end; |
|
33 |
||
62911
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
34 |
if ML_System.platform_is_windows then ML |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
35 |
\<open> |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
36 |
structure Bash: BASH = |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
37 |
struct |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
38 |
|
73227 | 39 |
open Bash; |
40 |
||
64304 | 41 |
val string = Bash_Syntax.string; |
42 |
val strings = Bash_Syntax.strings; |
|
43 |
||
62923 | 44 |
val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => |
62911
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
45 |
let |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
46 |
datatype result = Wait | Signal | Result of int; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
47 |
val result = Synchronized.var "bash_result" Wait; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
48 |
|
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
49 |
val id = serial_string (); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
50 |
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
51 |
val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
52 |
val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
53 |
val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
54 |
|
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
55 |
fun cleanup_files () = |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
56 |
(try File.rm script_path; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
57 |
try File.rm out_path; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
58 |
try File.rm err_path; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
59 |
try File.rm pid_path); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
60 |
val _ = cleanup_files (); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
61 |
|
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
62 |
val system_thread = |
71692 | 63 |
Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
62923 | 64 |
Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
62911
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
65 |
let |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
66 |
val _ = File.write script_path script; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
67 |
val bash_script = |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
68 |
"bash " ^ File.bash_path script_path ^ |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
69 |
" > " ^ File.bash_path out_path ^ |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
70 |
" 2> " ^ File.bash_path err_path; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
71 |
val bash_process = getenv_strict "ISABELLE_BASH_PROCESS"; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
72 |
val rc = |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
73 |
Windows.simpleExecute ("", |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
74 |
quote (ML_System.platform_path bash_process) ^ " " ^ |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
75 |
quote (File.platform_path pid_path) ^ " \"\" bash -c " ^ quote bash_script) |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
76 |
|> Windows.fromStatus |> SysWord.toInt; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
77 |
val res = if rc = 130 orelse rc = 512 then Signal else Result rc; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
78 |
in Synchronized.change result (K res) end |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
79 |
handle exn => |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
80 |
(Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
81 |
|
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
82 |
fun read_pid 0 = NONE |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
83 |
| read_pid count = |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
84 |
(case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
85 |
NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
86 |
| some => some); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
87 |
|
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
88 |
fun cleanup () = |
71692 | 89 |
(Isabelle_Thread.interrupt_unsynchronized system_thread; |
62911
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
90 |
cleanup_files ()); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
91 |
in |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
92 |
let |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
93 |
val _ = |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
94 |
restore_attributes (fn () => |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
95 |
Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
96 |
|
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
97 |
val out = the_default "" (try File.read out_path); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
98 |
val err = the_default "" (try File.read err_path); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
99 |
val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
100 |
val pid = read_pid 1; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
101 |
val _ = cleanup (); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
102 |
in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
103 |
handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
104 |
end); |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
105 |
|
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
106 |
end; |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
107 |
\<close> |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
108 |
else ML |
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
109 |
\<open> |
44054 | 110 |
structure Bash: BASH = |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
111 |
struct |
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
112 |
|
73227 | 113 |
open Bash; |
114 |
||
64304 | 115 |
val string = Bash_Syntax.string; |
116 |
val strings = Bash_Syntax.strings; |
|
117 |
||
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
118 |
val process_ml = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => |
40749 | 119 |
let |
120 |
datatype result = Wait | Signal | Result of int; |
|
121 |
val result = Synchronized.var "bash_result" Wait; |
|
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
122 |
|
40749 | 123 |
val id = serial_string (); |
124 |
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
125 |
val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
126 |
val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
40749 | 127 |
val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
128 |
|
54651
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
129 |
fun cleanup_files () = |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
130 |
(try File.rm script_path; |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
131 |
try File.rm out_path; |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
132 |
try File.rm err_path; |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
133 |
try File.rm pid_path); |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
134 |
val _ = cleanup_files (); |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
135 |
|
40749 | 136 |
val system_thread = |
71692 | 137 |
Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
62923 | 138 |
Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
40749 | 139 |
let |
140 |
val _ = File.write script_path script; |
|
62295 | 141 |
val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
40749 | 142 |
val status = |
143 |
OS.Process.system |
|
62569 | 144 |
("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^ |
62549
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62505
diff
changeset
|
145 |
" bash " ^ File.bash_path script_path ^ |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62505
diff
changeset
|
146 |
" > " ^ File.bash_path out_path ^ |
9498623b27f0
File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
wenzelm
parents:
62505
diff
changeset
|
147 |
" 2> " ^ File.bash_path err_path); |
40749 | 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 |
|
40783
21f7e8d66a39
more conventional exception propagation -- taking into account Simple_Thread.fork wrapping;
wenzelm
parents:
40750
diff
changeset
|
159 |
handle exn => |
62505 | 160 |
(Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
161 |
|
54651
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
162 |
fun read_pid 0 = NONE |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
163 |
| read_pid count = |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
164 |
(case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
165 |
NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) |
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
166 |
| some => some); |
43847
529159f81d06
more general bash_process, which allows to terminate background processes as well;
wenzelm
parents:
40896
diff
changeset
|
167 |
|
40749 | 168 |
fun cleanup () = |
71692 | 169 |
(Isabelle_Thread.interrupt_unsynchronized system_thread; |
54651
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
170 |
cleanup_files ()); |
40749 | 171 |
in |
172 |
let |
|
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
173 |
val _ = |
40749 | 174 |
restore_attributes (fn () => |
40750
2064991db2ac
more thorough process termination (cf. Scala version);
wenzelm
parents:
40749
diff
changeset
|
175 |
Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
176 |
|
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
177 |
val out = the_default "" (try File.read out_path); |
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
178 |
val err = the_default "" (try File.read err_path); |
40749 | 179 |
val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
54651
d71e7908eec3
more thorough read_pid with extra delay, to give external process a chance to write pid file before attempting to terminate it -- especially relevant for PIDE document processing, where interrupts can happen in the range of milliseconds;
wenzelm
parents:
47764
diff
changeset
|
180 |
val pid = read_pid 1; |
40749 | 181 |
val _ = cleanup (); |
47499
4b0daca2bf88
redirect bash stderr to Isabelle warning as appropriate -- avoid raw process error output which may either get ignored or overload PIDE syslog in extreme cases;
wenzelm
parents:
44112
diff
changeset
|
182 |
in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
62505 | 183 |
handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) |
40749 | 184 |
end); |
40748
591b6778d076
removed bash from ML system bootstrap, and past the Secure ML barrier;
wenzelm
parents:
diff
changeset
|
185 |
|
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
186 |
fun process_scala script = |
73244
5bded25065f8
more parallelism: avoid exhaustion of standard thread pool;
wenzelm
parents:
73234
diff
changeset
|
187 |
Scala.function_thread "bash_process" |
73229
5be512af2a86
inherit ISABELLE_TMP from ML process, e.g. required for $AFP/Hello_World/RunningCodeFromIsabelle.thy;
wenzelm
parents:
73228
diff
changeset
|
188 |
("export ISABELLE_TMP=" ^ string (getenv "ISABELLE_TMP") ^ "\n" ^ script) |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
189 |
|> YXML.parse_body |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
190 |
|> |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
191 |
let open XML.Decode in |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
192 |
variant |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
193 |
[fn ([], []) => raise Exn.Interrupt, |
73230 | 194 |
fn ([], a) => error (YXML.string_of_body a), |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
195 |
fn ([a, b], c) => |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
196 |
let |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
197 |
val rc = int_atom a; |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
198 |
val pid = int_atom b; |
73230 | 199 |
val (out, err) = pair I I c |> apply2 YXML.string_of_body; |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
200 |
in {out = out, err = err, rc = rc, terminate = fn () => terminate (SOME pid)} end] |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
201 |
end; |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
202 |
|
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
203 |
fun process script = |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
204 |
if ML_System.platform_is_rosetta () then process_scala script else process_ml script; |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73227
diff
changeset
|
205 |
|
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
43847
diff
changeset
|
206 |
end; |
62911
78e03d8bf1c4
back to dynamic conditional compilation (reverting 4764473c9b8d) via recursive ML name space;
wenzelm
parents:
62891
diff
changeset
|
207 |
\<close> |