67904
|
1 |
(*:maxLineLen=78:*)
|
|
2 |
|
|
3 |
theory Server
|
|
4 |
imports Base
|
|
5 |
begin
|
|
6 |
|
|
7 |
chapter \<open>The Isabelle server\<close>
|
|
8 |
|
|
9 |
text \<open>
|
|
10 |
An Isabelle session requires at least two processes, which are both rather
|
|
11 |
heavy: Isabelle/Scala for the system infrastructure and Isabelle/ML for the
|
|
12 |
logic session (e.g.\ HOL). In principle, these processes can be invoked
|
|
13 |
directly on the command-line, e.g.\ via @{tool java}, @{tool scala}, @{tool
|
|
14 |
process}, @{tool console}, but this approach is inadequate for reactive
|
|
15 |
applications that require quick responses from the prover.
|
|
16 |
|
|
17 |
In contrast, the Isabelle server exposes Isabelle/Scala as a
|
|
18 |
``terminate-stay-resident'' application that manages multiple logic
|
|
19 |
\<^emph>\<open>sessions\<close> and concurrent tasks to use \<^emph>\<open>theories\<close>. This provides an
|
|
20 |
analogous to @{ML Thy_Info.use_theories} in Isabelle/ML, but with full
|
|
21 |
concurrency and Isabelle/PIDE markup.
|
|
22 |
|
|
23 |
The client/server arrangement via TCP sockets also opens possibilities for
|
|
24 |
remote Isabelle services that are accessed by local applications, e.g.\ via
|
|
25 |
an SSH tunnel.
|
|
26 |
\<close>
|
|
27 |
|
|
28 |
|
|
29 |
section \<open>Command-line tools\<close>
|
|
30 |
|
|
31 |
subsection \<open>Server \label{sec:tool-server}\<close>
|
|
32 |
|
|
33 |
text \<open>
|
|
34 |
The @{tool_def server} tool manages resident server processes:
|
|
35 |
@{verbatim [display]
|
|
36 |
\<open>Usage: isabelle server [OPTIONS]
|
|
37 |
|
|
38 |
Options are:
|
|
39 |
-L FILE logging on FILE
|
|
40 |
-c console interaction with specified server
|
|
41 |
-l list servers (alternative operation)
|
|
42 |
-n NAME explicit server name (default: isabelle)
|
|
43 |
-p PORT explicit server port
|
|
44 |
-s assume existing server, no implicit startup
|
|
45 |
-x exit specified server (alternative operation)
|
|
46 |
|
|
47 |
Manage resident Isabelle servers.\<close>}
|
|
48 |
|
|
49 |
The main operation of \<^verbatim>\<open>isabelle server\<close> is to ensure that a named server is
|
|
50 |
running, either by finding an already running process (according to the
|
|
51 |
central database file @{path "$ISABELLE_HOME_USER/servers.db"}) or by
|
|
52 |
becoming itself a new server that accepts connections on a particular TCP
|
|
53 |
socket. The server name and its address are printed as initial output line.
|
|
54 |
If another server instance is already running, the current
|
|
55 |
\<^verbatim>\<open>isabelle server\<close> process will terminate; otherwise, it keeps running as a
|
|
56 |
new server process until an explicit \<^verbatim>\<open>shutdown\<close> command is received.
|
|
57 |
Further details of the server socket protocol are explained in
|
|
58 |
\secref{sec:server-protocol}.
|
|
59 |
|
|
60 |
Other server management operations are invoked via options \<^verbatim>\<open>-l\<close> and \<^verbatim>\<open>-x\<close>
|
|
61 |
(see below).
|
|
62 |
|
|
63 |
\<^medskip>
|
|
64 |
Option \<^verbatim>\<open>-n\<close> specifies an alternative server name: at most one process for
|
|
65 |
each name may run, but each server instance supports multiple connections
|
|
66 |
and logic sessions.
|
|
67 |
|
|
68 |
\<^medskip>
|
|
69 |
Option \<^verbatim>\<open>-p\<close> specifies an explicit TCP port for the server socket (which is
|
|
70 |
always on \<^verbatim>\<open>localhost\<close>): the default is to let the operating system assign a
|
|
71 |
free port number.
|
|
72 |
|
|
73 |
\<^medskip>
|
|
74 |
Option \<^verbatim>\<open>-s\<close> strictly assumes that the specified server process is already
|
|
75 |
running, skipping the optional server startup phase.
|
|
76 |
|
|
77 |
\<^medskip>
|
|
78 |
Option \<^verbatim>\<open>-c\<close> connects the console in/out channels after the initial check
|
|
79 |
for a suitable server process. Note that the @{tool client} tool
|
|
80 |
(\secref{sec:tool-client}) provides a more convenient way to do this
|
|
81 |
interactively, together with command-line editor support.
|
|
82 |
|
|
83 |
\<^medskip>
|
|
84 |
Option \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
|
|
85 |
details.
|
|
86 |
|
|
87 |
\<^medskip>
|
|
88 |
Option \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a \<^verbatim>\<open>shutdown\<close>
|
|
89 |
command.
|
|
90 |
|
|
91 |
\<^medskip>
|
|
92 |
Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
|
|
93 |
and session operations.
|
|
94 |
\<close>
|
|
95 |
|
|
96 |
|
|
97 |
subsection \<open>Client \label{sec:tool-client}\<close>
|
|
98 |
|
|
99 |
text \<open>
|
|
100 |
The @{tool_def client} provides console interaction for Isabelle servers:
|
|
101 |
@{verbatim [display]
|
|
102 |
\<open>Usage: isabelle client [OPTIONS]
|
|
103 |
|
|
104 |
Options are:
|
|
105 |
-n NAME explicit server name
|
|
106 |
-p PORT explicit server port
|
|
107 |
|
|
108 |
Console interaction for Isabelle server (with line-editor).\<close>}
|
|
109 |
|
|
110 |
This is a convenient wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
|
|
111 |
experimentation, wrapped into @{setting ISABELLE_LINE_EDITOR} if available.
|
|
112 |
The server name is sufficient for identification, as the client can
|
|
113 |
determine the connection details from the local database of active servers.
|
|
114 |
|
|
115 |
\<^medskip>
|
|
116 |
Option \<^verbatim>\<open>-n\<close> specifies an explicit server name as in @{tool server}.
|
|
117 |
|
|
118 |
\<^medskip>
|
|
119 |
Option \<^verbatim>\<open>-p\<close> specifies an explicit server port as in @{tool server}.
|
|
120 |
\<close>
|
|
121 |
|
|
122 |
|
|
123 |
subsection \<open>Examples\<close>
|
|
124 |
|
|
125 |
text \<open>
|
|
126 |
Ensure that a particular server instance is running in the background:
|
|
127 |
@{verbatim [display] \<open>isabelle server -n test &\<close>}
|
|
128 |
|
|
129 |
Here the first line of output presents the connection details:\<^footnote>\<open>This
|
|
130 |
information may be used in an independent TCP client, while the
|
|
131 |
Isabelle/Scala tool merely needs the server name to access the database of
|
|
132 |
servers.\<close>
|
|
133 |
@{verbatim [display] \<open>server "test" = 127.0.0.1:4711 (password "XYZ")\<close>}
|
|
134 |
|
|
135 |
\<^medskip>
|
|
136 |
List available server processes:
|
|
137 |
@{verbatim [display] \<open>isabelle server -l\<close>}
|
|
138 |
|
|
139 |
\<^medskip>
|
|
140 |
Connect the command-line client to the above test server:
|
|
141 |
@{verbatim [display] \<open>isabelle client -n test\<close>}
|
|
142 |
|
|
143 |
Interaction now works on a line-by-line basis, with commands like \<^verbatim>\<open>help\<close> or
|
|
144 |
\<^verbatim>\<open>echo\<close>. For example, some JSON values may be echoed like this:
|
|
145 |
|
|
146 |
@{verbatim [display]
|
|
147 |
\<open>echo 42
|
|
148 |
echo [1, 2, 3]
|
|
149 |
echo {"a": "text", "b": true, "c": 42}\<close>}
|
|
150 |
|
|
151 |
Closing the connection (via CTRL-D) leaves the server running: it is
|
|
152 |
possible to reconnect again, and have multiple connections at the same time.
|
|
153 |
|
|
154 |
\<^medskip>
|
|
155 |
Finally, exit the named server on the command-line:
|
|
156 |
@{verbatim [display] \<open>isabelle server -n test -x\<close>}
|
|
157 |
\<close>
|
|
158 |
|
|
159 |
|
|
160 |
section \<open>Protocol messages \label{sec:server-protocol}\<close>
|
|
161 |
|
|
162 |
text \<open>
|
|
163 |
The Isabelle server listens on a regular TCP socket, using a line-oriented
|
|
164 |
protocol of structured messages: input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
|
|
165 |
(via \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>) are strictly alternating on the toplevel, but
|
|
166 |
commands may also return a \<^emph>\<open>task\<close> identifier to indicate an ongoing
|
|
167 |
asynchronous process that is joined later (via \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>).
|
|
168 |
Asynchronous \<^verbatim>\<open>NOTE\<close> messages may occur at any time: they are independent of
|
|
169 |
the main command-reply protocol.
|
|
170 |
|
|
171 |
For example, the synchronous \<^verbatim>\<open>echo\<close> command immediately returns its
|
|
172 |
argument as \<^verbatim>\<open>OK\<close> result. In contrast, the asynchronous \<^verbatim>\<open>session_build\<close>
|
|
173 |
command returns \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> and continues in the background. It
|
|
174 |
will eventually produce \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> or
|
|
175 |
\<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> with the final result. Intermediately, it
|
|
176 |
may emit asynchronous messages of the form \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close>
|
|
177 |
to inform about its progress. Due to the explicit task identifier, the
|
|
178 |
client can show these messages in the proper context, e.g.\ a GUI window for
|
|
179 |
the session build job.
|
|
180 |
|
|
181 |
\medskip Subsequently, the protocol message formats are described in further
|
|
182 |
detail.
|
|
183 |
\<close>
|
|
184 |
|
|
185 |
|
|
186 |
subsection \<open>Byte messages\<close>
|
|
187 |
|
|
188 |
text \<open>
|
|
189 |
The client-server connection is a raw byte-channel for bidirectional
|
|
190 |
communication, but the Isabelle server always works with messages of a
|
|
191 |
particular length. Messages are written as a single chunk that is flushed
|
|
192 |
immediately.
|
|
193 |
|
|
194 |
The message boundary is determined as follows:
|
|
195 |
|
|
196 |
\<^item> A \<^emph>\<open>short message\<close> consists of a single line: it is a sequence of
|
|
197 |
arbitrary bytes excluding CR (13) and LF (10), and terminated by CR-LF or
|
|
198 |
just LF.
|
|
199 |
|
|
200 |
\<^item> A \<^emph>\<open>long message\<close> starts with a single line as above, which consists
|
|
201 |
only of decimal digits: that is interpreted as length of the subsequent
|
|
202 |
block of arbitrary bytes. A final line-terminator may be included here,
|
|
203 |
but is not required.
|
|
204 |
|
|
205 |
Messages in JSON format (see below) always fit on a single line, due to
|
|
206 |
escaping of newline characters within string literals. This is convenient
|
|
207 |
for interactive experimentation, but it can impact performance for very long
|
|
208 |
messages. If the message byte-length is given on the preceding line, the
|
|
209 |
server can read the message efficiently as a single block.
|
|
210 |
\<close>
|
|
211 |
|
|
212 |
|
|
213 |
subsection \<open>Text messages\<close>
|
|
214 |
|
|
215 |
text \<open>
|
|
216 |
Messages are read and written as byte streams (with byte lengths), but the
|
|
217 |
content is always interpreted as plain text in terms of the UTF-8
|
|
218 |
encoding.\<^footnote>\<open>See also the ``UTF-8 Everywhere Manifesto''
|
|
219 |
\<^url>\<open>http://utf8everywhere.org\<close>.\<close>
|
|
220 |
|
|
221 |
Note that line-endings and other formatting characters are invariant wrt.
|
|
222 |
UTF-8 representation of text: thus implementations are free to determine the
|
|
223 |
overall message structure before or after applying the text encoding.
|
|
224 |
\<close>
|
|
225 |
|
|
226 |
|
|
227 |
subsection \<open>Input and output messages\<close>
|
|
228 |
|
|
229 |
text \<open>
|
|
230 |
Server input and output messages have a uniform format as follows:
|
|
231 |
|
|
232 |
\<^item> \<open>name argument\<close> such that:
|
|
233 |
|
|
234 |
\<^item> \<open>name\<close> is the longest prefix consisting of ASCII letters, digits,
|
|
235 |
``\<^verbatim>\<open>_\<close>'' (underscore), or ``\<^verbatim>\<open>.\<close>'' (dot),
|
|
236 |
|
|
237 |
\<^item> the separator between \<open>name\<close> and \<open>argument\<close> is the longest possible
|
|
238 |
sequence of ASCII blanks (it could be empty, e.g.\ when the argument
|
|
239 |
starts with a quote or bracket),
|
|
240 |
|
|
241 |
\<^item> \<open>argument\<close> is the rest of the message without the line terminator.
|
|
242 |
|
|
243 |
\<^medskip>
|
|
244 |
Input messages are sent from the client to the server. Here the \<open>name\<close>
|
|
245 |
specifies a \<^emph>\<open>server command\<close>: the list of known commands may be
|
|
246 |
retrieved via the \<^verbatim>\<open>help\<close> command.
|
|
247 |
|
|
248 |
\<^medskip>
|
|
249 |
Output messages are sent from the server to the client. Here the \<open>name\<close>
|
|
250 |
specifies the \<^emph>\<open>server reply\<close>, which always has a specific meaning as
|
|
251 |
follows:
|
|
252 |
|
|
253 |
\<^item> synchronous results: \<^verbatim>\<open>OK\<close> or \<^verbatim>\<open>ERROR\<close>
|
|
254 |
\<^item> asynchronous results: \<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>
|
|
255 |
\<^item> intermediate notifications: \<^verbatim>\<open>NOTE\<close>
|
|
256 |
|
|
257 |
\<^medskip>
|
|
258 |
The \<open>argument\<close> format is uniform for both input and output messages:
|
|
259 |
|
|
260 |
\<^item> empty argument (Scala type \<^verbatim>\<open>Unit\<close>)
|
|
261 |
\<^item> XML element in YXML notation (Scala type \<^verbatim>\<open>XML.Elem\<close>)
|
|
262 |
\<^item> JSON value (Scala type \<^verbatim>\<open>JSON.T\<close>)
|
|
263 |
|
|
264 |
JSON values may consist of objects (records), arrays (lists), strings,
|
|
265 |
numbers, bools, null.\<^footnote>\<open>See also the official specification
|
|
266 |
\<^url>\<open>https://www.json.org\<close> and unofficial explorations ``Parsing JSON is a
|
|
267 |
Minefield'' \<^url>\<open>http://seriot.ch/parsing_json.php\<close>.\<close> Since JSON requires
|
|
268 |
explicit quotes and backslash-escapes to represent arbitrary text, the YXML
|
|
269 |
notation for XML trees (\secref{sec:yxml-vs-xml}) works better
|
|
270 |
for large messages with a lot of PIDE markup.
|
|
271 |
|
|
272 |
Nonetheless, the most common commands use JSON by default: big chunks of
|
|
273 |
text (theory sources etc.) are taken from the underlying file-system and
|
|
274 |
results are pre-formatted for plain-text output, without PIDE markup
|
|
275 |
information. This is a concession to simplicity: the server imitates the
|
|
276 |
appearance of command-line tools on top of the Isabelle/PIDE infrastructure.
|
|
277 |
\<close>
|
|
278 |
|
|
279 |
|
|
280 |
subsection \<open>Initial password exchange\<close>
|
|
281 |
|
|
282 |
text \<open>
|
|
283 |
Whenever a new client opens the server socket, the initial message needs to
|
|
284 |
be its unique password. The server replies either with \<^verbatim>\<open>OK\<close> (and some
|
|
285 |
information about the Isabelle version) or by silent disconnection of what
|
|
286 |
is considered an illegal connection attempt.
|
|
287 |
|
|
288 |
Server passwords are created as Universally Unique Identifier (UUID) in
|
|
289 |
Isabelle/Scala and stored in a per-user database, with restricted
|
|
290 |
file-system access only for the current user. The Isabelle/Scala server
|
|
291 |
implementation is careful to expose the password only on private output
|
|
292 |
channels, and not on a process command-line (which is accessible to other
|
|
293 |
users, e.g.\ via the \<^verbatim>\<open>ps\<close> command).
|
|
294 |
\<close>
|
|
295 |
|
|
296 |
|
|
297 |
subsection \<open>Synchronous commands\<close>
|
|
298 |
|
|
299 |
text \<open>
|
|
300 |
A \<^emph>\<open>synchronous command\<close> corresponds to regular function application in
|
|
301 |
Isabelle/Scala, with single argument and result (regular or error). Both the
|
|
302 |
argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
|
|
303 |
An error result typically consists of a JSON object with error message and
|
|
304 |
potentially further fields (this resembles exceptions in Scala).
|
|
305 |
|
|
306 |
These are the protocol exchanges for both cases of command execution:
|
|
307 |
\begin{center}
|
|
308 |
\begin{tabular}{rl}
|
|
309 |
\<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
|
|
310 |
(a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK\<close> \<open>result\<close> \\
|
|
311 |
(b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>ERROR\<close> \<open>result\<close> \\
|
|
312 |
\end{tabular}
|
|
313 |
\end{center}
|
|
314 |
\<close>
|
|
315 |
|
|
316 |
|
|
317 |
subsection \<open>Asynchronous commands\<close>
|
|
318 |
|
|
319 |
text \<open>
|
|
320 |
An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
|
|
321 |
or fails eventually, while emitting arbitrary notifications intermediately.
|
|
322 |
Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close> and
|
|
323 |
the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad command
|
|
324 |
syntax. For a running task, the termination is indicated later by
|
|
325 |
\<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result.
|
|
326 |
|
|
327 |
These are the protocol exchanges for various cases of command task
|
|
328 |
execution:
|
|
329 |
|
|
330 |
\begin{center}
|
|
331 |
\begin{tabular}{rl}
|
|
332 |
\<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
|
|
333 |
immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<close>\<^verbatim>\<open>}\<close> \\
|
|
334 |
intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
|
|
335 |
intermediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>NOTE {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
|
|
336 |
(a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FINISHED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\
|
|
337 |
(b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>FAILED {"task":\<close>\<open>id\<close>\<^verbatim>\<open>,\<close>\<open>\<dots>\<close>\<^verbatim>\<open>}\<close> \\[3ex]
|
|
338 |
\<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
|
|
339 |
immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>ERROR\<close>~\<open>\<dots>\<close> \\
|
|
340 |
\end{tabular}
|
|
341 |
\end{center}
|
|
342 |
|
|
343 |
All asynchronous messages are decorated with the task identifier that was
|
|
344 |
revealed in the immediate (synchronous) result. Thus it is possible to emit
|
|
345 |
further asynchronous commands and dispatch the mingled stream of
|
|
346 |
asynchronous messages properly.
|
|
347 |
|
|
348 |
The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
|
|
349 |
prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result with error message
|
|
350 |
\<^verbatim>\<open>Interrupt\<close>, but this is not guaranteed: the cancel event may come too
|
|
351 |
late or the task may just ignore it.
|
|
352 |
\<close>
|
|
353 |
|
|
354 |
end
|