author | wenzelm |
Sun, 06 Mar 2022 17:45:47 +0100 | |
changeset 75230 | bbbee54b1198 |
parent 74253 | 45dc9de1bd33 |
child 75393 | 87ebf5a50283 |
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 |
||
67835 | 11 |
import java.io.{InputStream, OutputStream, 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 |
{ |
|
16 |
/* messages */ |
|
17 |
||
18 |
sealed abstract class Message |
|
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62310
diff
changeset
|
19 |
type Receiver = Message => Unit |
56385 | 20 |
|
56386 | 21 |
class Input(val name: String, val args: List[String]) extends Message |
56385 | 22 |
{ |
23 |
override def toString: String = |
|
24 |
XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))), |
|
71383 | 25 |
args.flatMap(s => |
26 |
List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString |
|
56385 | 27 |
} |
28 |
||
29 |
class Output(val message: XML.Elem) extends Message |
|
30 |
{ |
|
31 |
def kind: String = message.markup.name |
|
32 |
def properties: Properties.T = message.markup.properties |
|
33 |
def body: XML.Body = message.body |
|
34 |
||
71601 | 35 |
def is_init: Boolean = kind == Markup.INIT |
36 |
def is_exit: Boolean = kind == Markup.EXIT |
|
37 |
def is_stdout: Boolean = kind == Markup.STDOUT |
|
38 |
def is_stderr: Boolean = kind == Markup.STDERR |
|
39 |
def is_system: Boolean = kind == Markup.SYSTEM |
|
40 |
def is_status: Boolean = kind == Markup.STATUS |
|
41 |
def is_report: Boolean = kind == Markup.REPORT |
|
42 |
def is_syslog: Boolean = is_init || is_exit || is_system || is_stderr |
|
56385 | 43 |
|
44 |
override def toString: String = |
|
45 |
{ |
|
46 |
val res = |
|
47 |
if (is_status || is_report) message.body.map(_.toString).mkString |
|
71649 | 48 |
else Pretty.string_of(message.body, metric = Symbol.Metric) |
56385 | 49 |
if (properties.isEmpty) |
73559 | 50 |
kind + " [[" + res + "]]" |
56385 | 51 |
else |
73559 | 52 |
kind + " " + |
73712 | 53 |
(properties.map(Properties.Eq.apply)).mkString("{", ",", "}") + " [[" + res + "]]" |
56385 | 54 |
} |
55 |
} |
|
56 |
||
73560 | 57 |
class Malformed(msg: String) extends Exn.User_Error("Malformed prover message: " + msg) |
58 |
def bad_header(print: String): Nothing = throw new Malformed("bad message header\n" + print) |
|
59 |
def bad_chunks(): Nothing = throw new Malformed("bad message chunks") |
|
73559 | 60 |
|
61 |
def the_chunk(chunks: List[Bytes], print: => String): Bytes = |
|
62 |
chunks match { |
|
63 |
case List(chunk) => chunk |
|
73560 | 64 |
case _ => throw new Malformed("single chunk expected: " + print) |
73559 | 65 |
} |
66 |
||
67 |
class Protocol_Output(props: Properties.T, val chunks: List[Bytes]) |
|
56385 | 68 |
extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) |
69 |
{ |
|
73559 | 70 |
def chunk: Bytes = the_chunk(chunks, toString) |
71 |
lazy val text: String = chunk.text |
|
56385 | 72 |
} |
73 |
} |
|
74 |
||
56393
22f533e6a049
more abstract Prover.Syntax, as proposed by Carst Tankink;
wenzelm
parents:
56387
diff
changeset
|
75 |
|
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65317
diff
changeset
|
76 |
class Prover( |
62556
c115e69f457f
more abstract Session.start, without prover command-line;
wenzelm
parents:
62310
diff
changeset
|
77 |
receiver: Prover.Receiver, |
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
71969
diff
changeset
|
78 |
cache: XML.Cache, |
65316 | 79 |
channel: System_Channel, |
80 |
process: Bash.Process) extends Protocol |
|
56387 | 81 |
{ |
57923 | 82 |
/** receiver output **/ |
57916 | 83 |
|
73340 | 84 |
private def system_output(text: String): Unit = |
57916 | 85 |
{ |
86 |
receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) |
|
87 |
} |
|
88 |
||
73559 | 89 |
private def protocol_output(props: Properties.T, chunks: List[Bytes]): Unit = |
57916 | 90 |
{ |
73562 | 91 |
receiver(new Prover.Protocol_Output(props, chunks)) |
57916 | 92 |
} |
93 |
||
73340 | 94 |
private def output(kind: String, props: Properties.T, body: XML.Body): Unit = |
57916 | 95 |
{ |
59713 | 96 |
val main = XML.Elem(Markup(kind, props), Protocol_Message.clean_reports(body)) |
97 |
val reports = Protocol_Message.reports(props, body) |
|
73031
f93f0597f4fb
clarified signature: absorb XZ.Cache into XML.Cache;
wenzelm
parents:
71969
diff
changeset
|
98 |
for (msg <- main :: reports) receiver(new Prover.Output(cache.elem(msg))) |
57916 | 99 |
} |
100 |
||
73340 | 101 |
private def exit_message(result: Process_Result): Unit = |
57916 | 102 |
{ |
65317 | 103 |
output(Markup.EXIT, Markup.Process_Result(result), |
71747 | 104 |
List(XML.Text(result.print_return_code))) |
57916 | 105 |
} |
106 |
||
107 |
||
56387 | 108 |
|
57916 | 109 |
/** process manager **/ |
110 |
||
65317 | 111 |
private val process_result: Future[Process_Result] = |
112 |
Future.thread("process_result") { |
|
74141 | 113 |
val rc = process.join() |
65317 | 114 |
val timing = process.get_timing |
115 |
Process_Result(rc, timing = timing) |
|
116 |
} |
|
57916 | 117 |
|
73340 | 118 |
private def terminate_process(): Unit = |
56387 | 119 |
{ |
73367 | 120 |
try { process.terminate() } |
57916 | 121 |
catch { |
122 |
case exn @ ERROR(_) => system_output("Failed to terminate prover process: " + exn.getMessage) |
|
123 |
} |
|
56387 | 124 |
} |
125 |
||
71692 | 126 |
private val process_manager = Isabelle_Thread.fork(name = "process_manager") |
57916 | 127 |
{ |
71641
c1409b9c2b22
proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
wenzelm
parents:
71601
diff
changeset
|
128 |
val stdout = physical_output(false) |
c1409b9c2b22
proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
wenzelm
parents:
71601
diff
changeset
|
129 |
|
57916 | 130 |
val (startup_failed, startup_errors) = |
131 |
{ |
|
132 |
var finished: Option[Boolean] = None |
|
133 |
val result = new StringBuilder(100) |
|
65316 | 134 |
while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) { |
135 |
while (finished.isEmpty && process.stderr.ready) { |
|
57916 | 136 |
try { |
65316 | 137 |
val c = process.stderr.read |
57916 | 138 |
if (c == 2) finished = Some(true) |
139 |
else result += c.toChar |
|
140 |
} |
|
141 |
catch { case _: IOException => finished = Some(false) } |
|
142 |
} |
|
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73562
diff
changeset
|
143 |
Time.seconds(0.05).sleep() |
57916 | 144 |
} |
145 |
(finished.isEmpty || !finished.get, result.toString.trim) |
|
146 |
} |
|
147 |
if (startup_errors != "") system_output(startup_errors) |
|
148 |
||
149 |
if (startup_failed) { |
|
150 |
terminate_process() |
|
151 |
process_result.join |
|
71641
c1409b9c2b22
proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
wenzelm
parents:
71601
diff
changeset
|
152 |
stdout.join |
65317 | 153 |
exit_message(Process_Result(127)) |
57916 | 154 |
} |
155 |
else { |
|
65316 | 156 |
val (command_stream, message_stream) = channel.rendezvous() |
57916 | 157 |
|
158 |
command_input_init(command_stream) |
|
159 |
val stderr = physical_output(true) |
|
160 |
val message = message_output(message_stream) |
|
161 |
||
65317 | 162 |
val result = process_result.join |
57916 | 163 |
system_output("process terminated") |
164 |
command_input_close() |
|
74140 | 165 |
for (thread <- List(stdout, stderr, message)) thread.join() |
57916 | 166 |
system_output("process_manager terminated") |
65317 | 167 |
exit_message(result) |
57916 | 168 |
} |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
68805
diff
changeset
|
169 |
channel.shutdown() |
57916 | 170 |
} |
171 |
||
172 |
||
173 |
/* management methods */ |
|
174 |
||
73340 | 175 |
def join(): Unit = process_manager.join() |
57916 | 176 |
|
73340 | 177 |
def terminate(): Unit = |
57916 | 178 |
{ |
62310
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
179 |
system_output("Terminating prover process") |
57916 | 180 |
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
|
181 |
|
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
182 |
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
|
183 |
while (!process_result.is_finished && count > 0) { |
73702
7202e12cb324
tuned signature --- following hints by IntelliJ IDEA;
wenzelm
parents:
73562
diff
changeset
|
184 |
Time.seconds(0.1).sleep() |
62310
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
185 |
count -= 1 |
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
186 |
} |
ab836dc7410e
more gentle termination (like Bash.multi_kill without signal) to give prover a chance to conclude;
wenzelm
parents:
62307
diff
changeset
|
187 |
if (!process_result.is_finished) terminate_process() |
57916 | 188 |
} |
189 |
||
190 |
||
191 |
||
192 |
/** process streams **/ |
|
193 |
||
194 |
/* command input */ |
|
195 |
||
196 |
private var command_input: Option[Consumer_Thread[List[Bytes]]] = None |
|
197 |
||
73367 | 198 |
private def command_input_close(): Unit = command_input.foreach(_.shutdown()) |
57916 | 199 |
|
73340 | 200 |
private def command_input_init(raw_stream: OutputStream): Unit = |
57916 | 201 |
{ |
202 |
val name = "command_input" |
|
203 |
val stream = new BufferedOutputStream(raw_stream) |
|
204 |
command_input = |
|
205 |
Some( |
|
206 |
Consumer_Thread.fork(name)( |
|
207 |
consume = |
|
208 |
{ |
|
209 |
case chunks => |
|
210 |
try { |
|
64004 | 211 |
Bytes(chunks.map(_.length).mkString("", ",", "\n")).write_stream(stream) |
212 |
chunks.foreach(_.write_stream(stream)) |
|
57916 | 213 |
stream.flush |
214 |
true |
|
215 |
} |
|
216 |
catch { case e: IOException => system_output(name + ": " + e.getMessage); false } |
|
217 |
}, |
|
73367 | 218 |
finish = { case () => stream.close(); system_output(name + " terminated") } |
57916 | 219 |
) |
220 |
) |
|
221 |
} |
|
56387 | 222 |
|
223 |
||
57916 | 224 |
/* physical output */ |
225 |
||
226 |
private def physical_output(err: Boolean): Thread = |
|
227 |
{ |
|
228 |
val (name, reader, markup) = |
|
65316 | 229 |
if (err) ("standard_error", process.stderr, Markup.STDERR) |
230 |
else ("standard_output", process.stdout, Markup.STDOUT) |
|
56387 | 231 |
|
71692 | 232 |
Isabelle_Thread.fork(name = name) { |
57916 | 233 |
try { |
234 |
var result = new StringBuilder(100) |
|
235 |
var finished = false |
|
236 |
while (!finished) { |
|
237 |
//{{{ |
|
238 |
var c = -1 |
|
239 |
var done = false |
|
71383 | 240 |
while (!done && (result.isEmpty || reader.ready)) { |
57916 | 241 |
c = reader.read |
242 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
|
243 |
else done = true |
|
244 |
} |
|
71383 | 245 |
if (result.nonEmpty) { |
65345
2fdd4431b30e
clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents:
65317
diff
changeset
|
246 |
output(markup, Nil, List(XML.Text(Symbol.decode(result.toString)))) |
73367 | 247 |
result.clear() |
57916 | 248 |
} |
249 |
else { |
|
73367 | 250 |
reader.close() |
57916 | 251 |
finished = true |
252 |
} |
|
253 |
//}}} |
|
254 |
} |
|
255 |
} |
|
256 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
|
257 |
system_output(name + " terminated") |
|
258 |
} |
|
259 |
} |
|
56387 | 260 |
|
261 |
||
57916 | 262 |
/* message output */ |
263 |
||
264 |
private def message_output(stream: InputStream): Thread = |
|
265 |
{ |
|
73561
c83152933579
clarified signature: Bytes extends CharSequence already (see d201996f72a8);
wenzelm
parents:
73560
diff
changeset
|
266 |
def decode_chunk(chunk: Bytes): XML.Body = |
73562 | 267 |
Symbol.decode_yxml_failsafe(chunk.text, cache = cache) |
56387 | 268 |
|
73559 | 269 |
val thread_name = "message_output" |
270 |
Isabelle_Thread.fork(name = thread_name) { |
|
271 |
try { |
|
272 |
var finished = false |
|
273 |
while (!finished) { |
|
274 |
Byte_Message.read_message(stream) match { |
|
275 |
case None => finished = true |
|
276 |
case Some(header :: chunks) => |
|
277 |
decode_chunk(header) match { |
|
73562 | 278 |
case List(XML.Elem(Markup(kind, props), Nil)) => |
73559 | 279 |
if (kind == Markup.PROTOCOL) protocol_output(props, chunks) |
73562 | 280 |
else output(kind, props, decode_chunk(Prover.the_chunk(chunks, kind))) |
73559 | 281 |
case _ => Prover.bad_header(header.toString) |
282 |
} |
|
283 |
case Some(_) => Prover.bad_chunks() |
|
284 |
} |
|
57916 | 285 |
} |
286 |
} |
|
287 |
catch { |
|
288 |
case e: IOException => system_output("Cannot read message:\n" + e.getMessage) |
|
73560 | 289 |
case e: Prover.Malformed => system_output(e.getMessage) |
57916 | 290 |
} |
73367 | 291 |
stream.close() |
56387 | 292 |
|
73559 | 293 |
system_output(thread_name + " terminated") |
57916 | 294 |
} |
295 |
} |
|
296 |
||
297 |
||
298 |
||
299 |
/** protocol commands **/ |
|
300 |
||
70666 | 301 |
var trace: Boolean = false |
302 |
||
70661 | 303 |
def protocol_command_raw(name: String, args: List[Bytes]): Unit = |
57916 | 304 |
command_input match { |
74253 | 305 |
case Some(thread) if thread.is_active() => |
70666 | 306 |
if (trace) { |
73359 | 307 |
val payload = args.foldLeft(0) { case (n, b) => n + b.length } |
70666 | 308 |
Output.writeln( |
309 |
"protocol_command " + name + ", args = " + args.length + ", payload = " + payload) |
|
310 |
} |
|
311 |
thread.send(Bytes(name) :: args) |
|
68805 | 312 |
case _ => error("Inactive prover input thread for command " + quote(name)) |
57916 | 313 |
} |
314 |
||
73340 | 315 |
def protocol_command_args(name: String, args: List[String]): Unit = |
57916 | 316 |
{ |
70661 | 317 |
receiver(new Prover.Input(name, args)) |
318 |
protocol_command_raw(name, args.map(Bytes(_))) |
|
57916 | 319 |
} |
70661 | 320 |
|
321 |
def protocol_command(name: String, args: String*): Unit = |
|
322 |
protocol_command_args(name, args.toList) |
|
56387 | 323 |
} |