author | wenzelm |
Mon, 03 Oct 2016 12:28:36 +0200 | |
changeset 64004 | b4ece7a3f2ca |
parent 63584 | 68751fe1c036 |
child 65218 | 102b8e092860 |
permissions | -rw-r--r-- |
56385 | 1 |
/* Title: Pure/PIDE/prover.scala |
2 |
Author: Makarius |
|
57923 | 3 |
Options: :folding=explicit: |
56385 | 4 |
|
57923 | 5 |
Prover process wrapping. |
56385 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
57916 | 11 |
import java.io.{InputStream, OutputStream, BufferedReader, BufferedOutputStream, IOException} |
57915
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
12 |
|
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
13 |
|
56385 | 14 |
object Prover |
15 |
{ |
|
57915
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
16 |
/* underlying system process */ |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
17 |
|
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
18 |
trait System_Process |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
19 |
{ |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
20 |
def stdout: BufferedReader |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
21 |
def stderr: BufferedReader |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
22 |
def terminate: Unit |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
23 |
def join: Int |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
24 |
} |
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
25 |
|
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
57906
diff
changeset
|
26 |
|
56385 | 27 |
/* messages */ |
28 |
||
29 |
sealed abstract class Message |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62310
diff
changeset
|
30 |
type Receiver = Message => Unit |
56385 | 31 |
|
56386 | 32 |
class Input(val name: String, val args: List[String]) extends Message |
56385 | 33 |
{ |
34 |
override def toString: String = |
|
35 |
XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))), |
|
36 |
args.map(s => |
|
37 |
List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString |
|
38 |
} |
|
39 |
||
40 |
class Output(val message: XML.Elem) extends Message |
|
41 |
{ |
|
42 |
def kind: String = message.markup.name |
|
43 |
def properties: Properties.T = message.markup.properties |
|
44 |
def body: XML.Body = message.body |
|
45 |
||
46 |
def is_init = kind == Markup.INIT |
|
47 |
def is_exit = kind == Markup.EXIT |
|
48 |
def is_stdout = kind == Markup.STDOUT |
|
49 |
def is_stderr = kind == Markup.STDERR |
|
50 |
def is_system = kind == Markup.SYSTEM |
|
51 |
def is_status = kind == Markup.STATUS |
|
52 |
def is_report = kind == Markup.REPORT |
|
53 |
def is_syslog = is_init || is_exit || is_system || is_stderr |
|
54 |
||
55 |
override def toString: String = |
|
56 |
{ |
|
57 |
val res = |
|
58 |
if (is_status || is_report) message.body.map(_.toString).mkString |
|
59 |
else Pretty.string_of(message.body) |
|
60 |
if (properties.isEmpty) |
|
61 |
kind.toString + " [[" + res + "]]" |
|
62 |
else |
|
63 |
kind.toString + " " + |
|
64 |
(for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" |
|
65 |
} |
|
66 |
} |
|
67 |
||
68 |
class Protocol_Output(props: Properties.T, val bytes: Bytes) |
|
69 |
extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) |
|
70 |
{ |
|
71 |
lazy val text: String = bytes.toString |
|
72 |
} |
|
73 |
} |
|
74 |
||
56393
22f533e6a049
more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents:
56387
diff
changeset
|
75 |
|
57916 | 76 |
abstract class Prover( |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62310
diff
changeset
|
77 |
receiver: Prover.Receiver, |
57917 | 78 |
system_channel: System_Channel, |
57916 | 79 |
system_process: Prover.System_Process) extends Protocol |
56387 | 80 |
{ |
57923 | 81 |
/** receiver output **/ |
57916 | 82 |
|
83 |
val xml_cache: XML.Cache = new XML.Cache() |
|
84 |
||
85 |
private def system_output(text: String) |
|
86 |
{ |
|
87 |
receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) |
|
88 |
} |
|
89 |
||
90 |
private def protocol_output(props: Properties.T, bytes: Bytes) |
|
91 |
{ |
|
92 |
receiver(new Prover.Protocol_Output(props, bytes)) |
|
93 |
} |
|
94 |
||
95 |
private def output(kind: String, props: Properties.T, body: XML.Body) |
|
96 |
{ |
|
57917 | 97 |
if (kind == Markup.INIT) system_channel.accepted() |
56387 | 98 |
|
59713 | 99 |
val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body)) |
100 |
val reports = Protocol_Message.reports(props, body) |
|
57916 | 101 |
for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg))) |
102 |
} |
|
103 |
||
104 |
private def exit_message(rc: Int) |
|
105 |
{ |
|
106 |
output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString))) |
|
107 |
} |
|
108 |
||
109 |
||
56387 | 110 |
|
57916 | 111 |
/** process manager **/ |
112 |
||
62307 | 113 |
private val process_result: Future[Int] = |
61559
313eca3fa847
more direct task future implementation, with proper cancel operation;
wenzelm
parents:
61556
diff
changeset
|
114 |
Future.thread("process_result") { system_process.join } |
57916 | 115 |
|
116 |
private def terminate_process() |
|
56387 | 117 |
{ |
57916 | 118 |
try { system_process.terminate } |
119 |
catch { |
|
120 |
case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage) |
|
121 |
} |
|
56387 | 122 |
} |
123 |
||
61556 | 124 |
private val process_manager = Standard_Thread.fork("process_manager") |
57916 | 125 |
{ |
126 |
val (startup_failed, startup_errors) = |
|
127 |
{ |
|
128 |
var finished: Option[Boolean] = None |
|
129 |
val result = new StringBuilder(100) |
|
130 |
while (finished.isEmpty && (system_process.stderr.ready || !process_result.is_finished)) { |
|
131 |
while (finished.isEmpty && system_process.stderr.ready) { |
|
132 |
try { |
|
133 |
val c = system_process.stderr.read |
|
134 |
if (c == 2) finished = Some(true) |
|
135 |
else result += c.toChar |
|
136 |
} |
|
137 |
catch { case _: IOException => finished = Some(false) } |
|
138 |
} |
|
139 |
Thread.sleep(10) |
|
140 |
} |
|
141 |
(finished.isEmpty || !finished.get, result.toString.trim) |
|
142 |
} |
|
143 |
if (startup_errors != "") system_output(startup_errors) |
|
144 |
||
145 |
if (startup_failed) { |
|
146 |
terminate_process() |
|
147 |
process_result.join |
|
148 |
exit_message(127) |
|
149 |
} |
|
150 |
else { |
|
57917 | 151 |
val (command_stream, message_stream) = system_channel.rendezvous() |
57916 | 152 |
|
153 |
command_input_init(command_stream) |
|
154 |
val stdout = physical_output(false) |
|
155 |
val stderr = physical_output(true) |
|
156 |
val message = message_output(message_stream) |
|
157 |
||
158 |
val rc = process_result.join |
|
159 |
system_output("process terminated") |
|
160 |
command_input_close() |
|
161 |
for (thread <- List(stdout, stderr, message)) thread.join |
|
162 |
system_output("process_manager terminated") |
|
163 |
exit_message(rc) |
|
164 |
} |
|
57917 | 165 |
system_channel.accepted() |
57916 | 166 |
} |
167 |
||
168 |
||
169 |
/* management methods */ |
|
170 |
||
171 |
def join() { process_manager.join() } |
|
172 |
||
173 |
def terminate() |
|
174 |
{ |
|
62310
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
175 |
system_output("Terminating prover process") |
57916 | 176 |
command_input_close() |
62310
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
177 |
|
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
178 |
var count = 10 |
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
179 |
while (!process_result.is_finished && count > 0) { |
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
180 |
Thread.sleep(100) |
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
181 |
count -= 1 |
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
182 |
} |
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
183 |
if (!process_result.is_finished) terminate_process() |
57916 | 184 |
} |
185 |
||
186 |
||
187 |
||
188 |
/** process streams **/ |
|
189 |
||
190 |
/* command input */ |
|
191 |
||
192 |
private var command_input: Option[Consumer_Thread[List[Bytes]]] = None |
|
193 |
||
194 |
private def command_input_close(): Unit = command_input.foreach(_.shutdown) |
|
195 |
||
196 |
private def command_input_init(raw_stream: OutputStream) |
|
197 |
{ |
|
198 |
val name = "command_input" |
|
199 |
val stream = new BufferedOutputStream(raw_stream) |
|
200 |
command_input = |
|
201 |
Some( |
|
202 |
Consumer_Thread.fork(name)( |
|
203 |
consume = |
|
204 |
{ |
|
205 |
case chunks => |
|
206 |
try { |
|
64004 | 207 |
Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream) |
208 |
chunks.foreach(_.write_stream(stream)) |
|
57916 | 209 |
stream.flush |
210 |
true |
|
211 |
} |
|
212 |
catch { case e: IOException => system_output(name + ": " + e.getMessage); false } |
|
213 |
}, |
|
214 |
finish = { case () => stream.close; system_output(name + " terminated") } |
|
215 |
) |
|
216 |
) |
|
217 |
} |
|
56387 | 218 |
|
219 |
||
57916 | 220 |
/* physical output */ |
221 |
||
222 |
private def physical_output(err: Boolean): Thread = |
|
223 |
{ |
|
224 |
val (name, reader, markup) = |
|
225 |
if (err) ("standard_error", system_process.stderr, Markup.STDERR) |
|
226 |
else ("standard_output", system_process.stdout, Markup.STDOUT) |
|
56387 | 227 |
|
61556 | 228 |
Standard_Thread.fork(name) { |
57916 | 229 |
try { |
230 |
var result = new StringBuilder(100) |
|
231 |
var finished = false |
|
232 |
while (!finished) { |
|
233 |
//{{{ |
|
234 |
var c = -1 |
|
235 |
var done = false |
|
236 |
while (!done && (result.length == 0 || reader.ready)) { |
|
237 |
c = reader.read |
|
238 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
|
239 |
else done = true |
|
240 |
} |
|
241 |
if (result.length > 0) { |
|
242 |
output(markup, Nil, List(XML.Text(decode(result.toString)))) |
|
243 |
result.length = 0 |
|
244 |
} |
|
245 |
else { |
|
246 |
reader.close |
|
247 |
finished = true |
|
248 |
} |
|
249 |
//}}} |
|
250 |
} |
|
251 |
} |
|
252 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
|
253 |
system_output(name + " terminated") |
|
254 |
} |
|
255 |
} |
|
56387 | 256 |
|
257 |
||
57916 | 258 |
/* message output */ |
259 |
||
260 |
private def message_output(stream: InputStream): Thread = |
|
261 |
{ |
|
262 |
class EOF extends Exception |
|
263 |
class Protocol_Error(msg: String) extends Exception(msg) |
|
264 |
||
265 |
val name = "message_output" |
|
61556 | 266 |
Standard_Thread.fork(name) { |
57916 | 267 |
val default_buffer = new Array[Byte](65536) |
268 |
var c = -1 |
|
56387 | 269 |
|
57916 | 270 |
def read_int(): Int = |
271 |
//{{{ |
|
272 |
{ |
|
273 |
var n = 0 |
|
274 |
c = stream.read |
|
275 |
if (c == -1) throw new EOF |
|
276 |
while (48 <= c && c <= 57) { |
|
277 |
n = 10 * n + (c - 48) |
|
278 |
c = stream.read |
|
279 |
} |
|
280 |
if (c != 10) |
|
281 |
throw new Protocol_Error("malformed header: expected integer followed by newline") |
|
282 |
else n |
|
283 |
} |
|
284 |
//}}} |
|
56387 | 285 |
|
57916 | 286 |
def read_chunk_bytes(): (Array[Byte], Int) = |
287 |
//{{{ |
|
288 |
{ |
|
289 |
val n = read_int() |
|
290 |
val buf = |
|
60215 | 291 |
if (n <= default_buffer.length) default_buffer |
57916 | 292 |
else new Array[Byte](n) |
293 |
||
294 |
var i = 0 |
|
295 |
var m = 0 |
|
296 |
do { |
|
297 |
m = stream.read(buf, i, n - i) |
|
298 |
if (m != -1) i += m |
|
299 |
} |
|
300 |
while (m != -1 && n > i) |
|
301 |
||
302 |
if (i != n) |
|
303 |
throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") |
|
304 |
||
305 |
(buf, n) |
|
306 |
} |
|
307 |
//}}} |
|
56387 | 308 |
|
57916 | 309 |
def read_chunk(): XML.Body = |
310 |
{ |
|
311 |
val (buf, n) = read_chunk_bytes() |
|
312 |
YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) |
|
313 |
} |
|
56387 | 314 |
|
57916 | 315 |
try { |
316 |
do { |
|
317 |
try { |
|
318 |
val header = read_chunk() |
|
319 |
header match { |
|
320 |
case List(XML.Elem(Markup(name, props), Nil)) => |
|
321 |
val kind = name.intern |
|
322 |
if (kind == Markup.PROTOCOL) { |
|
323 |
val (buf, n) = read_chunk_bytes() |
|
324 |
protocol_output(props, Bytes(buf, 0, n)) |
|
325 |
} |
|
326 |
else { |
|
327 |
val body = read_chunk() |
|
328 |
output(kind, props, body) |
|
329 |
} |
|
330 |
case _ => |
|
331 |
read_chunk() |
|
332 |
throw new Protocol_Error("bad header: " + header.toString) |
|
333 |
} |
|
334 |
} |
|
335 |
catch { case _: EOF => } |
|
336 |
} |
|
337 |
while (c != -1) |
|
338 |
} |
|
339 |
catch { |
|
340 |
case e: IOException => system_output("Cannot read message:\n" + e.getMessage) |
|
341 |
case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage) |
|
342 |
} |
|
343 |
stream.close |
|
56387 | 344 |
|
57916 | 345 |
system_output(name + " terminated") |
346 |
} |
|
347 |
} |
|
348 |
||
349 |
||
350 |
||
351 |
/** protocol commands **/ |
|
352 |
||
353 |
def protocol_command_bytes(name: String, args: Bytes*): Unit = |
|
354 |
command_input match { |
|
355 |
case Some(thread) => thread.send(Bytes(name) :: args.toList) |
|
356 |
case None => error("Uninitialized command input thread") |
|
357 |
} |
|
358 |
||
359 |
def protocol_command(name: String, args: String*) |
|
360 |
{ |
|
361 |
receiver(new Prover.Input(name, args.toList)) |
|
362 |
protocol_command_bytes(name, args.map(Bytes(_)): _*) |
|
363 |
} |
|
56387 | 364 |
} |