author | wenzelm |
Mon, 28 Jun 2021 13:45:46 +0200 | |
changeset 73890 | 8f6b2eb15240 |
parent 73702 | 7202e12cb324 |
child 73895 | b709faa96586 |
permissions | -rw-r--r-- |
62584 | 1 |
/* Title: Pure/System/bash.scala |
60991 | 2 |
Author: Makarius |
3 |
||
4 |
GNU bash processes, with propagation of interrupts. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import java.io.{File => JFile, BufferedReader, InputStreamReader, |
|
11 |
BufferedWriter, OutputStreamWriter} |
|
12 |
||
71706 | 13 |
import scala.annotation.tailrec |
73602
37243ad3ecb6
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents:
73601
diff
changeset
|
14 |
import scala.jdk.OptionConverters._ |
71706 | 15 |
|
60991 | 16 |
|
17 |
object Bash |
|
18 |
{ |
|
64304 | 19 |
/* concrete syntax */ |
20 |
||
21 |
private def bash_chr(c: Byte): String = |
|
22 |
{ |
|
23 |
val ch = c.toChar |
|
24 |
ch match { |
|
25 |
case '\t' => "$'\\t'" |
|
26 |
case '\n' => "$'\\n'" |
|
27 |
case '\f' => "$'\\f'" |
|
28 |
case '\r' => "$'\\r'" |
|
29 |
case _ => |
|
67200 | 30 |
if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch)) |
64304 | 31 |
Symbol.ascii(ch) |
32 |
else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" |
|
33 |
else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" |
|
34 |
else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" |
|
35 |
else "\\" + ch |
|
36 |
} |
|
37 |
} |
|
38 |
||
39 |
def string(s: String): String = |
|
40 |
if (s == "") "\"\"" |
|
71601 | 41 |
else UTF8.bytes(s).iterator.map(bash_chr).mkString |
64304 | 42 |
|
43 |
def strings(ss: List[String]): String = |
|
71601 | 44 |
ss.iterator.map(Bash.string).mkString(" ") |
64304 | 45 |
|
46 |
||
47 |
/* process and result */ |
|
48 |
||
72598 | 49 |
type Watchdog = (Time, Process => Boolean) |
50 |
||
73890 | 51 |
def process_signal(group_pid: String, signal: String = "0"): Boolean = |
52 |
{ |
|
53 |
val bash = |
|
54 |
if (Platform.is_windows) List(Isabelle_System.cygwin_root() + "\\bin\\bash.exe") |
|
55 |
else List("/usr/bin/env", "bash") |
|
56 |
val (_, rc) = |
|
57 |
Isabelle_Env.process_output(Isabelle_Env.process(bash ::: List("-c", "kill -" + signal + " -" + group_pid))) |
|
58 |
rc == 0 |
|
59 |
} |
|
60 |
||
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62543
diff
changeset
|
61 |
def process(script: String, |
62573 | 62 |
cwd: JFile = null, |
62610
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
63 |
env: Map[String, String] = Isabelle_System.settings(), |
62602 | 64 |
redirect: Boolean = false, |
65 |
cleanup: () => Unit = () => ()): Process = |
|
66 |
new Process(script, cwd, env, redirect, cleanup) |
|
60991 | 67 |
|
63996 | 68 |
class Process private[Bash]( |
62602 | 69 |
script: String, |
70 |
cwd: JFile, |
|
71 |
env: Map[String, String], |
|
72 |
redirect: Boolean, |
|
73 |
cleanup: () => Unit) |
|
60991 | 74 |
{ |
62604 | 75 |
private val timing_file = Isabelle_System.tmp_file("bash_timing") |
62569 | 76 |
private val timing = Synchronized[Option[Timing]](None) |
65317 | 77 |
def get_timing: Timing = timing.value getOrElse Timing.zero |
62569 | 78 |
|
73603
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
79 |
private val winpid_file: Option[JFile] = |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
80 |
if (Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) else None |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
81 |
private val winpid_script = |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
82 |
winpid_file match { |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
83 |
case None => script |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
84 |
case Some(file) => |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
85 |
"read < /proc/self/winpid > /dev/null 2> /dev/null\n" + |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
86 |
"""echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" + script |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
87 |
} |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
88 |
|
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
89 |
private val script_file: JFile = Isabelle_System.tmp_file("bash_script") |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
90 |
File.write(script_file, winpid_script) |
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62543
diff
changeset
|
91 |
|
62296 | 92 |
private val proc = |
73890 | 93 |
Isabelle_Env.process( |
73599 | 94 |
List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), |
62610
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
95 |
File.standard_path(timing_file), "bash", File.standard_path(script_file)), |
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
96 |
cwd = cwd, env = env, redirect = redirect) |
60991 | 97 |
|
98 |
||
99 |
// channels |
|
100 |
||
101 |
val stdin: BufferedWriter = |
|
102 |
new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) |
|
103 |
||
104 |
val stdout: BufferedReader = |
|
105 |
new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) |
|
106 |
||
107 |
val stderr: BufferedReader = |
|
108 |
new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) |
|
109 |
||
110 |
||
111 |
// signals |
|
112 |
||
73601 | 113 |
private val group_pid = stdout.readLine |
60991 | 114 |
|
73603
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
115 |
private def process_alive(pid: String): Boolean = |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
116 |
(for { |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
117 |
p <- Value.Long.unapply(pid) |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
118 |
handle <- ProcessHandle.of(p).toScala |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
119 |
} yield handle.isAlive) getOrElse false |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
120 |
|
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
121 |
private def root_process_alive(): Boolean = |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
122 |
winpid_file match { |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
123 |
case None => process_alive(group_pid) |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
124 |
case Some(file) => |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
125 |
file.exists() && process_alive(Library.trim_line(File.read(file))) |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
126 |
} |
73602
37243ad3ecb6
fast approximation of test for process group (NB: initial process might already be terminated, while background processes are still running);
wenzelm
parents:
73601
diff
changeset
|
127 |
|
73601 | 128 |
@tailrec private def signal(s: String, count: Int = 1): Boolean = |
60991 | 129 |
{ |
71706 | 130 |
count <= 0 || |
131 |
{ |
|
73890 | 132 |
process_signal(group_pid, signal = s) |
133 |
val running = root_process_alive() || process_signal(group_pid) |
|
71707 | 134 |
if (running) { |
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73604
diff
changeset
|
135 |
Time.seconds(0.1).sleep() |
73601 | 136 |
signal(s, count - 1) |
60991 | 137 |
} |
71706 | 138 |
else false |
60991 | 139 |
} |
140 |
} |
|
141 |
||
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71708
diff
changeset
|
142 |
def terminate(): Unit = Isabelle_Thread.try_uninterruptible |
62574 | 143 |
{ |
73601 | 144 |
signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL") |
73367 | 145 |
proc.destroy() |
62602 | 146 |
do_cleanup() |
62574 | 147 |
} |
60991 | 148 |
|
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71708
diff
changeset
|
149 |
def interrupt(): Unit = Isabelle_Thread.try_uninterruptible |
71705 | 150 |
{ |
73890 | 151 |
process_signal(group_pid, "INT") |
71705 | 152 |
} |
153 |
||
60991 | 154 |
|
155 |
// JVM shutdown hook |
|
156 |
||
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71708
diff
changeset
|
157 |
private val shutdown_hook = Isabelle_Thread.create(() => terminate()) |
60991 | 158 |
|
159 |
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } |
|
160 |
catch { case _: IllegalStateException => } |
|
161 |
||
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62543
diff
changeset
|
162 |
|
62574 | 163 |
// cleanup |
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62543
diff
changeset
|
164 |
|
73340 | 165 |
private def do_cleanup(): Unit = |
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62543
diff
changeset
|
166 |
{ |
60991 | 167 |
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } |
168 |
catch { case _: IllegalStateException => } |
|
169 |
||
73603
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
170 |
script_file.delete() |
342362c9496c
clarified check of root process on Windows (NB: the winpid is less stable than the Cygwin/Posix pid, so it needs to be "patched" into the the bash script, instead of bash_process.c);
wenzelm
parents:
73602
diff
changeset
|
171 |
winpid_file.foreach(_.delete()) |
60991 | 172 |
|
62569 | 173 |
timing.change { |
174 |
case None => |
|
62574 | 175 |
if (timing_file.isFile) { |
176 |
val t = |
|
177 |
Word.explode(File.read(timing_file)) match { |
|
63805 | 178 |
case List(Value.Long(elapsed), Value.Long(cpu)) => |
62574 | 179 |
Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
180 |
case _ => Timing.zero |
|
181 |
} |
|
182 |
timing_file.delete |
|
183 |
Some(t) |
|
184 |
} |
|
185 |
else Some(Timing.zero) |
|
62569 | 186 |
case some => some |
187 |
} |
|
62602 | 188 |
|
189 |
cleanup() |
|
62574 | 190 |
} |
62569 | 191 |
|
62574 | 192 |
|
193 |
// join |
|
194 |
||
195 |
def join: Int = |
|
196 |
{ |
|
197 |
val rc = proc.waitFor |
|
62602 | 198 |
do_cleanup() |
62545
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62543
diff
changeset
|
199 |
rc |
8ebffdaf2ce2
Bash.process always uses a closed script instead of an open argument list, for extra robustness on Windows, where quoting is not well-defined;
wenzelm
parents:
62543
diff
changeset
|
200 |
} |
62543 | 201 |
|
202 |
||
62574 | 203 |
// result |
62543 | 204 |
|
205 |
def result( |
|
206 |
progress_stdout: String => Unit = (_: String) => (), |
|
207 |
progress_stderr: String => Unit = (_: String) => (), |
|
72598 | 208 |
watchdog: Option[Watchdog] = None, |
62543 | 209 |
strict: Boolean = true): Process_Result = |
210 |
{ |
|
73367 | 211 |
stdin.close() |
62543 | 212 |
|
213 |
val out_lines = |
|
72105 | 214 |
Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } |
62543 | 215 |
val err_lines = |
72105 | 216 |
Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } |
62543 | 217 |
|
72598 | 218 |
val watchdog_thread = |
219 |
for ((time, check) <- watchdog) |
|
220 |
yield { |
|
221 |
Future.thread("bash_watchdog") { |
|
222 |
while (proc.isAlive) { |
|
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73604
diff
changeset
|
223 |
time.sleep() |
72598 | 224 |
if (check(this)) interrupt() |
225 |
} |
|
226 |
} |
|
227 |
} |
|
228 |
||
62543 | 229 |
val rc = |
230 |
try { join } |
|
62574 | 231 |
catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } |
72598 | 232 |
|
73367 | 233 |
watchdog_thread.foreach(_.cancel()) |
72598 | 234 |
|
62543 | 235 |
if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() |
236 |
||
73134
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
72598
diff
changeset
|
237 |
Process_Result(rc, out_lines.join, err_lines.join, get_timing) |
62543 | 238 |
} |
60991 | 239 |
} |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
240 |
|
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
241 |
|
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
242 |
/* Scala function */ |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
243 |
|
73565 | 244 |
object Process extends Scala.Fun_Strings("bash_process", thread = true) |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
245 |
{ |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
246 |
val here = Scala_Project.here |
73565 | 247 |
def apply(args: List[String]): List[String] = |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
248 |
{ |
73604 | 249 |
val result = |
250 |
Exn.capture { |
|
251 |
val redirect = args.head == "true" |
|
252 |
val script = cat_lines(args.tail) |
|
253 |
Isabelle_System.bash(script, redirect = redirect) |
|
254 |
} |
|
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
255 |
|
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
256 |
val is_interrupt = |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
257 |
result match { |
73263
ad60214bef09
more uniform Bash.process: always ask Isabelle/Scala;
wenzelm
parents:
73230
diff
changeset
|
258 |
case Exn.Res(res) => res.rc == Exn.Interrupt.return_code |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
259 |
case Exn.Exn(exn) => Exn.is_interrupt(exn) |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
260 |
} |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
261 |
|
73268
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73265
diff
changeset
|
262 |
result match { |
73565 | 263 |
case _ if is_interrupt => Nil |
264 |
case Exn.Exn(exn) => List(Exn.message(exn)) |
|
73268
c8abfe393c16
more accurate process_result in ML, corresponding to Process_Result in Scala;
wenzelm
parents:
73265
diff
changeset
|
265 |
case Exn.Res(res) => |
73565 | 266 |
res.rc.toString :: |
267 |
res.timing.elapsed.ms.toString :: |
|
268 |
res.timing.cpu.ms.toString :: |
|
269 |
res.out_lines.length.toString :: |
|
270 |
res.out_lines ::: res.err_lines |
|
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
271 |
} |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
272 |
} |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
273 |
} |
60991 | 274 |
} |