author | wenzelm |
Sat, 01 Jun 2024 14:33:38 +0200 | |
changeset 80227 | af6b60c75d7d |
parent 80224 | db92e0b6a11a |
child 80228 | df84e8ff4839 |
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 |
||
80218 | 11 |
import java.util.{List => JList, Map => JMap, LinkedList} |
74273
0a4cdf0036a0
more robust: client could have terminated already;
wenzelm
parents:
74212
diff
changeset
|
12 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, |
0a4cdf0036a0
more robust: client could have terminated already;
wenzelm
parents:
74212
diff
changeset
|
13 |
File => JFile, IOException} |
71706 | 14 |
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
|
15 |
import scala.jdk.OptionConverters._ |
71706 | 16 |
|
60991 | 17 |
|
75393 | 18 |
object Bash { |
64304 | 19 |
/* concrete syntax */ |
20 |
||
75393 | 21 |
private def bash_chr(c: Byte): String = { |
64304 | 22 |
val ch = c.toChar |
23 |
ch match { |
|
24 |
case '\t' => "$'\\t'" |
|
25 |
case '\n' => "$'\\n'" |
|
26 |
case '\f' => "$'\\f'" |
|
27 |
case '\r' => "$'\\r'" |
|
28 |
case _ => |
|
67200 | 29 |
if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch)) |
64304 | 30 |
Symbol.ascii(ch) |
31 |
else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" |
|
32 |
else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" |
|
33 |
else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" |
|
34 |
else "\\" + ch |
|
35 |
} |
|
36 |
} |
|
37 |
||
38 |
def string(s: String): String = |
|
39 |
if (s == "") "\"\"" |
|
71601 | 40 |
else UTF8.bytes(s).iterator.map(bash_chr).mkString |
64304 | 41 |
|
78910 | 42 |
def strings(ss: Iterable[String]): String = |
71601 | 43 |
ss.iterator.map(Bash.string).mkString(" ") |
64304 | 44 |
|
45 |
||
46 |
/* process and result */ |
|
47 |
||
80227
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
48 |
def context(script: String, |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
49 |
user_home: String = "", |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
50 |
isabelle_identifier: String = "", |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
51 |
cwd: Path = Path.current |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
52 |
): String = { |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
53 |
if_proper(user_home, |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
54 |
"export USER_HOME=" + Bash.string(user_home) + "\n") + |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
55 |
if_proper(isabelle_identifier, |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
56 |
"export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n") + |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
57 |
(if (cwd == null || cwd.is_current) "" else "cd " + quote(cwd.implode) + "\n") + |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
58 |
script |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
59 |
} |
af6b60c75d7d
clarified context for (remote) bash scripts: export variables are optional, support cwd;
wenzelm
parents:
80224
diff
changeset
|
60 |
|
74212 | 61 |
private def make_description(description: String): String = |
62 |
proper_string(description) getOrElse "bash_process" |
|
63 |
||
80218 | 64 |
def local_bash_process(): String = |
65 |
File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")) |
|
66 |
||
67 |
def local_bash(): String = |
|
68 |
if (Platform.is_unix) "bash" |
|
69 |
else isabelle.setup.Environment.cygwin_root() + "\\bin\\bash.exe" |
|
70 |
||
71 |
def remote_bash_process(ssh: SSH.Session): String = { |
|
72 |
val component = Components.provide(Component_Bash_Process.home, ssh = ssh) |
|
73 |
val exe = Component_Bash_Process.remote_program(component) |
|
74 |
ssh.make_command(args_host = true, args = ssh.bash_path(exe)) |
|
75 |
} |
|
76 |
||
72598 | 77 |
type Watchdog = (Time, Process => Boolean) |
78 |
||
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
|
79 |
def process(script: String, |
74212 | 80 |
description: String = "", |
80218 | 81 |
ssh: SSH.System = SSH.Local, |
80224
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
82 |
cwd: Path = Path.current, |
73897 | 83 |
env: JMap[String, String] = Isabelle_System.settings(), |
62602 | 84 |
redirect: Boolean = false, |
85 |
cleanup: () => Unit = () => ()): Process = |
|
80218 | 86 |
new Process(script, description, ssh, cwd, env, redirect, cleanup) |
60991 | 87 |
|
63996 | 88 |
class Process private[Bash]( |
75393 | 89 |
script: String, |
90 |
description: String, |
|
80218 | 91 |
ssh: SSH.System, |
80224
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
92 |
cwd: Path, |
75393 | 93 |
env: JMap[String, String], |
94 |
redirect: Boolean, |
|
95 |
cleanup: () => Unit |
|
96 |
) { |
|
74212 | 97 |
override def toString: String = make_description(description) |
98 |
||
80218 | 99 |
private val proc_command: JList[String] = new LinkedList[String] |
100 |
||
101 |
private val winpid_file: Option[JFile] = |
|
102 |
if (ssh.is_local && Platform.is_windows) Some(Isabelle_System.tmp_file("bash_winpid")) |
|
103 |
else None |
|
104 |
private val winpid_script = |
|
105 |
winpid_file match { |
|
106 |
case None => "" |
|
107 |
case Some(file) => |
|
108 |
"read < /proc/self/winpid > /dev/null 2> /dev/null\n" + |
|
109 |
"""echo -n "$REPLY" > """ + File.bash_path(file) + "\n\n" |
|
110 |
} |
|
111 |
||
80220
928e02d0cab7
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80218
diff
changeset
|
112 |
private val List(timing_file, script_file) = |
928e02d0cab7
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80218
diff
changeset
|
113 |
ssh.tmp_files(List("bash_timing", "bash_script")) |
928e02d0cab7
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80218
diff
changeset
|
114 |
|
62569 | 115 |
private val timing = Synchronized[Option[Timing]](None) |
65317 | 116 |
def get_timing: Timing = timing.value getOrElse Timing.zero |
62569 | 117 |
|
80218 | 118 |
ssh.write(script_file, winpid_script + script) |
119 |
||
120 |
private val ssh_file: Option[JFile] = |
|
121 |
ssh.ssh_session match { |
|
122 |
case None => |
|
123 |
proc_command.add(local_bash_process()) |
|
124 |
proc_command.add(File.platform_path(timing_file)) |
|
125 |
proc_command.add("bash") |
|
126 |
proc_command.add(File.platform_path(script_file)) |
|
127 |
None |
|
128 |
case Some(ssh_session) => |
|
129 |
val ssh_script = |
|
130 |
"exec " + remote_bash_process(ssh_session) + " " + |
|
131 |
ssh.bash_path(timing_file) + " bash " + |
|
132 |
ssh.bash_path(script_file) |
|
133 |
val file = Isabelle_System.tmp_file("bash_ssh") |
|
134 |
File.write(file, ssh_script) |
|
135 |
proc_command.add(local_bash()) |
|
136 |
proc_command.add(file.getPath) |
|
137 |
Some(file) |
|
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
|
138 |
} |
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
|
139 |
|
62296 | 140 |
private val proc = |
80224
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
141 |
isabelle.setup.Environment.process_builder( |
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
142 |
proc_command, |
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
143 |
if (cwd == null || cwd.is_current) null else cwd.file, |
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
144 |
env, |
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
145 |
redirect |
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
146 |
).start() |
60991 | 147 |
|
148 |
||
149 |
// channels |
|
150 |
||
151 |
val stdin: BufferedWriter = |
|
152 |
new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) |
|
153 |
||
154 |
val stdout: BufferedReader = |
|
155 |
new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) |
|
156 |
||
157 |
val stderr: BufferedReader = |
|
158 |
new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) |
|
159 |
||
160 |
||
161 |
// signals |
|
162 |
||
73601 | 163 |
private val group_pid = stdout.readLine |
60991 | 164 |
|
80218 | 165 |
private def local_process_alive(pid: String): Boolean = |
166 |
ssh.is_local && |
|
167 |
(for { |
|
168 |
p <- Value.Long.unapply(pid) |
|
169 |
handle <- ProcessHandle.of(p).toScala |
|
170 |
} yield handle.isAlive).getOrElse(false) |
|
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
|
171 |
|
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
|
172 |
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
|
173 |
winpid_file match { |
80218 | 174 |
case None => local_process_alive(group_pid) |
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
|
175 |
case Some(file) => |
80218 | 176 |
file.exists() && local_process_alive(Library.trim_line(File.read(file))) |
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
|
177 |
} |
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
|
178 |
|
75393 | 179 |
@tailrec private def signal(s: String, count: Int = 1): Boolean = { |
180 |
count <= 0 || { |
|
80218 | 181 |
ssh.kill_process(group_pid, s) |
182 |
val running = root_process_alive() || ssh.kill_process(group_pid, "0") |
|
71707 | 183 |
if (running) { |
80218 | 184 |
Time.seconds(if (ssh.is_local) 0.1 else 0.25).sleep() |
73601 | 185 |
signal(s, count - 1) |
60991 | 186 |
} |
71706 | 187 |
else false |
60991 | 188 |
} |
189 |
} |
|
190 |
||
75393 | 191 |
def terminate(): Unit = Isabelle_Thread.try_uninterruptible { |
73601 | 192 |
signal("INT", count = 7) && signal("TERM", count = 3) && signal("KILL") |
73367 | 193 |
proc.destroy() |
62602 | 194 |
do_cleanup() |
62574 | 195 |
} |
60991 | 196 |
|
75393 | 197 |
def interrupt(): Unit = Isabelle_Thread.try_uninterruptible { |
80218 | 198 |
ssh.kill_process(group_pid, "INT") |
71705 | 199 |
} |
200 |
||
60991 | 201 |
|
62574 | 202 |
// 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
|
203 |
|
76146 | 204 |
private val shutdown_hook = |
205 |
Isabelle_System.create_shutdown_hook { terminate() } |
|
206 |
||
75393 | 207 |
private def do_cleanup(): Unit = { |
76146 | 208 |
Isabelle_System.remove_shutdown_hook(shutdown_hook) |
60991 | 209 |
|
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
|
210 |
winpid_file.foreach(_.delete()) |
80218 | 211 |
ssh_file.foreach(_.delete()) |
212 |
||
62569 | 213 |
timing.change { |
214 |
case None => |
|
80221
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
215 |
val timing_text = |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
216 |
try { ssh.read(timing_file) } |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
217 |
catch { case ERROR(_) => "" } |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
218 |
val t = |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
219 |
Word.explode(timing_text) match { |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
220 |
case List(Value.Long(elapsed), Value.Long(cpu)) => |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
221 |
Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
222 |
case _ => Timing.zero |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
223 |
} |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
224 |
Some(t) |
62569 | 225 |
case some => some |
226 |
} |
|
62602 | 227 |
|
80221
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
228 |
ssh.delete(timing_file, script_file) |
0d89f0a39854
minor performance tuning: save approx. 70ms per SSH command;
wenzelm
parents:
80220
diff
changeset
|
229 |
|
62602 | 230 |
cleanup() |
62574 | 231 |
} |
62569 | 232 |
|
62574 | 233 |
|
234 |
// join |
|
235 |
||
75393 | 236 |
def join(): Int = { |
74141 | 237 |
val rc = proc.waitFor() |
62602 | 238 |
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
|
239 |
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
|
240 |
} |
62543 | 241 |
|
242 |
||
62574 | 243 |
// result |
62543 | 244 |
|
245 |
def result( |
|
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
246 |
input: String = "", |
62543 | 247 |
progress_stdout: String => Unit = (_: String) => (), |
248 |
progress_stderr: String => Unit = (_: String) => (), |
|
72598 | 249 |
watchdog: Option[Watchdog] = None, |
75393 | 250 |
strict: Boolean = true |
251 |
): Process_Result = { |
|
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
252 |
val in = |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
253 |
if (input.isEmpty) Future.value(stdin.close()) |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
254 |
else Future.thread("bash_stdin") { stdin.write(input); stdin.flush(); stdin.close(); } |
62543 | 255 |
val out_lines = |
72105 | 256 |
Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } |
62543 | 257 |
val err_lines = |
72105 | 258 |
Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } |
62543 | 259 |
|
72598 | 260 |
val watchdog_thread = |
261 |
for ((time, check) <- watchdog) |
|
262 |
yield { |
|
263 |
Future.thread("bash_watchdog") { |
|
264 |
while (proc.isAlive) { |
|
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73604
diff
changeset
|
265 |
time.sleep() |
72598 | 266 |
if (check(this)) interrupt() |
267 |
} |
|
268 |
} |
|
269 |
} |
|
270 |
||
62543 | 271 |
val rc = |
74141 | 272 |
try { join() } |
74306 | 273 |
catch { case Exn.Interrupt() => terminate(); Process_Result.RC.interrupt } |
72598 | 274 |
|
73367 | 275 |
watchdog_thread.foreach(_.cancel()) |
72598 | 276 |
|
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
277 |
in.join |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
278 |
out_lines.join |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
279 |
err_lines.join |
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
280 |
|
74306 | 281 |
if (strict && rc == Process_Result.RC.interrupt) throw Exn.Interrupt() |
62543 | 282 |
|
73134
8a8ffe78eee7
clarified return code: re-use SIGALRM for soft timeout;
wenzelm
parents:
72598
diff
changeset
|
283 |
Process_Result(rc, out_lines.join, err_lines.join, get_timing) |
62543 | 284 |
} |
60991 | 285 |
} |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
286 |
|
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
287 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
288 |
/* server */ |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
289 |
|
75393 | 290 |
object Server { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
291 |
// input messages |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
292 |
private val RUN = "run" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
293 |
private val KILL = "kill" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
294 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
295 |
// output messages |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
296 |
private val UUID = "uuid" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
297 |
private val INTERRUPT = "interrupt" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
298 |
private val FAILURE = "failure" |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
299 |
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
|
300 |
|
75393 | 301 |
def start(port: Int = 0, debugging: => Boolean = false): Server = { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
302 |
val server = new Server(port, debugging) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
303 |
server.start() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
304 |
server |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
305 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
306 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
307 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
308 |
class Server private(port: Int, debugging: => Boolean) |
75393 | 309 |
extends isabelle.Server.Handler(port) { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
310 |
server => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
311 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
312 |
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
|
313 |
|
75393 | 314 |
override def stop(): Unit = { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
315 |
for ((_, process) <- _processes.value) process.terminate() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
316 |
super.stop() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
317 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
318 |
|
75393 | 319 |
override def handle(connection: isabelle.Server.Connection): Unit = { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
320 |
def reply(chunks: List[String]): Unit = |
74273
0a4cdf0036a0
more robust: client could have terminated already;
wenzelm
parents:
74212
diff
changeset
|
321 |
try { connection.write_byte_message(chunks.map(Bytes.apply)) } |
0a4cdf0036a0
more robust: client could have terminated already;
wenzelm
parents:
74212
diff
changeset
|
322 |
catch { case _: IOException => } |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
323 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
324 |
def reply_failure(exn: Throwable): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
325 |
reply( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
326 |
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
|
327 |
else List(Server.FAILURE, Exn.message(exn))) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
328 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
329 |
def reply_result(result: Process_Result): Unit = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
330 |
reply( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
331 |
Server.RESULT :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
332 |
result.rc.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
333 |
result.timing.elapsed.ms.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
334 |
result.timing.cpu.ms.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
335 |
result.out_lines.length.toString :: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
336 |
result.out_lines ::: |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
337 |
result.err_lines) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
338 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
339 |
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
|
340 |
case None => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
341 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
342 |
case Some(List(Server.KILL, UUID(uuid))) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
343 |
if (debugging) Output.writeln("kill " + uuid) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
344 |
_processes.value.get(uuid).foreach(_.terminate()) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
345 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
346 |
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
|
347 |
Value.Boolean(redirect), Value.Seconds(timeout), description)) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
348 |
val uuid = UUID.random() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
349 |
|
74212 | 350 |
val descr = make_description(description) |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
351 |
if (debugging) { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
352 |
Output.writeln( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
353 |
"start " + quote(descr) + " (uuid=" + uuid + ", timeout=" + timeout.seconds + ")") |
74142
0f051404f487
clarified signature: more options for bash_process;
wenzelm
parents:
74141
diff
changeset
|
354 |
} |
73228
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
355 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
356 |
Exn.capture { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
357 |
Bash.process(script, |
74212 | 358 |
description = description, |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
359 |
cwd = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
360 |
XML.Decode.option(XML.Decode.string)(YXML.parse_body(cwd)) match { |
80224
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
361 |
case None => Path.current |
db92e0b6a11a
clarified signature: prefer symbolic isabelle.Path over physical java.io.File;
wenzelm
parents:
80221
diff
changeset
|
362 |
case Some(s) => Path.explode(s) |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
363 |
}, |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
364 |
env = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
365 |
Isabelle_System.settings( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
366 |
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
|
367 |
YXML.parse_body(putenv))), |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
368 |
redirect= redirect) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
369 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
370 |
match { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
371 |
case Exn.Exn(exn) => reply_failure(exn) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
372 |
case Exn.Res(process) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
373 |
_processes.change(processes => processes + (uuid -> process)) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
374 |
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
|
375 |
|
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
376 |
Isabelle_Thread.fork(name = "bash_process") { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
377 |
@volatile var is_timeout = false |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
378 |
val watchdog: Option[Watchdog] = |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
379 |
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
|
380 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
381 |
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
|
382 |
match { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
383 |
case Exn.Exn(exn) => reply_failure(exn) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
384 |
case Exn.Res(res0) => |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
385 |
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
|
386 |
if (debugging) { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
387 |
Output.writeln( |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
388 |
"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
|
389 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
390 |
reply_result(res) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
391 |
} |
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 |
_processes.change(provers => provers - uuid) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
394 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
395 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
396 |
connection.await_close() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
397 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
398 |
|
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
399 |
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
|
400 |
} |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
401 |
} |
0575cfd2ecfc
support multi-threaded Bash.process invocation on Apple Silicon, where Poly/ML is running on Rosetta 2;
wenzelm
parents:
73134
diff
changeset
|
402 |
} |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
403 |
|
75393 | 404 |
class Handler extends Session.Protocol_Handler { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
405 |
private var server: Server = null |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
406 |
|
75393 | 407 |
override def init(session: Session): Unit = { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
408 |
exit() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
409 |
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
|
410 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
411 |
|
75393 | 412 |
override def exit(): Unit = { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
413 |
if (server != null) { |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
414 |
server.stop() |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
415 |
server = null |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
416 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
417 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
418 |
|
75393 | 419 |
override def prover_options(options: Options): Options = { |
74147
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
420 |
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
|
421 |
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
|
422 |
options + |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
423 |
("bash_process_address=" + address) + |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
424 |
("bash_process_password=" + password) |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
425 |
} |
d030b988d470
provide bash_process server for Isabelle/ML and other external programs;
wenzelm
parents:
74142
diff
changeset
|
426 |
} |
60991 | 427 |
} |