author | wenzelm |
Sun, 29 Aug 2021 12:04:55 +0200 | |
changeset 74212 | a1ccecae6a57 |
parent 74158 | 1cb0ad6f9a2d |
child 74273 | 0a4cdf0036a0 |
permissions | -rw-r--r-- |
62584 | 1 |
/* Title: Pure/System/bash.scala |
60991 | 2 |
Author: Makarius |
3 |
||
74158 | 4 |
Support for GNU bash: portable external processes with propagation of |
5 |
interrupts. |
|
60991 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
73897 | 11 |
import java.util.{LinkedList, List => JList, Map => JMap} |
73895 | 12 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, File => JFile} |
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 |
||
74212 | 49 |
private def make_description(description: String): String = |
50 |
proper_string(description) getOrElse "bash_process" |
|
51 |
||
72598 | 52 |
type Watchdog = (Time, Process => Boolean) |
53 |
||
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
|
54 |
def process(script: String, |
74212 | 55 |
description: String = "", |
62573 | 56 |
cwd: JFile = null, |
73897 | 57 |
env: JMap[String, String] = Isabelle_System.settings(), |
62602 | 58 |
redirect: Boolean = false, |
59 |
cleanup: () => Unit = () => ()): Process = |
|
74212 | 60 |
new Process(script, description, cwd, env, redirect, cleanup) |
60991 | 61 |
|
63996 | 62 |
class Process private[Bash]( |
62602 | 63 |
script: String, |
74212 | 64 |
description: String, |
62602 | 65 |
cwd: JFile, |
73897 | 66 |
env: JMap[String, String], |
62602 | 67 |
redirect: Boolean, |
68 |
cleanup: () => Unit) |
|
60991 | 69 |
{ |
74212 | 70 |
override def toString: String = make_description(description) |
71 |
||
62604 | 72 |
private val timing_file = Isabelle_System.tmp_file("bash_timing") |
62569 | 73 |
private val timing = Synchronized[Option[Timing]](None) |
65317 | 74 |
def get_timing: Timing = timing.value getOrElse Timing.zero |
62569 | 75 |
|
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
|
76 |
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
|
77 |
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
|
78 |
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
|
79 |
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
|
80 |
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
|
81 |
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
|
82 |
"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
|
83 |
"""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
|
84 |
} |
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 |
|
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 |
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
|
87 |
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
|
88 |
|
62296 | 89 |
private val proc = |
73906 | 90 |
isabelle.setup.Environment.process_builder( |
73895 | 91 |
JList.of(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), |
62610
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
92 |
File.standard_path(timing_file), "bash", File.standard_path(script_file)), |
73906 | 93 |
cwd, env, redirect).start() |
60991 | 94 |
|
95 |
||
96 |
// channels |
|
97 |
||
98 |
val stdin: BufferedWriter = |
|
99 |
new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) |
|
100 |
||
101 |
val stdout: BufferedReader = |
|
102 |
new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) |
|
103 |
||
104 |
val stderr: BufferedReader = |
|
105 |
new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) |
|
106 |
||
107 |
||
108 |
// signals |
|
109 |
||
73601 | 110 |
private val group_pid = stdout.readLine |
60991 | 111 |
|
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
|
112 |
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
|
113 |
(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
|
114 |
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
|
115 |
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
|
116 |
} 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
|
117 |
|
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 |
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
|
119 |
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
|
120 |
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
|
121 |
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
|
122 |
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
|
123 |
} |
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
|
124 |
|
73601 | 125 |
@tailrec private def signal(s: String, count: Int = 1): Boolean = |
60991 | 126 |
{ |
71706 | 127 |
count <= 0 || |
128 |
{ |
|
73911 | 129 |
isabelle.setup.Environment.kill_process(group_pid, s) |
130 |
val running = |
|
131 |
root_process_alive() || |
|
132 |
isabelle.setup.Environment.kill_process(group_pid, "0") |
|
71707 | 133 |
if (running) { |
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73604
diff
changeset
|
134 |
Time.seconds(0.1).sleep() |
73601 | 135 |
signal(s, count - 1) |
60991 | 136 |
} |
71706 | 137 |
else false |
60991 | 138 |
} |
139 |
} |
|
140 |
||
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71708
diff
changeset
|
141 |
def terminate(): Unit = Isabelle_Thread.try_uninterruptible |
62574 | 142 |
{ |
73601 | 143 |
signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL") |
73367 | 144 |
proc.destroy() |
62602 | 145 |
do_cleanup() |
62574 | 146 |
} |
60991 | 147 |
|
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71708
diff
changeset
|
148 |
def interrupt(): Unit = Isabelle_Thread.try_uninterruptible |
71705 | 149 |
{ |
73911 | 150 |
isabelle.setup.Environment.kill_process(group_pid, "INT") |
71705 | 151 |
} |
152 |
||
60991 | 153 |
|
154 |
// JVM shutdown hook |
|
155 |
||
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71708
diff
changeset
|
156 |
private val shutdown_hook = Isabelle_Thread.create(() => terminate()) |
60991 | 157 |
|
158 |
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } |
|
159 |
catch { case _: IllegalStateException => } |
|
160 |
||
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
|
161 |
|
62574 | 162 |
// 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
|
163 |
|
73340 | 164 |
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
|
165 |
{ |
60991 | 166 |
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } |
167 |
catch { case _: IllegalStateException => } |
|
168 |
||
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
|
169 |
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
|
170 |
winpid_file.foreach(_.delete()) |
60991 | 171 |
|
62569 | 172 |
timing.change { |
173 |
case None => |
|
62574 | 174 |
if (timing_file.isFile) { |
175 |
val t = |
|
176 |
Word.explode(File.read(timing_file)) match { |
|
63805 | 177 |
case List(Value.Long(elapsed), Value.Long(cpu)) => |
62574 | 178 |
Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
179 |
case _ => Timing.zero |
|
180 |
} |
|
181 |
timing_file.delete |
|
182 |
Some(t) |
|
183 |
} |
|
184 |
else Some(Timing.zero) |
|
62569 | 185 |
case some => some |
186 |
} |
|
62602 | 187 |
|
188 |
cleanup() |
|
62574 | 189 |
} |
62569 | 190 |
|
62574 | 191 |
|
192 |
// join |
|
193 |
||
74141 | 194 |
def join(): Int = |
62574 | 195 |
{ |
74141 | 196 |
val rc = proc.waitFor() |
62602 | 197 |
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
|
198 |
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
|
199 |
} |
62543 | 200 |
|
201 |
||
62574 | 202 |
// result |
62543 | 203 |
|
204 |
def result( |
|
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
205 |
input: String = "", |
62543 | 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 |
{ |
|
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
211 |
val in = |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
212 |
if (input.isEmpty) Future.value(stdin.close()) |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
213 |
else Future.thread("bash_stdin") { stdin.write(input); stdin.flush(); stdin.close(); } |
62543 | 214 |
val out_lines = |
72105 | 215 |
Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } |
62543 | 216 |
val err_lines = |
72105 | 217 |
Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } |
62543 | 218 |
|
72598 | 219 |
val watchdog_thread = |
220 |
for ((time, check) <- watchdog) |
|
221 |
yield { |
|
222 |
Future.thread("bash_watchdog") { |
|
223 |
while (proc.isAlive) { |
|
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73604
diff
changeset
|
224 |
time.sleep() |
72598 | 225 |
if (check(this)) interrupt() |
226 |
} |
|
227 |
} |
|
228 |
} |
|
229 |
||
62543 | 230 |
val rc = |
74141 | 231 |
try { join() } |
74067 | 232 |
catch { case Exn.Interrupt() => terminate(); Process_Result.interrupt_rc } |
72598 | 233 |
|
73367 | 234 |
watchdog_thread.foreach(_.cancel()) |
72598 | 235 |
|
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
236 |
in.join |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
237 |
out_lines.join |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
238 |
err_lines.join |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
239 |
|
74067 | 240 |
if (strict && rc == Process_Result.interrupt_rc) throw Exn.Interrupt() |
62543 | 241 |
|
73134
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
72598
diff
changeset
|
242 |
Process_Result(rc, out_lines.join, err_lines.join, get_timing) |
62543 | 243 |
} |
60991 | 244 |
} |
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 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
247 |
/* server */ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
248 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
249 |
object Server |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
250 |
{ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
251 |
// input messages |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
252 |
private val RUN = "run" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
253 |
private val KILL = "kill" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
254 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
255 |
// output messages |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
256 |
private val UUID = "uuid" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
257 |
private val INTERRUPT = "interrupt" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
258 |
private val FAILURE = "failure" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
259 |
private val RESULT = "result" |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
260 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
261 |
def start(port: Int = 0, debugging: => Boolean = false): Server = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
262 |
{ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
263 |
val server = new Server(port, debugging) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
264 |
server.start() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
265 |
server |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
266 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
267 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
268 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
269 |
class Server private(port: Int, debugging: => Boolean) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
270 |
extends isabelle.Server.Handler(port) |
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 |
{ |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
272 |
server => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
273 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
274 |
private val _processes = Synchronized(Map.empty[UUID.T, Bash.Process]) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
275 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
276 |
override def stop(): Unit = |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
277 |
{ |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
278 |
for ((_, process) <- _processes.value) process.terminate() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
279 |
super.stop() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
280 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
281 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
282 |
override def handle(connection: isabelle.Server.Connection): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
283 |
{ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
284 |
def reply(chunks: List[String]): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
285 |
connection.write_byte_message(chunks.map(Bytes.apply)) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
286 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
287 |
def reply_failure(exn: Throwable): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
288 |
reply( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
289 |
if (Exn.is_interrupt(exn)) List(Server.INTERRUPT) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
290 |
else List(Server.FAILURE, Exn.message(exn))) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
291 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
292 |
def reply_result(result: Process_Result): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
293 |
reply( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
294 |
Server.RESULT :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
295 |
result.rc.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
296 |
result.timing.elapsed.ms.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
297 |
result.timing.cpu.ms.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
298 |
result.out_lines.length.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
299 |
result.out_lines ::: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
300 |
result.err_lines) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
301 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
302 |
connection.read_byte_message().map(_.map(_.text)) match { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
303 |
case None => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
304 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
305 |
case Some(List(Server.KILL, UUID(uuid))) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
306 |
if (debugging) Output.writeln("kill " + uuid) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
307 |
_processes.value.get(uuid).foreach(_.terminate()) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
308 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
309 |
case Some(List(Server.RUN, script, input, cwd, putenv, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
310 |
Value.Boolean(redirect), Value.Seconds(timeout), description)) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
311 |
val uuid = UUID.random() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
312 |
|
74212 | 313 |
val descr = make_description(description) |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
314 |
if (debugging) { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
315 |
Output.writeln( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
316 |
"start " + quote(descr) + " (uuid=" + uuid + ", timeout=" + timeout.seconds + ")") |
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
317 |
} |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
318 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
319 |
Exn.capture { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
320 |
Bash.process(script, |
74212 | 321 |
description = description, |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
322 |
cwd = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
323 |
XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
324 |
case None => null |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
325 |
case Some(s) => Path.explode(s).file |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
326 |
}, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
327 |
env = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
328 |
Isabelle_System.settings( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
329 |
XML.Decode.list(XML.Decode.pair(XML.Decode.string, XML.Decode.string))( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
330 |
YXML.parse_body(putenv))), |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
331 |
redirect= redirect) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
332 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
333 |
match { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
334 |
case Exn.Exn(exn) => reply_failure(exn) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
335 |
case Exn.Res(process) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
336 |
_processes.change(processes => processes + (uuid -> process)) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
337 |
reply(List(Server.UUID, uuid.toString)) |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
338 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
339 |
Isabelle_Thread.fork(name = "bash_process") { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
340 |
@volatile var is_timeout = false |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
341 |
val watchdog: Option[Watchdog] = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
342 |
if (timeout.is_zero) None else Some((timeout, _ => { is_timeout = true; true })) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
343 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
344 |
Exn.capture { process.result(input = input, watchdog = watchdog, strict = false) } |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
345 |
match { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
346 |
case Exn.Exn(exn) => reply_failure(exn) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
347 |
case Exn.Res(res0) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
348 |
val res = if (!res0.ok && is_timeout) res0.timeout_rc else res0 |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
349 |
if (debugging) { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
350 |
Output.writeln( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
351 |
"stop " + quote(descr) + " (uuid=" + uuid + ", return_code=" + res.rc + ")") |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
352 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
353 |
reply_result(res) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
354 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
355 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
356 |
_processes.change(provers => provers - uuid) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
357 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
358 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
359 |
connection.await_close() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
360 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
361 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
362 |
case Some(_) => reply_failure(ERROR("Bad protocol message")) |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
363 |
} |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
364 |
} |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
365 |
} |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
366 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
367 |
class Handler extends Session.Protocol_Handler |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
368 |
{ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
369 |
private var server: Server = null |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
370 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
371 |
override def init(session: Session): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
372 |
{ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
373 |
exit() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
374 |
server = Server.start(debugging = session.session_options.bool("bash_process_debugging")) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
375 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
376 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
377 |
override def exit(): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
378 |
{ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
379 |
if (server != null) { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
380 |
server.stop() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
381 |
server = null |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
382 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
383 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
384 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
385 |
override def prover_options(options: Options): Options = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
386 |
{ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
387 |
val address = if (server == null) "" else server.address |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
388 |
val password = if (server == null) "" else server.password |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
389 |
options + |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
390 |
("bash_process_address=" + address) + |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
391 |
("bash_process_password=" + password) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
392 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
393 |
} |
60991 | 394 |
} |