wenzelm@30174
|
1 |
(* Title: Pure/System/isabelle_process.ML
|
wenzelm@25528
|
2 |
Author: Makarius
|
wenzelm@25528
|
3 |
|
wenzelm@38691
|
4 |
Isabelle process wrapper, based on private fifos for maximum
|
wenzelm@38691
|
5 |
robustness and performance.
|
wenzelm@39797
|
6 |
|
wenzelm@39797
|
7 |
Startup phases:
|
wenzelm@39797
|
8 |
. raw Posix process startup with uncontrolled output on stdout/stderr
|
wenzelm@39797
|
9 |
. stdout \002: ML running
|
wenzelm@39797
|
10 |
.. stdin/stdout/stderr freely available (raw ML loop)
|
wenzelm@39797
|
11 |
.. protocol thread initialization
|
wenzelm@39797
|
12 |
... switch to in_fifo/out_fifo channels (rendezvous via open)
|
wenzelm@39797
|
13 |
... out_fifo INIT(pid): channels ready
|
wenzelm@39797
|
14 |
... out_fifo STATUS(keywords)
|
wenzelm@39797
|
15 |
... out_fifo READY: main loop ready
|
wenzelm@25528
|
16 |
*)
|
wenzelm@25528
|
17 |
|
wenzelm@25528
|
18 |
signature ISABELLE_PROCESS =
|
wenzelm@25528
|
19 |
sig
|
wenzelm@26574
|
20 |
val isabelle_processN: string
|
wenzelm@38568
|
21 |
val add_command: string -> (string list -> unit) -> unit
|
wenzelm@38568
|
22 |
val command: string -> string list -> unit
|
wenzelm@38568
|
23 |
val crashes: exn list Unsynchronized.ref
|
wenzelm@38551
|
24 |
val init: string -> string -> unit
|
wenzelm@25528
|
25 |
end;
|
wenzelm@25528
|
26 |
|
wenzelm@31800
|
27 |
structure Isabelle_Process: ISABELLE_PROCESS =
|
wenzelm@25528
|
28 |
struct
|
wenzelm@25528
|
29 |
|
wenzelm@26550
|
30 |
(* print modes *)
|
wenzelm@25554
|
31 |
|
wenzelm@25748
|
32 |
val isabelle_processN = "isabelle_process";
|
wenzelm@25748
|
33 |
|
wenzelm@26550
|
34 |
val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
|
wenzelm@28036
|
35 |
val _ = Markup.add_mode isabelle_processN YXML.output_markup;
|
wenzelm@25841
|
36 |
|
wenzelm@25841
|
37 |
|
wenzelm@38568
|
38 |
(* commands *)
|
wenzelm@38568
|
39 |
|
wenzelm@38568
|
40 |
local
|
wenzelm@38568
|
41 |
|
wenzelm@38568
|
42 |
val global_commands = Unsynchronized.ref (Symtab.empty: (string list -> unit) Symtab.table);
|
wenzelm@38568
|
43 |
|
wenzelm@38568
|
44 |
in
|
wenzelm@38568
|
45 |
|
wenzelm@38568
|
46 |
fun add_command name cmd = CRITICAL (fn () =>
|
wenzelm@38568
|
47 |
Unsynchronized.change global_commands (fn cmds =>
|
wenzelm@38568
|
48 |
(if not (Symtab.defined cmds name) then ()
|
wenzelm@38568
|
49 |
else warning ("Redefining Isabelle process command " ^ quote name);
|
wenzelm@38568
|
50 |
Symtab.update (name, cmd) cmds)));
|
wenzelm@38568
|
51 |
|
wenzelm@38568
|
52 |
fun command name args =
|
wenzelm@38568
|
53 |
(case Symtab.lookup (! global_commands) name of
|
wenzelm@38568
|
54 |
NONE => error ("Undefined Isabelle process command " ^ quote name)
|
wenzelm@38568
|
55 |
| SOME cmd => cmd args);
|
wenzelm@38568
|
56 |
|
wenzelm@38568
|
57 |
end;
|
wenzelm@38568
|
58 |
|
wenzelm@38568
|
59 |
|
wenzelm@25841
|
60 |
(* message markup *)
|
wenzelm@25841
|
61 |
|
wenzelm@25841
|
62 |
local
|
wenzelm@25810
|
63 |
|
wenzelm@34102
|
64 |
fun chunk s = string_of_int (size s) ^ "\n" ^ s;
|
wenzelm@26574
|
65 |
|
wenzelm@34102
|
66 |
fun message _ _ _ "" = ()
|
wenzelm@38691
|
67 |
| message out_stream ch raw_props body =
|
wenzelm@34102
|
68 |
let
|
wenzelm@38691
|
69 |
val robust_props = map (pairself YXML.escape_controls) raw_props;
|
wenzelm@38691
|
70 |
val header = YXML.string_of (XML.Elem ((ch, robust_props), []));
|
wenzelm@38691
|
71 |
in TextIO.output (out_stream, chunk header ^ chunk body) (*atomic output!*) end;
|
wenzelm@25554
|
72 |
|
wenzelm@25554
|
73 |
in
|
wenzelm@25554
|
74 |
|
wenzelm@39778
|
75 |
fun standard_message out_stream with_serial ch body =
|
wenzelm@39197
|
76 |
message out_stream ch
|
wenzelm@39778
|
77 |
((if with_serial then cons (Markup.serialN, serial_string ()) else I)
|
wenzelm@39778
|
78 |
(Position.properties_of (Position.thread_data ()))) body;
|
wenzelm@25554
|
79 |
|
wenzelm@28044
|
80 |
fun init_message out_stream =
|
wenzelm@39849
|
81 |
message out_stream "A" [] (Session.welcome ());
|
wenzelm@25748
|
82 |
|
wenzelm@25554
|
83 |
end;
|
wenzelm@25554
|
84 |
|
wenzelm@25554
|
85 |
|
wenzelm@25841
|
86 |
(* channels *)
|
wenzelm@25841
|
87 |
|
wenzelm@28188
|
88 |
local
|
wenzelm@28188
|
89 |
|
wenzelm@28188
|
90 |
fun auto_flush stream =
|
wenzelm@28188
|
91 |
let
|
wenzelm@28189
|
92 |
val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
|
wenzelm@28188
|
93 |
fun loop () =
|
wenzelm@38554
|
94 |
(OS.Process.sleep (Time.fromMilliseconds 20); try TextIO.flushOut stream; loop ());
|
wenzelm@28188
|
95 |
in loop end;
|
wenzelm@28188
|
96 |
|
wenzelm@28188
|
97 |
in
|
wenzelm@28188
|
98 |
|
wenzelm@38551
|
99 |
fun setup_channels in_fifo out_fifo =
|
wenzelm@28189
|
100 |
let
|
wenzelm@39799
|
101 |
(*rendezvous*)
|
wenzelm@39799
|
102 |
val in_stream = TextIO.openIn in_fifo;
|
wenzelm@39799
|
103 |
val out_stream = TextIO.openOut out_fifo;
|
wenzelm@39799
|
104 |
|
wenzelm@37216
|
105 |
val _ = Simple_Thread.fork false (auto_flush out_stream);
|
wenzelm@37216
|
106 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
|
wenzelm@37216
|
107 |
val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
|
wenzelm@28044
|
108 |
in
|
wenzelm@39778
|
109 |
Output.status_fn := standard_message out_stream false "B";
|
wenzelm@39778
|
110 |
Output.report_fn := standard_message out_stream false "C";
|
wenzelm@39778
|
111 |
Output.writeln_fn := standard_message out_stream true "D";
|
wenzelm@39778
|
112 |
Output.tracing_fn := standard_message out_stream true "E";
|
wenzelm@39778
|
113 |
Output.warning_fn := standard_message out_stream true "F";
|
wenzelm@39778
|
114 |
Output.error_fn := standard_message out_stream true "G";
|
wenzelm@37121
|
115 |
Output.priority_fn := ! Output.writeln_fn;
|
wenzelm@28498
|
116 |
Output.prompt_fn := ignore;
|
wenzelm@38551
|
117 |
(in_stream, out_stream)
|
wenzelm@28044
|
118 |
end;
|
wenzelm@25841
|
119 |
|
wenzelm@28188
|
120 |
end;
|
wenzelm@28188
|
121 |
|
wenzelm@25841
|
122 |
|
wenzelm@39511
|
123 |
(* protocol loop -- uninterruptible *)
|
wenzelm@38568
|
124 |
|
wenzelm@38568
|
125 |
val crashes = Unsynchronized.ref ([]: exn list);
|
wenzelm@38568
|
126 |
|
wenzelm@38568
|
127 |
local
|
wenzelm@38568
|
128 |
|
wenzelm@38568
|
129 |
fun recover crash =
|
wenzelm@38568
|
130 |
(CRITICAL (fn () => Unsynchronized.change crashes (cons crash));
|
wenzelm@38568
|
131 |
warning "Recovering from Isabelle process crash -- see also Isabelle_Process.crashes");
|
wenzelm@38568
|
132 |
|
wenzelm@38568
|
133 |
fun read_chunk stream len =
|
wenzelm@38568
|
134 |
let
|
wenzelm@38568
|
135 |
val n =
|
wenzelm@38568
|
136 |
(case Int.fromString len of
|
wenzelm@38568
|
137 |
SOME n => n
|
wenzelm@38568
|
138 |
| NONE => error ("Isabelle process: malformed chunk header " ^ quote len));
|
wenzelm@38568
|
139 |
val chunk = TextIO.inputN (stream, n);
|
wenzelm@38568
|
140 |
val m = size chunk;
|
wenzelm@38568
|
141 |
in
|
wenzelm@38568
|
142 |
if m = n then chunk
|
wenzelm@38568
|
143 |
else error ("Isabelle process: bad chunk (" ^ string_of_int m ^ " vs. " ^ string_of_int n ^ ")")
|
wenzelm@38568
|
144 |
end;
|
wenzelm@38568
|
145 |
|
wenzelm@38568
|
146 |
fun read_command stream =
|
wenzelm@38568
|
147 |
(case TextIO.inputLine stream of
|
wenzelm@38568
|
148 |
NONE => raise Runtime.TERMINATE
|
wenzelm@38568
|
149 |
| SOME line => map (read_chunk stream) (space_explode "," line));
|
wenzelm@38568
|
150 |
|
wenzelm@38568
|
151 |
fun run_command name args =
|
wenzelm@38568
|
152 |
Runtime.debugging (command name) args
|
wenzelm@38568
|
153 |
handle exn =>
|
wenzelm@38568
|
154 |
error ("Isabelle process command failure: " ^ name ^ "\n" ^ ML_Compiler.exn_message exn);
|
wenzelm@38568
|
155 |
|
wenzelm@38568
|
156 |
in
|
wenzelm@38568
|
157 |
|
wenzelm@38568
|
158 |
fun loop stream =
|
wenzelm@38568
|
159 |
let val continue =
|
wenzelm@38568
|
160 |
(case read_command stream of
|
wenzelm@38568
|
161 |
[] => (Output.error_msg "Isabelle process: no input"; true)
|
wenzelm@38568
|
162 |
| name :: args => (run_command name args; true))
|
wenzelm@38568
|
163 |
handle Runtime.TERMINATE => false
|
wenzelm@38568
|
164 |
| exn => (Output.error_msg (ML_Compiler.exn_message exn) handle crash => recover crash; true);
|
wenzelm@38568
|
165 |
in if continue then loop stream else () end;
|
wenzelm@38568
|
166 |
|
wenzelm@38568
|
167 |
end;
|
wenzelm@38568
|
168 |
|
wenzelm@38568
|
169 |
|
wenzelm@25554
|
170 |
(* init *)
|
wenzelm@25554
|
171 |
|
wenzelm@39797
|
172 |
fun init in_fifo out_fifo = ignore (Simple_Thread.fork false (fn () =>
|
wenzelm@38551
|
173 |
let
|
wenzelm@39797
|
174 |
val _ = OS.Process.sleep (Time.fromMilliseconds 500); (*yield to raw ML toplevel*)
|
wenzelm@39797
|
175 |
val _ = Output.std_output Symbol.STX;
|
wenzelm@39797
|
176 |
|
wenzelm@39797
|
177 |
val _ = quick_and_dirty := true; (* FIXME !? *)
|
wenzelm@39797
|
178 |
val _ = Context.set_thread_data NONE;
|
wenzelm@38551
|
179 |
val _ = Unsynchronized.change print_mode
|
wenzelm@38551
|
180 |
(fold (update op =) [isabelle_processN, Keyword.keyword_statusN, Pretty.symbolicN]);
|
wenzelm@39797
|
181 |
|
wenzelm@38551
|
182 |
val (in_stream, out_stream) = setup_channels in_fifo out_fifo;
|
wenzelm@38551
|
183 |
val _ = init_message out_stream;
|
wenzelm@38551
|
184 |
val _ = Keyword.status ();
|
wenzelm@39855
|
185 |
val _ = Output.status (Markup.markup Markup.ready "Prover ready");
|
wenzelm@39797
|
186 |
in loop in_stream end));
|
wenzelm@25528
|
187 |
|
wenzelm@25528
|
188 |
end;
|
wenzelm@39797
|
189 |
|