author | wenzelm |
Thu, 03 Apr 2014 14:54:17 +0200 | |
changeset 56387 | d92eb5c3960d |
parent 56385 | 76acce58aeab |
child 56390 | 8185044353fd |
permissions | -rw-r--r-- |
43283 | 1 |
/* Title: Pure/System/isabelle_process.scala |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
27963 | 3 |
Options: :folding=explicit:collapseFolds=1: |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
4 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
5 |
Isabelle process management -- always reactive due to multi-threaded I/O. |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
6 |
*/ |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
7 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
8 |
package isabelle |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
9 |
|
55618 | 10 |
|
27955
4c32c5e75eca
use java.util.concurrent.LinkedBlockingQueue, which blocks as required;
wenzelm
parents:
27949
diff
changeset
|
11 |
import java.util.concurrent.LinkedBlockingQueue |
28045 | 12 |
import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
13 |
InputStream, OutputStream, BufferedOutputStream, IOException} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
14 |
|
32474
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
15 |
import scala.actors.Actor |
0818e6b1c8a6
Isabelle_Process: receiver as Actor, not EventBus;
wenzelm
parents:
32448
diff
changeset
|
16 |
import Actor._ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
17 |
|
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
18 |
|
45055
55274f7e306b
explicit option for socket vs. fifo communication;
wenzelm
parents:
45027
diff
changeset
|
19 |
class Isabelle_Process( |
56387 | 20 |
receiver: Prover.Message => Unit = Console.println(_), |
21 |
prover_args: List[String] = Nil) |
|
29192 | 22 |
{ |
56387 | 23 |
/* text and tree data */ |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
24 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
25 |
def encode(s: String): String = Symbol.encode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
26 |
def decode(s: String): String = Symbol.decode(s) |
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
27 |
|
56387 | 28 |
val xml_cache = new XML.Cache() |
48705
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
29 |
|
dd32321d6eef
tuned signature -- slightly more abstract text representation of prover process;
wenzelm
parents:
48355
diff
changeset
|
30 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
31 |
/* output */ |
39573 | 32 |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
33 |
private def system_output(text: String) |
39573 | 34 |
{ |
56385 | 35 |
receiver(new Prover.Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) |
39573 | 36 |
} |
37 |
||
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
38 |
private def protocol_output(props: Properties.T, bytes: Bytes) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
39 |
{ |
56385 | 40 |
receiver(new Prover.Protocol_Output(props, bytes)) |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
41 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
42 |
|
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
43 |
private def output(kind: String, props: Properties.T, body: XML.Body) |
39573 | 44 |
{ |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
45 |
if (kind == Markup.INIT) system_channel.accepted() |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
46 |
|
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
47 |
val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body)) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
48 |
val reports = Protocol.message_reports(props, body) |
56385 | 49 |
for (msg <- main :: reports) receiver(new Prover.Output(xml_cache.elem(msg))) |
39573 | 50 |
} |
51 |
||
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
52 |
private def exit_message(rc: Int) |
39573 | 53 |
{ |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
54 |
output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString))) |
39573 | 55 |
} |
56 |
||
57 |
||
52581 | 58 |
/* command input actor */ |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
59 |
|
54440 | 60 |
private case class Input_Chunks(chunks: List[Bytes]) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
61 |
|
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
62 |
private case object Close |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
63 |
private def close(p: (Thread, Actor)) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
64 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
65 |
if (p != null && p._1.isAlive) { |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
66 |
p._2 ! Close |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
67 |
p._1.join |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
68 |
} |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
69 |
} |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
70 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
71 |
@volatile private var command_input: (Thread, Actor) = null |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
72 |
|
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
73 |
|
56387 | 74 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
75 |
/** process manager **/ |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
76 |
|
45158 | 77 |
private val system_channel = System_Channel() |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
78 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
79 |
private val process = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
80 |
try { |
56387 | 81 |
val cmdline = |
82 |
Isabelle_System.getenv_strict("ISABELLE_PROCESS") :: |
|
83 |
(system_channel.isabelle_args ::: prover_args) |
|
48353
bcce872202b3
support external processes with explicit environment;
wenzelm
parents:
48020
diff
changeset
|
84 |
new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
85 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
86 |
catch { case e: IOException => system_channel.accepted(); throw(e) } |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
87 |
|
56387 | 88 |
private val (_, process_result) = |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
89 |
Simple_Thread.future("process_result") { process.join } |
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
90 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
91 |
private def terminate_process() |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
92 |
{ |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
93 |
try { process.terminate } |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
94 |
catch { case e: IOException => system_output("Failed to terminate Isabelle: " + e.getMessage) } |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
95 |
} |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
96 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
97 |
private val process_manager = Simple_Thread.fork("process_manager") |
39572 | 98 |
{ |
46548
c54a4a22501c
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
wenzelm
parents:
46121
diff
changeset
|
99 |
val (startup_failed, startup_errors) = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
100 |
{ |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
101 |
var finished: Option[Boolean] = None |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
102 |
val result = new StringBuilder(100) |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
103 |
while (finished.isEmpty && (process.stderr.ready || !process_result.is_finished)) { |
46548
c54a4a22501c
clarified initial process startup errors: recover image load failure message (cf. 2cb7e34f6096) and suppress accidental output from raw ML toplevel;
wenzelm
parents:
46121
diff
changeset
|
104 |
while (finished.isEmpty && process.stderr.ready) { |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
105 |
try { |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
106 |
val c = process.stderr.read |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
107 |
if (c == 2) finished = Some(true) |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
108 |
else result += c.toChar |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
109 |
} |
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
110 |
catch { case _: IOException => finished = Some(false) } |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
111 |
} |
48020
a4f9957878ab
clarified prover startup: no timeout, read stderr more carefully;
wenzelm
parents:
48019
diff
changeset
|
112 |
Thread.sleep(10) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
113 |
} |
39623 | 114 |
(finished.isEmpty || !finished.get, result.toString.trim) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
115 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
116 |
if (startup_errors != "") system_output(startup_errors) |
39572 | 117 |
|
52581 | 118 |
process.stdin.close |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
119 |
if (startup_failed) { |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
120 |
exit_message(127) |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
121 |
Thread.sleep(300) |
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
122 |
terminate_process() |
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
123 |
process_result.join |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
124 |
} |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
125 |
else { |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
126 |
val (command_stream, message_stream) = system_channel.rendezvous() |
39530
16adc476348f
Isabelle_Process: more robust rendezvous, even without proper blocking on open (Cygwin);
wenzelm
parents:
39528
diff
changeset
|
127 |
|
46773 | 128 |
val stdout = physical_output_actor(false) |
129 |
val stderr = physical_output_actor(true) |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
130 |
command_input = input_actor(command_stream) |
39572 | 131 |
val message = message_actor(message_stream) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
132 |
|
39587
f84b70e3bb9c
more reactive handling of Isabelle_Process startup errors;
wenzelm
parents:
39585
diff
changeset
|
133 |
val rc = process_result.join |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
134 |
system_output("process terminated") |
52581 | 135 |
close(command_input) |
136 |
for ((thread, _) <- List(stdout, stderr, command_input, message)) |
|
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
137 |
thread.join |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
138 |
system_output("process_manager terminated") |
48016
edbc8e8accd9
more explicit treatment of return code vs. session phase;
wenzelm
parents:
46774
diff
changeset
|
139 |
exit_message(rc) |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
140 |
} |
45027
f459e93a038e
more abstract wrapping of fifos as System_Channel;
wenzelm
parents:
44775
diff
changeset
|
141 |
system_channel.accepted() |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
142 |
} |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
143 |
|
39572 | 144 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
145 |
/* management methods */ |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
146 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
147 |
def join() { process_manager.join() } |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
148 |
|
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
149 |
def terminate() |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
150 |
{ |
52581 | 151 |
close(command_input) |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
152 |
system_output("Terminating Isabelle process") |
39585
00be8711082f
main Isabelle_Process via Isabelle_System.Managed_Process;
wenzelm
parents:
39575
diff
changeset
|
153 |
terminate_process() |
27973
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
154 |
} |
18d02c0b90b6
moved class Result into static object, removed dynamic tree method;
wenzelm
parents:
27963
diff
changeset
|
155 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
156 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
157 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
158 |
/** stream actors **/ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
159 |
|
46773 | 160 |
/* physical output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
161 |
|
46773 | 162 |
private def physical_output_actor(err: Boolean): (Thread, Actor) = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
163 |
{ |
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
164 |
val (name, reader, markup) = |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
165 |
if (err) ("standard_error", process.stderr, Markup.STDERR) |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
50117
diff
changeset
|
166 |
else ("standard_output", process.stdout, Markup.STDOUT) |
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
167 |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
168 |
Simple_Thread.actor(name) { |
46769 | 169 |
try { |
170 |
var result = new StringBuilder(100) |
|
171 |
var finished = false |
|
172 |
while (!finished) { |
|
28045 | 173 |
//{{{ |
174 |
var c = -1 |
|
175 |
var done = false |
|
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
176 |
while (!done && (result.length == 0 || reader.ready)) { |
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
177 |
c = reader.read |
28045 | 178 |
if (c >= 0) result.append(c.asInstanceOf[Char]) |
179 |
else done = true |
|
180 |
} |
|
181 |
if (result.length > 0) { |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
182 |
output(markup, Nil, List(XML.Text(decode(result.toString)))) |
28045 | 183 |
result.length = 0 |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
184 |
} |
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
185 |
else { |
45633
2cb7e34f6096
retain stderr and include it in syslog, which is buffered and thus increases the chance that users see remains from crashes etc.;
wenzelm
parents:
45158
diff
changeset
|
186 |
reader.close |
28045 | 187 |
finished = true |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
188 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
189 |
//}}} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
190 |
} |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
191 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
192 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
193 |
system_output(name + " terminated") |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
194 |
} |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
195 |
} |
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
196 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
197 |
|
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
198 |
/* command input */ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
199 |
|
39572 | 200 |
private def input_actor(raw_stream: OutputStream): (Thread, Actor) = |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
201 |
{ |
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
202 |
val name = "command_input" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
203 |
Simple_Thread.actor(name) { |
46769 | 204 |
try { |
205 |
val stream = new BufferedOutputStream(raw_stream) |
|
206 |
var finished = false |
|
207 |
while (!finished) { |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
208 |
//{{{ |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
209 |
receive { |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
210 |
case Input_Chunks(chunks) => |
54440 | 211 |
Bytes(chunks.map(_.length).mkString("", ",", "\n")).write(stream) |
212 |
chunks.foreach(_.write(stream)) |
|
38270
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
213 |
stream.flush |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
214 |
case Close => |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
215 |
stream.close |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
216 |
finished = true |
71bb3c273dd1
native Isabelle_Process commands, based on efficient byte channel protocol for string lists;
wenzelm
parents:
38262
diff
changeset
|
217 |
case bad => System.err.println(name + ": ignoring bad message " + bad) |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
218 |
} |
28045 | 219 |
//}}} |
27963 | 220 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
221 |
} |
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
222 |
catch { case e: IOException => system_output(name + ": " + e.getMessage) } |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
223 |
system_output(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
224 |
} |
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
225 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
226 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
227 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
228 |
/* message output */ |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
229 |
|
39572 | 230 |
private def message_actor(stream: InputStream): (Thread, Actor) = |
39526 | 231 |
{ |
232 |
class EOF extends Exception |
|
233 |
class Protocol_Error(msg: String) extends Exception(msg) |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
234 |
|
39528
c01d89d18ff0
refined Isabelle_Process startup: emit \002 before rendezvous on fifos, more robust treatment of startup failure with timeout, do not quit() after main loop;
wenzelm
parents:
39526
diff
changeset
|
235 |
val name = "message_output" |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
38573
diff
changeset
|
236 |
Simple_Thread.actor(name) { |
34100 | 237 |
val default_buffer = new Array[Byte](65536) |
238 |
var c = -1 |
|
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
239 |
|
52799 | 240 |
def read_int(): Int = |
241 |
//{{{ |
|
34100 | 242 |
{ |
243 |
var n = 0 |
|
244 |
c = stream.read |
|
39526 | 245 |
if (c == -1) throw new EOF |
34100 | 246 |
while (48 <= c && c <= 57) { |
247 |
n = 10 * n + (c - 48) |
|
248 |
c = stream.read |
|
249 |
} |
|
52799 | 250 |
if (c != 10) |
251 |
throw new Protocol_Error("malformed header: expected integer followed by newline") |
|
252 |
else n |
|
253 |
} |
|
254 |
//}}} |
|
34100 | 255 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
256 |
def read_chunk_bytes(): (Array[Byte], Int) = |
52799 | 257 |
//{{{ |
258 |
{ |
|
259 |
val n = read_int() |
|
34100 | 260 |
val buf = |
261 |
if (n <= default_buffer.size) default_buffer |
|
262 |
else new Array[Byte](n) |
|
263 |
||
264 |
var i = 0 |
|
265 |
var m = 0 |
|
266 |
do { |
|
267 |
m = stream.read(buf, i, n - i) |
|
39731
5cb0d7b0d601
bulk read: observe EOF protocol more carefully -- 0 counts as successful read;
wenzelm
parents:
39632
diff
changeset
|
268 |
if (m != -1) i += m |
52799 | 269 |
} |
270 |
while (m != -1 && n > i) |
|
34100 | 271 |
|
52799 | 272 |
if (i != n) |
273 |
throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") |
|
34100 | 274 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
275 |
(buf, n) |
34100 | 276 |
} |
52799 | 277 |
//}}} |
34100 | 278 |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
279 |
def read_chunk(): XML.Body = |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
280 |
{ |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
281 |
val (buf, n) = read_chunk_bytes() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
282 |
YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
283 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
284 |
|
46769 | 285 |
try { |
286 |
do { |
|
287 |
try { |
|
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
288 |
val header = read_chunk() |
46769 | 289 |
header match { |
49677
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
290 |
case List(XML.Elem(Markup(name, props), Nil)) => |
c4e2762a265c
more direct message header: eliminated historic encoding via single letter;
wenzelm
parents:
49445
diff
changeset
|
291 |
val kind = name.intern |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
292 |
if (kind == Markup.PROTOCOL) { |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
293 |
val (buf, n) = read_chunk_bytes() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
294 |
protocol_output(props, Bytes(buf, 0, n)) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
295 |
} |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
296 |
else { |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
297 |
val body = read_chunk() |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
298 |
output(kind, props, body) |
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
299 |
} |
46769 | 300 |
case _ => |
54442
c39972ddd672
more specific Protocol_Output: empty message.body, main content via bytes/text;
wenzelm
parents:
54440
diff
changeset
|
301 |
read_chunk() |
46769 | 302 |
throw new Protocol_Error("bad header: " + header.toString) |
303 |
} |
|
28063 | 304 |
} |
46769 | 305 |
catch { case _: EOF => } |
52799 | 306 |
} |
307 |
while (c != -1) |
|
46769 | 308 |
} |
309 |
catch { |
|
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
310 |
case e: IOException => system_output("Cannot read message:\n" + e.getMessage) |
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
311 |
case e: Protocol_Error => system_output("Malformed message:\n" + e.getMessage) |
46769 | 312 |
} |
34100 | 313 |
stream.close |
314 |
||
46772
be21f050eda4
tuned signature -- emphasize Isabelle_Process Input vs. Output;
wenzelm
parents:
46769
diff
changeset
|
315 |
system_output(name + " terminated") |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
316 |
} |
39526 | 317 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
318 |
|
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
319 |
|
38259
2b61c5e27399
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
wenzelm
parents:
38253
diff
changeset
|
320 |
|
56387 | 321 |
/** protocol commands **/ |
322 |
||
323 |
def protocol_command_bytes(name: String, args: Bytes*): Unit = |
|
54440 | 324 |
command_input._2 ! Input_Chunks(Bytes(name) :: args.toList) |
38372
e753f71b6b34
added Isabelle_Process.input_bytes, which avoids the somewhat slow Standard_System.string_bytes (just in case someone wants to stream raw data at 250MB/s);
wenzelm
parents:
38270
diff
changeset
|
325 |
|
52582 | 326 |
def protocol_command(name: String, args: String*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
327 |
{ |
56385 | 328 |
receiver(new Prover.Input(name, args.toList)) |
56387 | 329 |
protocol_command_bytes(name, args.map(Bytes(_)): _*) |
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43695
diff
changeset
|
330 |
} |
27949
6eb0327c0b9b
Isabelle process management -- always reactive due to multi-threaded I/O.
wenzelm
parents:
diff
changeset
|
331 |
} |