author | wenzelm |
Mon, 06 Apr 2020 14:03:58 +0200 | |
changeset 71708 | dd9fc8a3036c |
parent 71707 | 2e602e278b77 |
child 71712 | c6b7f4da67b3 |
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 |
14 |
||
60991 | 15 |
|
16 |
object Bash |
|
17 |
{ |
|
64304 | 18 |
/* concrete syntax */ |
19 |
||
20 |
private def bash_chr(c: Byte): String = |
|
21 |
{ |
|
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 |
|
42 |
def strings(ss: List[String]): String = |
|
71601 | 43 |
ss.iterator.map(Bash.string).mkString(" ") |
64304 | 44 |
|
45 |
||
46 |
/* process and result */ |
|
47 |
||
62543 | 48 |
private class Limited_Progress(proc: Process, progress_limit: Option[Long]) |
49 |
{ |
|
50 |
private var count = 0L |
|
51 |
def apply(progress: String => Unit)(line: String): Unit = synchronized { |
|
52 |
progress(line) |
|
53 |
count = count + line.length + 1 |
|
54 |
progress_limit match { |
|
55 |
case Some(limit) if count > limit => proc.terminate |
|
56 |
case _ => |
|
57 |
} |
|
58 |
} |
|
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 |
|
79 |
private val script_file = Isabelle_System.tmp_file("bash_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
|
80 |
File.write(script_file, script) |
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
|
81 |
|
62296 | 82 |
private val proc = |
62610
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
83 |
Isabelle_System.process( |
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
84 |
List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", |
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
85 |
File.standard_path(timing_file), "bash", File.standard_path(script_file)), |
4c89504c76fb
more uniform signature for various process invocations;
wenzelm
parents:
62604
diff
changeset
|
86 |
cwd = cwd, env = env, redirect = redirect) |
60991 | 87 |
|
88 |
||
89 |
// channels |
|
90 |
||
91 |
val stdin: BufferedWriter = |
|
92 |
new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset)) |
|
93 |
||
94 |
val stdout: BufferedReader = |
|
95 |
new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset)) |
|
96 |
||
97 |
val stderr: BufferedReader = |
|
98 |
new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) |
|
99 |
||
100 |
||
101 |
// signals |
|
102 |
||
103 |
private val pid = stdout.readLine |
|
104 |
||
71707 | 105 |
@tailrec private def kill(signal: String, count: Int = 1): Boolean = |
60991 | 106 |
{ |
71706 | 107 |
count <= 0 || |
108 |
{ |
|
71707 | 109 |
Isabelle_System.kill(signal, pid) |
110 |
val running = Isabelle_System.kill("0", pid)._2 == 0 |
|
111 |
if (running) { |
|
71705 | 112 |
Time.seconds(0.1).sleep |
71707 | 113 |
kill(signal, count - 1) |
60991 | 114 |
} |
71706 | 115 |
else false |
60991 | 116 |
} |
117 |
} |
|
118 |
||
71705 | 119 |
def terminate(): Unit = Isabelle_Thread.uninterruptible |
62574 | 120 |
{ |
71708 | 121 |
kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL") |
62574 | 122 |
proc.destroy |
62602 | 123 |
do_cleanup() |
62574 | 124 |
} |
60991 | 125 |
|
71705 | 126 |
def interrupt(): Unit = Isabelle_Thread.uninterruptible |
127 |
{ |
|
128 |
Isabelle_System.kill("INT", pid) |
|
129 |
} |
|
130 |
||
60991 | 131 |
|
132 |
// JVM shutdown hook |
|
133 |
||
134 |
private val shutdown_hook = new Thread { override def run = terminate() } |
|
135 |
||
136 |
try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } |
|
137 |
catch { case _: IllegalStateException => } |
|
138 |
||
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
|
139 |
|
62574 | 140 |
// 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
|
141 |
|
62602 | 142 |
private def 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
|
143 |
{ |
60991 | 144 |
try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } |
145 |
catch { case _: IllegalStateException => } |
|
146 |
||
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
|
147 |
script_file.delete |
60991 | 148 |
|
62569 | 149 |
timing.change { |
150 |
case None => |
|
62574 | 151 |
if (timing_file.isFile) { |
152 |
val t = |
|
153 |
Word.explode(File.read(timing_file)) match { |
|
63805 | 154 |
case List(Value.Long(elapsed), Value.Long(cpu)) => |
62574 | 155 |
Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
156 |
case _ => Timing.zero |
|
157 |
} |
|
158 |
timing_file.delete |
|
159 |
Some(t) |
|
160 |
} |
|
161 |
else Some(Timing.zero) |
|
62569 | 162 |
case some => some |
163 |
} |
|
62602 | 164 |
|
165 |
cleanup() |
|
62574 | 166 |
} |
62569 | 167 |
|
62574 | 168 |
|
169 |
// join |
|
170 |
||
171 |
def join: Int = |
|
172 |
{ |
|
173 |
val rc = proc.waitFor |
|
62602 | 174 |
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
|
175 |
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
|
176 |
} |
62543 | 177 |
|
178 |
||
62574 | 179 |
// result |
62543 | 180 |
|
181 |
def result( |
|
182 |
progress_stdout: String => Unit = (_: String) => (), |
|
183 |
progress_stderr: String => Unit = (_: String) => (), |
|
184 |
progress_limit: Option[Long] = None, |
|
185 |
strict: Boolean = true): Process_Result = |
|
186 |
{ |
|
187 |
stdin.close |
|
188 |
||
189 |
val limited = new Limited_Progress(this, progress_limit) |
|
190 |
val out_lines = |
|
191 |
Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) } |
|
192 |
val err_lines = |
|
193 |
Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) } |
|
194 |
||
195 |
val rc = |
|
196 |
try { join } |
|
62574 | 197 |
catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } |
62543 | 198 |
if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() |
199 |
||
65317 | 200 |
Process_Result(rc, out_lines.join, err_lines.join, false, get_timing) |
62543 | 201 |
} |
60991 | 202 |
} |
203 |
} |