wenzelm@30174
|
1 |
/* Title: Pure/System/isabelle_process.ML
|
wenzelm@27949
|
2 |
Author: Makarius
|
wenzelm@27963
|
3 |
Options: :folding=explicit:collapseFolds=1:
|
wenzelm@27949
|
4 |
|
wenzelm@27949
|
5 |
Isabelle process management -- always reactive due to multi-threaded I/O.
|
wenzelm@27949
|
6 |
*/
|
wenzelm@27949
|
7 |
|
wenzelm@27949
|
8 |
package isabelle
|
wenzelm@27949
|
9 |
|
wenzelm@27955
|
10 |
import java.util.concurrent.LinkedBlockingQueue
|
wenzelm@28045
|
11 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
|
wenzelm@38568
|
12 |
InputStream, OutputStream, BufferedOutputStream, IOException}
|
wenzelm@27949
|
13 |
|
wenzelm@32485
|
14 |
import scala.actors.Actor
|
wenzelm@32485
|
15 |
import Actor._
|
wenzelm@27949
|
16 |
|
wenzelm@27973
|
17 |
|
wenzelm@32485
|
18 |
object Isabelle_Process
|
wenzelm@32485
|
19 |
{
|
wenzelm@27949
|
20 |
/* results */
|
wenzelm@27949
|
21 |
|
wenzelm@37705
|
22 |
object Kind {
|
wenzelm@29522
|
23 |
// message markup
|
wenzelm@29522
|
24 |
val markup = Map(
|
wenzelm@37705
|
25 |
('A' : Int) -> Markup.INIT,
|
wenzelm@37705
|
26 |
('B' : Int) -> Markup.STATUS,
|
wenzelm@38492
|
27 |
('C' : Int) -> Markup.REPORT,
|
wenzelm@38492
|
28 |
('D' : Int) -> Markup.WRITELN,
|
wenzelm@38492
|
29 |
('E' : Int) -> Markup.TRACING,
|
wenzelm@38492
|
30 |
('F' : Int) -> Markup.WARNING,
|
wenzelm@39782
|
31 |
('G' : Int) -> Markup.ERROR)
|
wenzelm@37705
|
32 |
def is_raw(kind: String) =
|
wenzelm@37705
|
33 |
kind == Markup.STDOUT
|
wenzelm@37705
|
34 |
def is_control(kind: String) =
|
wenzelm@37705
|
35 |
kind == Markup.SYSTEM ||
|
wenzelm@37705
|
36 |
kind == Markup.SIGNAL ||
|
wenzelm@37705
|
37 |
kind == Markup.EXIT
|
wenzelm@37705
|
38 |
def is_system(kind: String) =
|
wenzelm@37705
|
39 |
kind == Markup.SYSTEM ||
|
wenzelm@38557
|
40 |
kind == Markup.INPUT ||
|
wenzelm@37705
|
41 |
kind == Markup.STDIN ||
|
wenzelm@37705
|
42 |
kind == Markup.SIGNAL ||
|
wenzelm@37705
|
43 |
kind == Markup.EXIT ||
|
wenzelm@37705
|
44 |
kind == Markup.STATUS
|
wenzelm@27949
|
45 |
}
|
wenzelm@27949
|
46 |
|
wenzelm@37705
|
47 |
class Result(val message: XML.Elem)
|
wenzelm@34106
|
48 |
{
|
wenzelm@38486
|
49 |
def kind = message.markup.name
|
wenzelm@38486
|
50 |
def properties = message.markup.properties
|
wenzelm@37705
|
51 |
def body = message.body
|
wenzelm@37705
|
52 |
|
wenzelm@37705
|
53 |
def is_raw = Kind.is_raw(kind)
|
wenzelm@37705
|
54 |
def is_control = Kind.is_control(kind)
|
wenzelm@37705
|
55 |
def is_system = Kind.is_system(kind)
|
wenzelm@37705
|
56 |
def is_status = kind == Markup.STATUS
|
wenzelm@38492
|
57 |
def is_report = kind == Markup.REPORT
|
wenzelm@38487
|
58 |
def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
|
wenzelm@34106
|
59 |
|
wenzelm@34106
|
60 |
override def toString: String =
|
wenzelm@34106
|
61 |
{
|
wenzelm@29522
|
62 |
val res =
|
wenzelm@38492
|
63 |
if (is_status || is_report) message.body.map(_.toString).mkString
|
wenzelm@37705
|
64 |
else Pretty.string_of(message.body)
|
wenzelm@38486
|
65 |
if (properties.isEmpty)
|
wenzelm@29572
|
66 |
kind.toString + " [[" + res + "]]"
|
wenzelm@29572
|
67 |
else
|
wenzelm@29572
|
68 |
kind.toString + " " +
|
wenzelm@38486
|
69 |
(for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
|
wenzelm@27949
|
70 |
}
|
wenzelm@27973
|
71 |
}
|
wenzelm@27973
|
72 |
}
|
wenzelm@27973
|
73 |
|
wenzelm@27973
|
74 |
|
wenzelm@34106
|
75 |
class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*)
|
wenzelm@29192
|
76 |
{
|
wenzelm@31800
|
77 |
import Isabelle_Process._
|
wenzelm@29194
|
78 |
|
wenzelm@27973
|
79 |
|
wenzelm@29192
|
80 |
/* demo constructor */
|
wenzelm@27973
|
81 |
|
wenzelm@29192
|
82 |
def this(args: String*) =
|
wenzelm@32485
|
83 |
this(new Isabelle_System,
|
wenzelm@34213
|
84 |
actor { loop { react { case res => Console.println(res) } } }, args: _*)
|
wenzelm@29174
|
85 |
|
wenzelm@29174
|
86 |
|
wenzelm@27973
|
87 |
/* process information */
|
wenzelm@27973
|
88 |
|
wenzelm@38568
|
89 |
@volatile private var proc: Option[Process] = None
|
wenzelm@38568
|
90 |
@volatile private var pid: Option[String] = None
|
wenzelm@27973
|
91 |
|
wenzelm@27973
|
92 |
|
wenzelm@27973
|
93 |
/* results */
|
wenzelm@27949
|
94 |
|
wenzelm@38692
|
95 |
private val xml_cache = new XML.Cache(131071)
|
wenzelm@38692
|
96 |
|
wenzelm@38867
|
97 |
private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
|
wenzelm@29572
|
98 |
{
|
wenzelm@38692
|
99 |
if (pid.isEmpty && kind == Markup.INIT)
|
wenzelm@38692
|
100 |
pid = props.find(_._1 == Markup.PID).map(_._1)
|
wenzelm@38692
|
101 |
|
wenzelm@39748
|
102 |
val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
|
wenzelm@39748
|
103 |
xml_cache.cache_tree(msg)((message: XML.Tree) =>
|
wenzelm@38692
|
104 |
receiver ! new Result(message.asInstanceOf[XML.Elem]))
|
wenzelm@34106
|
105 |
}
|
wenzelm@34106
|
106 |
|
wenzelm@37705
|
107 |
private def put_result(kind: String, text: String)
|
wenzelm@34106
|
108 |
{
|
wenzelm@34106
|
109 |
put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
|
wenzelm@27992
|
110 |
}
|
wenzelm@27992
|
111 |
|
wenzelm@27973
|
112 |
|
wenzelm@27973
|
113 |
/* signals */
|
wenzelm@27973
|
114 |
|
wenzelm@38568
|
115 |
def interrupt()
|
wenzelm@38568
|
116 |
{
|
wenzelm@38568
|
117 |
if (proc.isEmpty) put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: no process")
|
wenzelm@38568
|
118 |
else
|
wenzelm@38568
|
119 |
pid match {
|
wenzelm@38568
|
120 |
case None => put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: unknowd pid")
|
wenzelm@38568
|
121 |
case Some(i) =>
|
wenzelm@38568
|
122 |
try {
|
wenzelm@38568
|
123 |
if (system.execute(true, "kill", "-INT", i).waitFor == 0)
|
wenzelm@38568
|
124 |
put_result(Markup.SIGNAL, "INT")
|
wenzelm@38568
|
125 |
else
|
wenzelm@38568
|
126 |
put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: kill command failed")
|
wenzelm@38568
|
127 |
}
|
wenzelm@38568
|
128 |
catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
|
wenzelm@27973
|
129 |
}
|
wenzelm@38568
|
130 |
}
|
wenzelm@38568
|
131 |
|
wenzelm@38568
|
132 |
def kill()
|
wenzelm@38568
|
133 |
{
|
wenzelm@38568
|
134 |
proc match {
|
wenzelm@38568
|
135 |
case None => put_result(Markup.SYSTEM, "Cannot kill Isabelle: no process")
|
wenzelm@38568
|
136 |
case Some(p) =>
|
wenzelm@38568
|
137 |
close()
|
wenzelm@38568
|
138 |
Thread.sleep(500) // FIXME !?
|
wenzelm@38568
|
139 |
put_result(Markup.SIGNAL, "KILL")
|
wenzelm@38568
|
140 |
p.destroy
|
wenzelm@38568
|
141 |
proc = None
|
wenzelm@38568
|
142 |
pid = None
|
wenzelm@27973
|
143 |
}
|
wenzelm@27973
|
144 |
}
|
wenzelm@27973
|
145 |
|
wenzelm@27949
|
146 |
|
wenzelm@27949
|
147 |
|
wenzelm@38557
|
148 |
/** stream actors **/
|
wenzelm@27949
|
149 |
|
wenzelm@39788
|
150 |
private val in_fifo = system.mk_fifo()
|
wenzelm@39788
|
151 |
private val out_fifo = system.mk_fifo()
|
wenzelm@39788
|
152 |
private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
|
wenzelm@39788
|
153 |
|
wenzelm@39788
|
154 |
private case class Input_Text(text: String)
|
wenzelm@39788
|
155 |
private case class Input_Chunks(chunks: List[Array[Byte]])
|
wenzelm@39788
|
156 |
private case object Close
|
wenzelm@27949
|
157 |
|
wenzelm@38568
|
158 |
|
wenzelm@38568
|
159 |
/* raw stdin */
|
wenzelm@38568
|
160 |
|
wenzelm@38568
|
161 |
private def stdin_actor(name: String, stream: OutputStream): Actor =
|
wenzelm@38895
|
162 |
Simple_Thread.actor(name) {
|
wenzelm@38551
|
163 |
val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
|
wenzelm@27949
|
164 |
var finished = false
|
wenzelm@27949
|
165 |
while (!finished) {
|
wenzelm@27949
|
166 |
try {
|
wenzelm@27949
|
167 |
//{{{
|
wenzelm@38557
|
168 |
receive {
|
wenzelm@38568
|
169 |
case Input_Text(text) =>
|
wenzelm@38568
|
170 |
// FIXME echo input?!
|
wenzelm@38557
|
171 |
writer.write(text)
|
wenzelm@38557
|
172 |
writer.flush
|
wenzelm@38557
|
173 |
case Close =>
|
wenzelm@38557
|
174 |
writer.close
|
wenzelm@38557
|
175 |
finished = true
|
wenzelm@38557
|
176 |
case bad => System.err.println(name + ": ignoring bad message " + bad)
|
wenzelm@27949
|
177 |
}
|
wenzelm@27949
|
178 |
//}}}
|
wenzelm@27949
|
179 |
}
|
wenzelm@27949
|
180 |
catch {
|
wenzelm@38557
|
181 |
case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
|
wenzelm@27949
|
182 |
}
|
wenzelm@27949
|
183 |
}
|
wenzelm@38557
|
184 |
put_result(Markup.SYSTEM, name + " terminated")
|
wenzelm@27949
|
185 |
}
|
wenzelm@27949
|
186 |
|
wenzelm@27949
|
187 |
|
wenzelm@38568
|
188 |
/* raw stdout */
|
wenzelm@27949
|
189 |
|
wenzelm@38568
|
190 |
private def stdout_actor(name: String, stream: InputStream): Actor =
|
wenzelm@38895
|
191 |
Simple_Thread.actor(name) {
|
wenzelm@38551
|
192 |
val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
|
wenzelm@27949
|
193 |
var result = new StringBuilder(100)
|
wenzelm@27949
|
194 |
|
wenzelm@27949
|
195 |
var finished = false
|
wenzelm@27949
|
196 |
while (!finished) {
|
wenzelm@27949
|
197 |
try {
|
wenzelm@27949
|
198 |
//{{{
|
wenzelm@27949
|
199 |
var c = -1
|
wenzelm@27949
|
200 |
var done = false
|
wenzelm@27949
|
201 |
while (!done && (result.length == 0 || reader.ready)) {
|
wenzelm@27949
|
202 |
c = reader.read
|
wenzelm@28045
|
203 |
if (c >= 0) result.append(c.asInstanceOf[Char])
|
wenzelm@27949
|
204 |
else done = true
|
wenzelm@27949
|
205 |
}
|
wenzelm@27949
|
206 |
if (result.length > 0) {
|
wenzelm@38568
|
207 |
put_result(Markup.STDOUT, result.toString)
|
wenzelm@27949
|
208 |
result.length = 0
|
wenzelm@27949
|
209 |
}
|
wenzelm@27949
|
210 |
else {
|
wenzelm@27949
|
211 |
reader.close
|
wenzelm@27949
|
212 |
finished = true
|
wenzelm@38568
|
213 |
close()
|
wenzelm@38568
|
214 |
}
|
wenzelm@38568
|
215 |
//}}}
|
wenzelm@38568
|
216 |
}
|
wenzelm@38568
|
217 |
catch {
|
wenzelm@38568
|
218 |
case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
|
wenzelm@38568
|
219 |
}
|
wenzelm@38568
|
220 |
}
|
wenzelm@38568
|
221 |
put_result(Markup.SYSTEM, name + " terminated")
|
wenzelm@38568
|
222 |
}
|
wenzelm@38568
|
223 |
|
wenzelm@38568
|
224 |
|
wenzelm@38568
|
225 |
/* command input */
|
wenzelm@38568
|
226 |
|
wenzelm@39788
|
227 |
private def input_actor(name: String): Actor =
|
wenzelm@38895
|
228 |
Simple_Thread.actor(name) {
|
wenzelm@39788
|
229 |
val stream = new BufferedOutputStream(system.fifo_output_stream(in_fifo)) // FIXME potentially blocking forever
|
wenzelm@38568
|
230 |
var finished = false
|
wenzelm@38568
|
231 |
while (!finished) {
|
wenzelm@38568
|
232 |
try {
|
wenzelm@38568
|
233 |
//{{{
|
wenzelm@38568
|
234 |
receive {
|
wenzelm@38568
|
235 |
case Input_Chunks(chunks) =>
|
wenzelm@38568
|
236 |
stream.write(Standard_System.string_bytes(
|
wenzelm@38568
|
237 |
chunks.map(_.length).mkString("", ",", "\n")));
|
wenzelm@38568
|
238 |
chunks.foreach(stream.write(_));
|
wenzelm@38568
|
239 |
stream.flush
|
wenzelm@38568
|
240 |
case Close =>
|
wenzelm@38568
|
241 |
stream.close
|
wenzelm@38568
|
242 |
finished = true
|
wenzelm@38568
|
243 |
case bad => System.err.println(name + ": ignoring bad message " + bad)
|
wenzelm@27949
|
244 |
}
|
wenzelm@27949
|
245 |
//}}}
|
wenzelm@27963
|
246 |
}
|
wenzelm@27963
|
247 |
catch {
|
wenzelm@38557
|
248 |
case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
|
wenzelm@27949
|
249 |
}
|
wenzelm@27949
|
250 |
}
|
wenzelm@38557
|
251 |
put_result(Markup.SYSTEM, name + " terminated")
|
wenzelm@27949
|
252 |
}
|
wenzelm@27949
|
253 |
|
wenzelm@27949
|
254 |
|
wenzelm@38557
|
255 |
/* message output */
|
wenzelm@27949
|
256 |
|
wenzelm@38557
|
257 |
private class Protocol_Error(msg: String) extends Exception(msg)
|
wenzelm@38557
|
258 |
|
wenzelm@39788
|
259 |
private def message_actor(name: String): Actor =
|
wenzelm@38895
|
260 |
Simple_Thread.actor(name) {
|
wenzelm@39788
|
261 |
val stream = system.fifo_input_stream(out_fifo) // FIXME potentially blocking forever
|
wenzelm@34106
|
262 |
val default_buffer = new Array[Byte](65536)
|
wenzelm@34106
|
263 |
var c = -1
|
wenzelm@28045
|
264 |
|
wenzelm@38867
|
265 |
def read_chunk(): XML.Body =
|
wenzelm@34106
|
266 |
{
|
wenzelm@34106
|
267 |
//{{{
|
wenzelm@34106
|
268 |
// chunk size
|
wenzelm@34106
|
269 |
var n = 0
|
wenzelm@34106
|
270 |
c = stream.read
|
wenzelm@34106
|
271 |
while (48 <= c && c <= 57) {
|
wenzelm@34106
|
272 |
n = 10 * n + (c - 48)
|
wenzelm@34106
|
273 |
c = stream.read
|
wenzelm@34106
|
274 |
}
|
wenzelm@34106
|
275 |
if (c != 10) throw new Protocol_Error("bad message chunk header")
|
wenzelm@34106
|
276 |
|
wenzelm@34106
|
277 |
// chunk content
|
wenzelm@34106
|
278 |
val buf =
|
wenzelm@34106
|
279 |
if (n <= default_buffer.size) default_buffer
|
wenzelm@34106
|
280 |
else new Array[Byte](n)
|
wenzelm@34106
|
281 |
|
wenzelm@34106
|
282 |
var i = 0
|
wenzelm@34106
|
283 |
var m = 0
|
wenzelm@34106
|
284 |
do {
|
wenzelm@34106
|
285 |
m = stream.read(buf, i, n - i)
|
wenzelm@34106
|
286 |
i += m
|
wenzelm@34106
|
287 |
} while (m > 0 && n > i)
|
wenzelm@34106
|
288 |
|
wenzelm@34106
|
289 |
if (i != n) throw new Protocol_Error("bad message chunk content")
|
wenzelm@34106
|
290 |
|
wenzelm@34106
|
291 |
YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
|
wenzelm@34106
|
292 |
//}}}
|
wenzelm@34106
|
293 |
}
|
wenzelm@34106
|
294 |
|
wenzelm@34106
|
295 |
do {
|
wenzelm@28045
|
296 |
try {
|
wenzelm@38691
|
297 |
val header = read_chunk()
|
wenzelm@38691
|
298 |
val body = read_chunk()
|
wenzelm@38691
|
299 |
header match {
|
wenzelm@38691
|
300 |
case List(XML.Elem(Markup(name, props), Nil))
|
wenzelm@38691
|
301 |
if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
|
wenzelm@38691
|
302 |
put_result(Kind.markup(name(0)), props, body)
|
wenzelm@38691
|
303 |
case _ => throw new Protocol_Error("bad header: " + header.toString)
|
wenzelm@34106
|
304 |
}
|
wenzelm@28045
|
305 |
}
|
wenzelm@28063
|
306 |
catch {
|
wenzelm@34106
|
307 |
case e: IOException =>
|
wenzelm@37705
|
308 |
put_result(Markup.SYSTEM, "Cannot read message:\n" + e.getMessage)
|
wenzelm@34106
|
309 |
case e: Protocol_Error =>
|
wenzelm@37705
|
310 |
put_result(Markup.SYSTEM, "Malformed message:\n" + e.getMessage)
|
wenzelm@28063
|
311 |
}
|
wenzelm@34106
|
312 |
} while (c != -1)
|
wenzelm@34106
|
313 |
stream.close
|
wenzelm@38568
|
314 |
close()
|
wenzelm@34106
|
315 |
|
wenzelm@38557
|
316 |
put_result(Markup.SYSTEM, name + " terminated")
|
wenzelm@38557
|
317 |
}
|
wenzelm@38557
|
318 |
|
wenzelm@38557
|
319 |
|
wenzelm@38557
|
320 |
|
wenzelm@38557
|
321 |
/** init **/
|
wenzelm@38557
|
322 |
|
wenzelm@38557
|
323 |
/* exec process */
|
wenzelm@38557
|
324 |
|
wenzelm@38557
|
325 |
try {
|
wenzelm@38557
|
326 |
val cmdline =
|
wenzelm@38557
|
327 |
List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
|
wenzelm@38568
|
328 |
proc = Some(system.execute(true, cmdline: _*))
|
wenzelm@38557
|
329 |
}
|
wenzelm@38557
|
330 |
catch {
|
wenzelm@38557
|
331 |
case e: IOException =>
|
wenzelm@38557
|
332 |
rm_fifos()
|
wenzelm@38557
|
333 |
error("Failed to execute Isabelle process: " + e.getMessage)
|
wenzelm@38557
|
334 |
}
|
wenzelm@38557
|
335 |
|
wenzelm@38557
|
336 |
|
wenzelm@38568
|
337 |
/* I/O actors */
|
wenzelm@38568
|
338 |
|
wenzelm@39788
|
339 |
private val command_input = input_actor("command_input")
|
wenzelm@39788
|
340 |
message_actor("message_output")
|
wenzelm@39788
|
341 |
|
wenzelm@38568
|
342 |
private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
|
wenzelm@38568
|
343 |
stdout_actor("standard_output", proc.get.getInputStream)
|
wenzelm@38568
|
344 |
|
wenzelm@38568
|
345 |
|
wenzelm@38557
|
346 |
/* exit process */
|
wenzelm@38557
|
347 |
|
wenzelm@38895
|
348 |
Simple_Thread.actor("process_exit") {
|
wenzelm@38568
|
349 |
proc match {
|
wenzelm@38568
|
350 |
case None =>
|
wenzelm@38568
|
351 |
case Some(p) =>
|
wenzelm@38568
|
352 |
val rc = p.waitFor()
|
wenzelm@38568
|
353 |
Thread.sleep(300) // FIXME property!?
|
wenzelm@38568
|
354 |
put_result(Markup.SYSTEM, "process_exit terminated")
|
wenzelm@38568
|
355 |
put_result(Markup.EXIT, rc.toString)
|
wenzelm@38568
|
356 |
}
|
wenzelm@38557
|
357 |
rm_fifos()
|
wenzelm@38557
|
358 |
}
|
wenzelm@38557
|
359 |
|
wenzelm@38557
|
360 |
|
wenzelm@38557
|
361 |
|
wenzelm@38557
|
362 |
/** main methods **/
|
wenzelm@38557
|
363 |
|
wenzelm@38568
|
364 |
def input_raw(text: String): Unit = standard_input ! Input_Text(text)
|
wenzelm@38557
|
365 |
|
wenzelm@38654
|
366 |
def input_bytes(name: String, args: Array[Byte]*): Unit =
|
wenzelm@38654
|
367 |
command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
|
wenzelm@38654
|
368 |
|
wenzelm@38568
|
369 |
def input(name: String, args: String*): Unit =
|
wenzelm@38654
|
370 |
input_bytes(name, args.map(Standard_System.string_bytes): _*)
|
wenzelm@38557
|
371 |
|
wenzelm@38568
|
372 |
def close(): Unit = command_input ! Close
|
wenzelm@27949
|
373 |
}
|