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
|
67918
|
79 |
for a suitable server process. Also note that the @{tool client} tool
|
|
80 |
(\secref{sec:tool-client}) provides a command-line editor to interact with
|
|
81 |
the server.
|
67904
|
82 |
|
|
83 |
\<^medskip>
|
|
84 |
Option \<^verbatim>\<open>-L\<close> specifies a log file for exceptional output of internal server
|
|
85 |
and session operations.
|
67918
|
86 |
|
|
87 |
\<^medskip>
|
|
88 |
Operation \<^verbatim>\<open>-l\<close> lists all active server processes with their connection
|
|
89 |
details.
|
|
90 |
|
|
91 |
\<^medskip>
|
|
92 |
Operation \<^verbatim>\<open>-x\<close> exits the specified server process by sending it a
|
|
93 |
\<^verbatim>\<open>shutdown\<close> command.
|
67904
|
94 |
\<close>
|
|
95 |
|
|
96 |
|
|
97 |
subsection \<open>Client \label{sec:tool-client}\<close>
|
|
98 |
|
|
99 |
text \<open>
|
67918
|
100 |
The @{tool_def client} tool provides console interaction for Isabelle
|
|
101 |
servers:
|
67904
|
102 |
@{verbatim [display]
|
|
103 |
\<open>Usage: isabelle client [OPTIONS]
|
|
104 |
|
|
105 |
Options are:
|
|
106 |
-n NAME explicit server name
|
|
107 |
-p PORT explicit server port
|
|
108 |
|
|
109 |
Console interaction for Isabelle server (with line-editor).\<close>}
|
|
110 |
|
67918
|
111 |
This is a wrapper to \<^verbatim>\<open>isabelle server -s -c\<close> for interactive
|
|
112 |
experimentation, which uses @{setting ISABELLE_LINE_EDITOR} if available.
|
67904
|
113 |
The server name is sufficient for identification, as the client can
|
|
114 |
determine the connection details from the local database of active servers.
|
|
115 |
|
|
116 |
\<^medskip>
|
|
117 |
Option \<^verbatim>\<open>-n\<close> specifies an explicit server name as in @{tool server}.
|
|
118 |
|
|
119 |
\<^medskip>
|
|
120 |
Option \<^verbatim>\<open>-p\<close> specifies an explicit server port as in @{tool server}.
|
|
121 |
\<close>
|
|
122 |
|
|
123 |
|
|
124 |
subsection \<open>Examples\<close>
|
|
125 |
|
|
126 |
text \<open>
|
|
127 |
Ensure that a particular server instance is running in the background:
|
|
128 |
@{verbatim [display] \<open>isabelle server -n test &\<close>}
|
|
129 |
|
67918
|
130 |
The first line of output presents the connection details:\<^footnote>\<open>This information
|
|
131 |
may be used in other TCP clients, without access to Isabelle/Scala and the
|
|
132 |
underlying database of running servers.\<close>
|
67904
|
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>
|
67918
|
155 |
Exit the named server on the command-line:
|
67904
|
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
|
67918
|
164 |
protocol of structured messages. Input \<^emph>\<open>commands\<close> and output \<^emph>\<open>results\<close>
|
67904
|
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
|
67918
|
169 |
the main command-result protocol.
|
67904
|
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
|
67918
|
179 |
this particular session build job.
|
67904
|
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 |
|
67918
|
194 |
Message boundaries are determined as follows:
|
67904
|
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 |
|
67918
|
200 |
\<^item> A \<^emph>\<open>long message\<close> starts with a single that consists only of decimal
|
|
201 |
digits: these are interpreted as length of the subsequent block of
|
|
202 |
arbitrary bytes. A final line-terminator (as above) may be included here,
|
67904
|
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
|
67918
|
209 |
server can read the message more efficiently as a single block.
|
67904
|
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 |
|
67917
|
227 |
subsection \<open>Input and output messages \label{sec:input-output-messages}\<close>
|
67904
|
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,
|
67918
|
235 |
``\<^verbatim>\<open>_\<close>'', ``\<^verbatim>\<open>.\<close>'',
|
67904
|
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 |
|
67918
|
241 |
\<^item> \<open>argument\<close> is the rest of the message without line terminator.
|
67904
|
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
|
67918
|
286 |
is considered an illegal connection attempt. Note that @{tool client}
|
|
287 |
already presents the correct password internally.
|
67904
|
288 |
|
|
289 |
Server passwords are created as Universally Unique Identifier (UUID) in
|
|
290 |
Isabelle/Scala and stored in a per-user database, with restricted
|
|
291 |
file-system access only for the current user. The Isabelle/Scala server
|
|
292 |
implementation is careful to expose the password only on private output
|
|
293 |
channels, and not on a process command-line (which is accessible to other
|
|
294 |
users, e.g.\ via the \<^verbatim>\<open>ps\<close> command).
|
|
295 |
\<close>
|
|
296 |
|
|
297 |
|
|
298 |
subsection \<open>Synchronous commands\<close>
|
|
299 |
|
|
300 |
text \<open>
|
|
301 |
A \<^emph>\<open>synchronous command\<close> corresponds to regular function application in
|
|
302 |
Isabelle/Scala, with single argument and result (regular or error). Both the
|
|
303 |
argument and the result may consist of type \<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close>.
|
|
304 |
An error result typically consists of a JSON object with error message and
|
67918
|
305 |
potentially further result fields (this resembles exceptions in Scala).
|
67904
|
306 |
|
|
307 |
These are the protocol exchanges for both cases of command execution:
|
|
308 |
\begin{center}
|
|
309 |
\begin{tabular}{rl}
|
|
310 |
\<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
|
|
311 |
(a) regular \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK\<close> \<open>result\<close> \\
|
|
312 |
(b) error \<^bold>\<open>output:\<close> & \<^verbatim>\<open>ERROR\<close> \<open>result\<close> \\
|
|
313 |
\end{tabular}
|
|
314 |
\end{center}
|
|
315 |
\<close>
|
|
316 |
|
|
317 |
|
|
318 |
subsection \<open>Asynchronous commands\<close>
|
|
319 |
|
|
320 |
text \<open>
|
|
321 |
An \<^emph>\<open>asynchronous command\<close> corresponds to an ongoing process that finishes
|
67918
|
322 |
or fails eventually, while emitting arbitrary notifications in between.
|
|
323 |
Formally, it starts as synchronous command with immediate result \<^verbatim>\<open>OK\<close>
|
|
324 |
giving the \<^verbatim>\<open>task\<close> identifier, or an immediate \<^verbatim>\<open>ERROR\<close> that indicates bad
|
|
325 |
command syntax. For a running task, the termination is indicated later by
|
|
326 |
\<^verbatim>\<open>FINISHED\<close> or \<^verbatim>\<open>FAILED\<close>, together with its ultimate result value.
|
67904
|
327 |
|
|
328 |
These are the protocol exchanges for various cases of command task
|
|
329 |
execution:
|
|
330 |
|
|
331 |
\begin{center}
|
|
332 |
\begin{tabular}{rl}
|
|
333 |
\<^bold>\<open>input:\<close> & \<open>command argument\<close> \\
|
|
334 |
immediate \<^bold>\<open>output:\<close> & \<^verbatim>\<open>OK {"task":\<close>\<open>id\<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
|
67918
|
344 |
revealed in the immediate (synchronous) result. Thus the client can
|
|
345 |
invoke further asynchronous commands and still dispatch the resulting stream of
|
67904
|
346 |
asynchronous messages properly.
|
|
347 |
|
|
348 |
The synchronous command \<^verbatim>\<open>cancel\<close>~\<open>id\<close> tells the specified task to terminate
|
67917
|
349 |
prematurely: usually causing a \<^verbatim>\<open>FAILED\<close> result, but this is not guaranteed:
|
67918
|
350 |
the cancel event may come too late or the running process may just ignore
|
|
351 |
it.
|
67917
|
352 |
\<close>
|
|
353 |
|
|
354 |
|
67918
|
355 |
section \<open>Types for JSON values \label{sec:json-types}\<close>
|
67917
|
356 |
|
|
357 |
text \<open>
|
|
358 |
In order to specify concrete JSON types for command arguments and result
|
|
359 |
messages, the following type definition language shall be used:
|
|
360 |
|
|
361 |
\<^rail>\<open>
|
|
362 |
@{syntax type_def}: @'type' @{syntax name} '=' @{syntax type}
|
|
363 |
;
|
|
364 |
@{syntax type}: @{syntax name} | @{syntax value} | 'any' | 'null' |
|
|
365 |
'bool' | 'int' | 'long' | 'double' | 'string' | '[' @{syntax type} ']' |
|
|
366 |
'{' (@{syntax field_type} ',' *) '}' |
|
|
367 |
@{syntax type} '\<oplus>' @{syntax type} |
|
67918
|
368 |
@{syntax type} '|' @{syntax type} |
|
|
369 |
'(' @{syntax type} ')'
|
67917
|
370 |
;
|
|
371 |
@{syntax field_type}: @{syntax name} ('?'?) ':' @{syntax type}
|
|
372 |
\<close>
|
|
373 |
|
67918
|
374 |
This is a simplified variation of TypeScript
|
|
375 |
interfaces.\<^footnote>\<open>\<^url>\<open>https://www.typescriptlang.org/docs/handbook/interfaces.html\<close>\<close>
|
|
376 |
The meaning of these types is specified wrt. the Isabelle/Scala
|
|
377 |
implementation as follows.
|
67917
|
378 |
|
|
379 |
\<^item> A \<open>name\<close> refers to a type defined elsewhere. The environment of type
|
|
380 |
definitions is given informally: put into proper foundational order, it
|
67918
|
381 |
needs to specify a strongly normalizing system of syntactic abbreviations;
|
|
382 |
type definitions may not be recursive.
|
67917
|
383 |
|
|
384 |
\<^item> A \<open>value\<close> in JSON notation represents the singleton type of the given
|
67918
|
385 |
item. For example, the string \<^verbatim>\<open>"error"\<close> can be used as type for a slot that
|
|
386 |
is guaranteed to contain that constant.
|
67917
|
387 |
|
|
388 |
\<^item> Type \<open>any\<close> is the super type of all other types: it is an untyped slot in
|
|
389 |
the specification and corresponds to \<^verbatim>\<open>Any\<close> or \<^verbatim>\<open>JSON.T\<close> in Isabelle/Scala.
|
|
390 |
|
|
391 |
\<^item> Type \<open>null\<close> is the type of the improper value \<open>null\<close>; it corresponds to
|
|
392 |
type \<^verbatim>\<open>Null\<close> in Scala and is normally not used in Isabelle/Scala.\<^footnote>\<open>See also
|
|
393 |
``Null References: The Billion Dollar Mistake'' by Tony Hoare
|
|
394 |
\<^url>\<open>https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare\<close>.\<close>
|
|
395 |
|
67918
|
396 |
\<^item> Type \<open>bool\<close> is the type of the truth values \<^verbatim>\<open>true\<close> and \<^verbatim>\<open>false\<close>; it
|
67917
|
397 |
corresponds to \<^verbatim>\<open>Boolean\<close> in Scala.
|
|
398 |
|
|
399 |
\<^item> Types \<open>int\<close>, \<open>long\<close>, \<open>double\<close> are specific versions of the generic
|
|
400 |
\<open>number\<close> type, corresponding to \<^verbatim>\<open>Int\<close>, \<^verbatim>\<open>Long\<close>, \<^verbatim>\<open>Double\<close> in Scala, but
|
|
401 |
\<^verbatim>\<open>Long\<close> is limited to 53 bit precision.\<^footnote>\<open>Implementations of JSON typically
|
|
402 |
standardize \<open>number\<close> to \<^verbatim>\<open>Double\<close>, which can absorb \<^verbatim>\<open>Int\<close> faithfully, but
|
|
403 |
not all of \<^verbatim>\<open>Long\<close>.\<close>
|
|
404 |
|
|
405 |
\<^item> Type \<open>string\<close> represents Unicode text; it corresponds to type \<^verbatim>\<open>String\<close> in
|
|
406 |
Scala.
|
|
407 |
|
|
408 |
\<^item> Type \<open>[t]\<close> is the array (or list) type over \<open>t\<close>; it corresponds to
|
|
409 |
\<^verbatim>\<open>List[t]\<close> in Scala. The list type is co-variant as usual (i.e.\ monotonic
|
67918
|
410 |
wrt. the subtype relation).
|
67917
|
411 |
|
|
412 |
\<^item> Object types describe the possible content of JSON records, with field
|
|
413 |
names and types. A question mark after a field name means that it is
|
67918
|
414 |
optional. In Scala this could refer to an explicit type \<^verbatim>\<open>Option[t]\<close>, e.g.\
|
|
415 |
\<open>{a: int, b?: string}\<close> corresponding to a Scala case class with arguments
|
|
416 |
\<^verbatim>\<open>a: Int\<close>, \<^verbatim>\<open>b: Option[String]\<close>.
|
67917
|
417 |
|
|
418 |
Alternatively, optional fields can have a default value. If nothing else is
|
67918
|
419 |
specified, a standard ``empty value'' is used for each type, i.e.\ \<^verbatim>\<open>0\<close> for
|
|
420 |
the number types, \<^verbatim>\<open>false\<close> for \<open>bool\<close>, or the empty string, array, object
|
|
421 |
etc.
|
67917
|
422 |
|
|
423 |
Object types are \<^emph>\<open>permissive\<close> in the sense that only the specified field
|
|
424 |
names need to conform to the given types, but unspecified fields may be
|
|
425 |
present as well.
|
|
426 |
|
|
427 |
\<^item> The type expression \<open>t\<^sub>1 \<oplus> t\<^sub>2\<close> only works for two object types with
|
|
428 |
disjoint field names: it is the concatenation of the respective @{syntax
|
|
429 |
field_type} specifications taken together. For example: \<open>{task: string} \<oplus>
|
|
430 |
{ok: bool}\<close> is the equivalent to \<open>{task: string, ok: bool}\<close>.
|
|
431 |
|
|
432 |
\<^item> The type expression \<open>t\<^sub>1 | t\<^sub>2\<close> is the disjoint union of two types, either
|
|
433 |
one of the two cases may occur.
|
|
434 |
|
67918
|
435 |
\<^item> Parentheses \<open>(t)\<close> merely group type expressions syntactically.
|
|
436 |
|
67917
|
437 |
|
|
438 |
These types correspond to JSON values in an obvious manner, which is not
|
|
439 |
further described here. For example, the JSON array \<^verbatim>\<open>[1, 2, 3]\<close> conforms to
|
|
440 |
types \<open>[int]\<close>, \<open>[long]\<close>, \<open>[double]\<close>, \<open>[any]\<close>, \<open>any\<close>.
|
|
441 |
|
|
442 |
Note that JSON objects require field names to be quoted, but the type
|
67918
|
443 |
language omits quotes for clarity. Thus the object \<^verbatim>\<open>{"a": 42, "b": "xyz"}\<close>
|
|
444 |
conforms to the type \<open>{a: int, b: string}\<close>, for example.
|
67917
|
445 |
|
|
446 |
\<^medskip>
|
67918
|
447 |
The absence of an argument or result is represented by the Scala type
|
|
448 |
\<^verbatim>\<open>Unit\<close>: it is written as empty text in the message \<open>argument\<close>
|
67917
|
449 |
(\secref{sec:input-output-messages}). This is not part of the JSON language.
|
|
450 |
|
|
451 |
Server replies have name tags like \<^verbatim>\<open>OK\<close>, \<^verbatim>\<open>ERROR\<close>: these are used literally
|
|
452 |
together with type specifications to indicate the particular name with the
|
|
453 |
type of its argument, e.g.\ \<^verbatim>\<open>OK\<close>~\<open>[string]\<close> for a regular result that is a
|
|
454 |
list (JSON array) of strings.
|
|
455 |
|
|
456 |
\<^bigskip>
|
67918
|
457 |
Here are some common type definitions, for use in particular specifications
|
|
458 |
of command arguments and results.
|
67917
|
459 |
|
|
460 |
\<^item> \<^bold>\<open>type\<close>~\<open>position = {line?: int, offset?: int, end_offset?: int, file?:
|
67918
|
461 |
string, id?: long}\<close> describes a source position within Isabelle text. Only
|
|
462 |
the \<open>line\<close> and \<open>file\<close> fields make immediate sense to external programs.
|
67917
|
463 |
Detailed \<open>offset\<close> and \<open>end_offset\<close> positions are counted according to
|
|
464 |
Isabelle symbols, see @{ML_type Symbol.symbol} in Isabelle/ML @{cite
|
67918
|
465 |
"isabelle-implementation"}. The position \<open>id\<close> belongs to the representation
|
|
466 |
of command transactions in the Isabelle/PIDE protocol: it normally does not
|
|
467 |
occur in externalized positions.
|
67917
|
468 |
|
|
469 |
\<^item> \<^bold>\<open>type\<close>~\<open>message = {kind?: string, message: string, pos?: position}\<close> where
|
|
470 |
the \<open>kind\<close> provides some hint about the role and importance of the message.
|
|
471 |
The main message kinds are \<^verbatim>\<open>writeln\<close> (for regular output), \<^verbatim>\<open>warning\<close>, and
|
|
472 |
\<^verbatim>\<open>error\<close>. The table \<^verbatim>\<open>Markup.messages\<close> in Isabelle/Scala defines further
|
|
473 |
message kinds for more specific applications.
|
|
474 |
|
|
475 |
\<^item> \<^bold>\<open>type\<close>~\<open>error_message = {kind:\<close>~\<^verbatim>\<open>"error"\<close>\<open>, message: string}\<close> refers to
|
|
476 |
error messages in particular. These occur routinely with \<^verbatim>\<open>ERROR\<close> or
|
|
477 |
\<^verbatim>\<open>FAILED\<close> replies, but also as initial command syntax errors (which are
|
|
478 |
omitted in the command specifications below).
|
|
479 |
|
|
480 |
\<^item> \<^bold>\<open>type\<close>~\<open>theory_progress = {kind:\<close>~\<^verbatim>\<open>"writeln"\<close>\<open>, message: string, theory:
|
|
481 |
string, session: string}\<close> reports formal progress in loading theories (e.g.\
|
|
482 |
when building a session image). Apart from a regular output message, it also
|
67918
|
483 |
reveals the formal theory name (e.g.\ \<^verbatim>\<open>"HOL.Nat"\<close>) and session name (e.g.\
|
|
484 |
\<^verbatim>\<open>"HOL"\<close>). Note that some rare theory names lack a proper session prefix,
|
|
485 |
e.g. theory \<^verbatim>\<open>"Main"\<close> in session \<^verbatim>\<open>"HOL"\<close>.
|
67917
|
486 |
|
|
487 |
\<^item> \<^bold>\<open>type\<close>~\<open>timing = {elapsed: double, cpu: double, gc: double}\<close> refers to
|
|
488 |
common Isabelle timing information in seconds, usually with a precision of
|
|
489 |
three digits after the point (whole milliseconds).
|
|
490 |
|
|
491 |
\<^item> \<^bold>\<open>type\<close>~\<open>uuid = string\<close> refers to a Universally Unique Identifier (UUID)
|
|
492 |
as plain text.\<^footnote>\<open>See \<^url>\<open>https://www.ietf.org/rfc/rfc4122.txt\<close> and
|
|
493 |
\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/UUID.html\<close>.\<close> Such
|
|
494 |
identifiers are created as private random numbers of the server and only
|
|
495 |
revealed to the client that creates a certain resource (e.g.\ task or
|
|
496 |
session). A client may disclose this information for use in a different
|
67918
|
497 |
client connection: this allows to share sessions between multiple
|
67917
|
498 |
connections.
|
|
499 |
|
|
500 |
Client commands need to provide syntactically wellformed UUIDs: this is
|
|
501 |
trivial to achieve by using only identifiers that have been produced by the
|
|
502 |
server beforehand.
|
|
503 |
|
|
504 |
\<^item> \<^bold>\<open>type\<close>~\<open>task = {task: uuid}\<close> identifies a newly created asynchronous task
|
|
505 |
and thus allows the client to control it by the \<^verbatim>\<open>cancel\<close> command. The same
|
67918
|
506 |
task identification is included in all messages produced by this task.
|
|
507 |
|
|
508 |
\<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
|
|
509 |
int, warned: int, failed: int, finished: int, consolidated: bool}\<close>
|
|
510 |
represents a formal theory node status of the PIDE document model. Fields
|
|
511 |
\<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> account
|
|
512 |
for individual commands within a theory node; \<open>ok\<close> is an abstraction for
|
|
513 |
\<open>failed = 0\<close>. The \<open>consolidated\<close> flag indicates whether the outermost theory
|
|
514 |
command structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has
|
|
515 |
been checked.
|
|
516 |
\<close>
|
|
517 |
|
|
518 |
|
|
519 |
section \<open>Server commands and results\<close>
|
|
520 |
|
|
521 |
text \<open>
|
|
522 |
Here follows an overview of particular Isabelle server commands with their
|
|
523 |
results, which are usually represented as JSON values with types according
|
|
524 |
to \secref{sec:json-types}. The general format of input and output messages
|
|
525 |
is described in \secref{sec:input-output-messages}. The relevant
|
|
526 |
Isabelle/Scala source files are:
|
|
527 |
|
|
528 |
\<^medskip>
|
|
529 |
\begin{tabular}{l}
|
|
530 |
\<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server_commands.scala\<close> \\
|
|
531 |
\<^file>\<open>$ISABELLE_HOME/src/Pure/Tools/server.scala\<close> \\
|
|
532 |
\<^file>\<open>$ISABELLE_HOME/src/Pure/General/json.scala\<close> \\
|
|
533 |
\end{tabular}
|
67917
|
534 |
\<close>
|
|
535 |
|
|
536 |
|
|
537 |
subsection \<open>Command \<^verbatim>\<open>help\<close>\<close>
|
|
538 |
|
|
539 |
text \<open>
|
|
540 |
\begin{tabular}{ll}
|
|
541 |
regular result: & \<^verbatim>\<open>OK\<close> \<open>[string]\<close> \\
|
|
542 |
\end{tabular}
|
|
543 |
\<^medskip>
|
|
544 |
|
67918
|
545 |
The \<^verbatim>\<open>help\<close> command has no argument and returns the list of server command
|
|
546 |
names. This is occasionally useful for interactive experimentation (see also
|
|
547 |
@{tool client} in \secref{sec:tool-client}).
|
67917
|
548 |
\<close>
|
|
549 |
|
|
550 |
|
|
551 |
subsection \<open>Command \<^verbatim>\<open>echo\<close>\<close>
|
|
552 |
|
|
553 |
text \<open>
|
|
554 |
\begin{tabular}{ll}
|
|
555 |
argument: & \<open>any\<close> \\
|
|
556 |
regular result: & \<^verbatim>\<open>OK\<close> \<open>any\<close> \\
|
|
557 |
\end{tabular}
|
|
558 |
\<^medskip>
|
|
559 |
|
|
560 |
The \<^verbatim>\<open>echo\<close> command is the identity function: it returns its argument as
|
|
561 |
regular result. This is occasionally useful for testing and interactive
|
|
562 |
experimentation (see also @{tool client} in \secref{sec:tool-client}).
|
|
563 |
|
67918
|
564 |
The Scala type of \<^verbatim>\<open>echo\<close> is actually more general than given above:
|
|
565 |
\<^verbatim>\<open>Unit\<close>, \<^verbatim>\<open>XML.Elem\<close>, \<^verbatim>\<open>JSON.T\<close> work uniformly. Note that \<^verbatim>\<open>XML.Elem\<close> might
|
67917
|
566 |
be difficult to type on the console in its YXML syntax
|
|
567 |
(\secref{sec:yxml-vs-xml}).
|
|
568 |
\<close>
|
|
569 |
|
|
570 |
|
|
571 |
subsection \<open>Command \<^verbatim>\<open>shutdown\<close>\<close>
|
|
572 |
|
|
573 |
text \<open>
|
|
574 |
\begin{tabular}{ll}
|
|
575 |
regular result: & \<^verbatim>\<open>OK\<close> \\
|
|
576 |
\end{tabular}
|
|
577 |
\<^medskip>
|
|
578 |
|
|
579 |
The \<^verbatim>\<open>shutdown\<close> command has no argument and result value. It forces a
|
|
580 |
shutdown of the connected server process, stopping all open sessions and
|
|
581 |
closing the server socket. This may disrupt pending commands on other
|
|
582 |
connections!
|
|
583 |
|
|
584 |
\<^medskip>
|
67918
|
585 |
The command-line invocation \<^verbatim>\<open>isabelle server -x\<close> opens a server connection
|
|
586 |
and issues a \<^verbatim>\<open>shutdown\<close> command (see also \secref{sec:tool-server}).
|
67917
|
587 |
\<close>
|
|
588 |
|
|
589 |
|
|
590 |
subsection \<open>Command \<^verbatim>\<open>cancel\<close>\<close>
|
|
591 |
|
|
592 |
text \<open>
|
|
593 |
\begin{tabular}{ll}
|
|
594 |
argument: & \<open>uuid\<close> \\
|
|
595 |
regular result: & \<^verbatim>\<open>OK\<close> \\
|
|
596 |
\end{tabular}
|
|
597 |
\<^medskip>
|
|
598 |
|
67918
|
599 |
The command invocation \<^verbatim>\<open>cancel "\<close>\<open>uuid\<close>\<^verbatim>\<open>"\<close> attempts to cancel the
|
|
600 |
specified task.
|
67917
|
601 |
|
|
602 |
Cancellation is merely a hint that the client prefers an ongoing process to
|
|
603 |
be stopped. The command always succeeds formally, but it may get ignored by
|
67918
|
604 |
a task that is still running; it might also refer to a non-existing or
|
|
605 |
no-longer existing task (without producing an error).
|
67917
|
606 |
|
|
607 |
Successful cancellation typically leads to an asynchronous failure of type
|
67918
|
608 |
\<^verbatim>\<open>FAILED {\<close>\<open>task: uuid, message:\<close>~\<^verbatim>\<open>"Interrupt"}\<close>. A different message is
|
|
609 |
also possible, depending how the task handles the event.
|
67917
|
610 |
\<close>
|
|
611 |
|
|
612 |
|
|
613 |
subsection \<open>Command \<^verbatim>\<open>session_build\<close> \label{sec:command-session-build}\<close>
|
|
614 |
|
|
615 |
text \<open>
|
|
616 |
\begin{tabular}{lll}
|
|
617 |
argument: & \<open>session_build_args\<close> \\
|
|
618 |
immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
|
|
619 |
notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
|
|
620 |
regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_build_results\<close> \\
|
|
621 |
error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_build_results\<close> \\[2ex]
|
|
622 |
\end{tabular}
|
|
623 |
|
|
624 |
\begin{tabular}{lll}
|
|
625 |
\<^bold>\<open>type\<close> \<open>session_build_args =\<close> \\
|
|
626 |
\quad\<open>{session: string,\<close> \\
|
|
627 |
\quad~~\<open>preferences?: string,\<close> & \<^bold>\<open>default:\<close> server preferences \\
|
|
628 |
\quad~~\<open>options?: [string],\<close> \\
|
|
629 |
\quad~~\<open>dirs?: [string],\<close> \\
|
|
630 |
\quad~~\<open>ancestor_session?: string,\<close> \\
|
|
631 |
\quad~~\<open>all_known?: bool,\<close> \\
|
|
632 |
\quad~~\<open>focus_session?: bool,\<close> \\
|
|
633 |
\quad~~\<open>required_session?: bool,\<close> \\
|
|
634 |
\quad~~\<open>system_mode?: bool,\<close> \\
|
|
635 |
\quad~~\<open>verbose?: bool}\<close> \\[2ex]
|
|
636 |
|
|
637 |
\<^bold>\<open>type\<close> \<open>session_build_result =\<close> \\
|
|
638 |
\quad\<open>{session: string,\<close> \\
|
|
639 |
\quad~~\<open>ok: bool,\<close> \\
|
|
640 |
\quad~~\<open>return_code: int,\<close> \\
|
|
641 |
\quad~~\<open>timeout: bool,\<close> \\
|
67918
|
642 |
\quad~~\<open>timing: timing}\<close> \\[2ex]
|
|
643 |
|
|
644 |
\<^bold>\<open>type\<close> \<open>session_build_results =\<close> \\
|
|
645 |
\quad\<open>{ok: bool,\<close> \\
|
|
646 |
\quad~~\<open>return_code: int,\<close> \\
|
|
647 |
\quad~~\<open>sessions: [session_build_result]}\<close> \\
|
67917
|
648 |
\end{tabular}
|
|
649 |
\<close>
|
|
650 |
|
|
651 |
text \<open>
|
67918
|
652 |
The \<^verbatim>\<open>session_build\<close> command prepares a session image for interactive use of
|
|
653 |
theories. This is a limited version of command-line tool @{tool build}
|
|
654 |
(\secref{sec:tool-build}), with specific options to request a formal context
|
|
655 |
for an interactive PIDE session.
|
67917
|
656 |
|
|
657 |
The build process is asynchronous, with notifications that inform about the
|
67918
|
658 |
progress of loaded theories. Some further informative messages are output as
|
|
659 |
well.
|
67917
|
660 |
|
|
661 |
Coordination of independent build processes is at the discretion of the
|
67918
|
662 |
client (or end-user), just as for @{tool build} and @{tool jedit}. There is
|
|
663 |
no built-in coordination of conflicting builds with overlapping hierarchies
|
|
664 |
of session images. In the worst case, a session image produced by one task
|
|
665 |
may get overwritten by another task!
|
67917
|
666 |
\<close>
|
|
667 |
|
|
668 |
|
|
669 |
subsubsection \<open>Arguments\<close>
|
|
670 |
|
|
671 |
text \<open>
|
67918
|
672 |
The \<open>session\<close> field is mandatory. It specifies the target session name:
|
|
673 |
either directly (default) or indirectly (if \<open>required_session\<close> is \<^verbatim>\<open>true\<close>).
|
|
674 |
The build process will produce all required ancestor images for the
|
|
675 |
specified target.
|
67917
|
676 |
|
|
677 |
\<^medskip>
|
|
678 |
The environment of Isabelle system options is determined from \<open>preferences\<close>
|
|
679 |
that are augmented by \<open>options\<close>, which is a list individual updates of the
|
|
680 |
form the \<open>name\<close>\<^verbatim>\<open>=\<close>\<open>value\<close> or \<open>name\<close> (the latter abbreviates
|
|
681 |
\<open>name\<close>\<^verbatim>\<open>=true\<close>); see also command-line option \<^verbatim>\<open>-o\<close> for @{tool build}. The
|
|
682 |
preferences are loaded from the file
|
|
683 |
\<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> by default, but the client may
|
|
684 |
provide alternative contents for it (as text, not a file-name). This could
|
|
685 |
be relevant in situations where client and server run in different
|
|
686 |
operating-system contexts.
|
|
687 |
|
|
688 |
\<^medskip>
|
67918
|
689 |
The \<open>dirs\<close> field specifies additional directories for session ROOT and ROOTS
|
|
690 |
files (\secref{sec:session-root}). This augments the name space of available
|
|
691 |
sessions; see also option \<^verbatim>\<open>-d\<close> in @{tool build}.
|
67917
|
692 |
|
|
693 |
\<^medskip>
|
|
694 |
The \<open>ancestor_session\<close> field specifies an alternative image as starting
|
|
695 |
point for the target image. The default is to use the parent session
|
|
696 |
according to the ROOT entry; see also option \<^verbatim>\<open>-A\<close> in @{tool jedit}. This
|
|
697 |
can lead to a more light-weight build process, by skipping intermediate
|
|
698 |
session images of the hierarchy that are not used later on.
|
|
699 |
|
|
700 |
\<^medskip>
|
67918
|
701 |
The \<open>all_known\<close> field set to \<^verbatim>\<open>true\<close> includes all sessions from reachable
|
|
702 |
ROOT entries into the name space of theories. This is relevant for proper
|
|
703 |
session-qualified names, instead of referring to theory file names. The
|
|
704 |
option enables the \<^verbatim>\<open>use_theories\<close> command
|
67917
|
705 |
(\secref{sec:command-use-theories}) to refer to arbitrary theories from
|
67918
|
706 |
other sessions, but considerable time is required to explore all accessible
|
|
707 |
session directories and theory dependencies.
|
67917
|
708 |
|
|
709 |
\<^medskip>
|
67918
|
710 |
The \<open>focus_session\<close> field set to \<^verbatim>\<open>true\<close> focuses on the target session:
|
67917
|
711 |
the accessible name space of theories is restricted to sessions that are
|
67918
|
712 |
connected to it in the imports graph.
|
67917
|
713 |
|
|
714 |
\<^medskip>
|
|
715 |
The \<open>required_session\<close> field set to \<^verbatim>\<open>true\<close> indicates that the target image
|
|
716 |
should not be the \<open>session\<close>, but its parent (or ancestor according to
|
|
717 |
\<open>ancestor_session\<close>). Thus it prepares a session context where theories from
|
|
718 |
the \<open>session\<close> itself can be loaded.
|
|
719 |
|
|
720 |
\<^medskip>
|
67918
|
721 |
The \<open>system_mode\<close> field set to \<^verbatim>\<open>true\<close> stores resulting session images and
|
67917
|
722 |
log files in @{path "$ISABELLE_HOME/heaps"} instead of the default location
|
|
723 |
@{setting ISABELLE_OUTPUT} (which is normally in @{setting
|
67918
|
724 |
ISABELLE_HOME_USER}). See also option \<^verbatim>\<open>-s\<close> in @{tool build}.
|
67917
|
725 |
|
|
726 |
\<^medskip>
|
67918
|
727 |
The \<open>verbose\<close> field set to \<^verbatim>\<open>true\<close> yields extra verbosity. The effect is
|
67917
|
728 |
similar to option \<^verbatim>\<open>-v\<close> in @{tool build}.
|
|
729 |
\<close>
|
|
730 |
|
|
731 |
|
|
732 |
subsubsection \<open>Intermediate output\<close>
|
|
733 |
|
|
734 |
text \<open>
|
|
735 |
The asynchronous notifications of command \<^verbatim>\<open>session_build\<close> mainly serve as
|
|
736 |
progress indicator: the output resembles that of the session build window of
|
|
737 |
Isabelle/jEdit after startup @{cite "isabelle-jedit"}.
|
|
738 |
|
|
739 |
For the client it is usually sufficient to print the messages in plain text,
|
67918
|
740 |
but note that \<open>theory_progress\<close> also reveals formal \<open>theory\<close> and
|
|
741 |
\<open>session\<close> names directly.
|
67917
|
742 |
\<close>
|
|
743 |
|
|
744 |
|
|
745 |
subsubsection \<open>Results\<close>
|
|
746 |
|
|
747 |
text \<open>
|
67918
|
748 |
The overall \<open>session_build_results\<close> contain both a summary and an entry
|
|
749 |
\<open>session_build_result\<close> for each session in the build hierarchy. The result
|
|
750 |
is always provided, independently of overall success (\<^verbatim>\<open>FINISHED\<close> task) or
|
|
751 |
failure (\<^verbatim>\<open>FAILED\<close> task).
|
67917
|
752 |
|
|
753 |
The \<open>ok\<close> field tells abstractly, whether all required session builds came
|
67918
|
754 |
out as \<open>ok\<close>, i.e.\ with zero \<open>return_code\<close>. A non-zero \<open>return_code\<close>
|
|
755 |
indicates an error according to usual POSIX conventions for process exit.
|
|
756 |
|
|
757 |
The individual \<open>session_build_result\<close> entries provide extra fields:
|
67917
|
758 |
|
67918
|
759 |
\<^item> \<open>timeout\<close> tells if the build process was aborted after running too long,
|
|
760 |
|
|
761 |
\<^item> \<open>timing\<close> gives the overall process timing in the usual Isabelle format
|
|
762 |
with elapsed, CPU, GC time.
|
67917
|
763 |
\<close>
|
|
764 |
|
|
765 |
|
|
766 |
subsubsection \<open>Examples\<close>
|
|
767 |
|
|
768 |
text \<open>
|
|
769 |
Build of a session image from the Isabelle distribution:
|
|
770 |
@{verbatim [display] \<open>session_build {"session": "HOL-Word"}\<close>}
|
|
771 |
|
|
772 |
Build a session image from the Archive of Formal Proofs:
|
|
773 |
@{verbatim [display] \<open>session_build {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
|
|
774 |
|
|
775 |
Build of a session image of \<^verbatim>\<open>HOL-Number_Theory\<close> directly on top of \<^verbatim>\<open>HOL\<close>:
|
|
776 |
@{verbatim [display] \<open>session_build {"session": "HOL-Number_Theory", "ancestor_session": "HOL"}\<close>}
|
|
777 |
\<close>
|
|
778 |
|
|
779 |
|
|
780 |
subsection \<open>Command \<^verbatim>\<open>session_start\<close> \label{sec:command-session-start}\<close>
|
|
781 |
|
|
782 |
text \<open>
|
|
783 |
\begin{tabular}{lll}
|
|
784 |
argument: & \<open>session_build_args \<oplus> {print_mode?: [string]}\<close> \\
|
|
785 |
immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
|
|
786 |
notifications: & \<^verbatim>\<open>NOTE\<close> \<open>task \<oplus> (theory_progress | message)\<close> \\
|
|
787 |
regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_start_result\<close> \\
|
|
788 |
error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message\<close> \\[2ex]
|
|
789 |
\end{tabular}
|
|
790 |
|
|
791 |
\begin{tabular}{l}
|
|
792 |
\<^bold>\<open>type\<close> \<open>session_start_result = {session: string, session_id: uuid}\<close>
|
|
793 |
\end{tabular}
|
|
794 |
|
|
795 |
\<^medskip>
|
|
796 |
The \<^verbatim>\<open>session_start\<close> command starts a new Isabelle/PIDE session with
|
|
797 |
underlying Isabelle/ML process, based on a session image that it produces on
|
67918
|
798 |
demand using \<^verbatim>\<open>session_build\<close>. Thus it accepts all \<open>session_build_args\<close> and
|
|
799 |
produces similar notifications, but the detailed \<open>session_build_results\<close> are
|
|
800 |
omitted.
|
67917
|
801 |
|
|
802 |
The session build and startup process is asynchronous: when the task is
|
67918
|
803 |
finished, the session remains active for commands, until a \<^verbatim>\<open>session_stop\<close>
|
|
804 |
or \<^verbatim>\<open>shutdown\<close> command is sent to the server.
|
67917
|
805 |
|
|
806 |
Sessions are independent of client connections: it is possible to start a
|
|
807 |
session and later apply \<^verbatim>\<open>use_theories\<close> on different connections, as long as
|
67918
|
808 |
the internal session identifier is known: shared theory imports will be used
|
|
809 |
only once (and persist until purged explicitly).
|
67917
|
810 |
\<close>
|
|
811 |
|
|
812 |
|
|
813 |
subsubsection \<open>Arguments\<close>
|
|
814 |
|
|
815 |
text \<open>
|
67918
|
816 |
Most arguments are shared with \<^verbatim>\<open>session_build\<close>
|
67917
|
817 |
(\secref{sec:command-session-build}).
|
|
818 |
|
|
819 |
\<^medskip>
|
|
820 |
The \<open>print_mode\<close> field adds identifiers of print modes to be made active for
|
|
821 |
this session. For example, \<^verbatim>\<open>"print_mode": ["ASCII"]\<close> prefers ASCII
|
|
822 |
replacement syntax over mathematical Isabelle symbols. See also option \<^verbatim>\<open>-m\<close>
|
|
823 |
in @{tool process} (\secref{sec:tool-process}).
|
|
824 |
\<close>
|
|
825 |
|
|
826 |
|
|
827 |
subsubsection \<open>Results\<close>
|
|
828 |
|
|
829 |
text \<open>
|
|
830 |
The \<open>session\<close> field provides the active session name for clarity.
|
|
831 |
|
|
832 |
\<^medskip>
|
|
833 |
The \<open>session_id\<close> field provides the internal identification of the session
|
|
834 |
object within the sever process. It can remain active as long as the server
|
|
835 |
is running, independently of the current client connection.
|
|
836 |
\<close>
|
|
837 |
|
|
838 |
|
|
839 |
subsection \<open>Examples\<close>
|
|
840 |
|
|
841 |
text \<open>
|
|
842 |
Start a default Isabelle/HOL session:
|
|
843 |
@{verbatim [display] \<open>session_start {"session": "HOL"}\<close>}
|
67918
|
844 |
|
|
845 |
Start a session from the Archive of Formal Proofs:
|
|
846 |
@{verbatim [display] \<open>session_start {"session": "Coinductive", "dirs": ["$AFP_BASE/thys"]}\<close>}
|
67917
|
847 |
\<close>
|
|
848 |
|
|
849 |
|
|
850 |
subsection \<open>Command \<^verbatim>\<open>session_stop\<close>\<close>
|
|
851 |
|
|
852 |
text \<open>
|
|
853 |
\begin{tabular}{ll}
|
|
854 |
argument: & \<open>{session_id?: uuid}\<close> \\
|
|
855 |
immediate result: & \<^verbatim>\<open>OK\<close> \<open>task\<close> \\
|
|
856 |
regular result: & \<^verbatim>\<open>FINISHED\<close> \<open>task \<oplus> session_stop_result\<close> \\
|
|
857 |
error result: & \<^verbatim>\<open>FAILED\<close> \<open>task \<oplus> error_message \<oplus> session_stop_result\<close> \\[2ex]
|
|
858 |
\end{tabular}
|
|
859 |
|
|
860 |
\begin{tabular}{l}
|
|
861 |
\<^bold>\<open>type\<close> \<open>session_stop_result = {ok: bool, return_code: int}\<close>
|
|
862 |
\end{tabular}
|
|
863 |
|
|
864 |
\<^medskip>
|
67918
|
865 |
The \<^verbatim>\<open>session_stop\<close> command forces a shutdown of the identified PIDE
|
|
866 |
session. This asynchronous tasks usually finishes quickly. Failure only
|
|
867 |
happens in unusual situations, according to the return code of the
|
67917
|
868 |
underlying Isabelle/ML process.
|
|
869 |
\<close>
|
|
870 |
|
|
871 |
|
|
872 |
subsubsection \<open>Arguments\<close>
|
|
873 |
|
|
874 |
text \<open>
|
67918
|
875 |
The \<open>session_id\<close> field provides the UUID originally created by the server
|
|
876 |
for this session.
|
67917
|
877 |
\<close>
|
|
878 |
|
|
879 |
|
|
880 |
subsubsection \<open>Results\<close>
|
|
881 |
|
|
882 |
text \<open>
|
67918
|
883 |
The \<open>ok\<close> field tells abstractly, whether the Isabelle/ML process has
|
|
884 |
terminated properly.
|
|
885 |
|
|
886 |
The \<open>return_code\<close> field expresses this information according to usual POSIX
|
|
887 |
conventions for process exit.
|
67917
|
888 |
\<close>
|
|
889 |
|
|
890 |
|
|
891 |
subsection \<open>Command \<^verbatim>\<open>use_theories\<close> \label{sec:command-use-theories}\<close>
|
|
892 |
|
|
893 |
text \<open>
|
|
894 |
\begin{tabular}{ll}
|
|
895 |
argument: & \<open>use_theories_arguments\<close> \\
|
|
896 |
regular result: & \<^verbatim>\<open>OK\<close> \<open>use_theories_results\<close> \\
|
|
897 |
\end{tabular}
|
|
898 |
|
|
899 |
\begin{tabular}{ll}
|
|
900 |
\<^bold>\<open>type\<close> \<open>theory_name = string | {name: string, pos: position}\<close> \\
|
|
901 |
\end{tabular}
|
|
902 |
|
|
903 |
\begin{tabular}{ll}
|
|
904 |
\<^bold>\<open>type\<close> \<open>use_theories_arguments =\<close> \\
|
|
905 |
\quad\<open>{session_id: uuid,\<close> \\
|
|
906 |
\quad~~\<open>theories: [theory_name],\<close> \\
|
|
907 |
\quad~~\<open>qualifier?: string,\<close> \\
|
|
908 |
\quad~~\<open>master_dir?: string,\<close> \\
|
|
909 |
\quad~~\<open>pretty_margin?: double\<close> & \<^bold>\<open>default:\<close> \<^verbatim>\<open>76\<close> \\
|
|
910 |
\quad~~\<open>unicode_symbols?: bool}\<close> \\[2ex]
|
67918
|
911 |
\end{tabular}
|
67917
|
912 |
|
67918
|
913 |
\begin{tabular}{ll}
|
67917
|
914 |
\<^bold>\<open>type\<close> \<open>node_result =\<close> \\
|
|
915 |
\quad\<open>{node_name: string,\<close> \\
|
|
916 |
\quad~~\<open>theory: string,\<close> \\
|
|
917 |
\quad~~\<open>status: node_status,\<close> \\
|
|
918 |
\quad~~\<open>messages: [message]}\<close> \\[2ex]
|
|
919 |
|
|
920 |
\<^bold>\<open>type\<close> \<open>use_theories_results =\<close> \\
|
|
921 |
\quad\<open>{ok: bool,\<close> \\
|
|
922 |
\quad~~\<open>errors: [message],\<close> \\
|
|
923 |
\quad~~\<open>nodes: [node_result]}\<close> \\[2ex]
|
|
924 |
\end{tabular}
|
|
925 |
|
|
926 |
\<^medskip>
|
67918
|
927 |
The \<^verbatim>\<open>use_theories\<close> command updates the identified session by adding the
|
|
928 |
current version of theory files to it, while dependencies are resolved
|
|
929 |
implicitly. The command succeeds eventually, when all theories have been
|
|
930 |
\<^emph>\<open>consolidated\<close> in the sense the formal \<open>node_status\<close>
|
|
931 |
(\secref{sec:json-types}): the outermost command structure has finished (or
|
|
932 |
failed) and the final \<^theory_text>\<open>end\<close> command of each theory has been checked.
|
67917
|
933 |
|
67918
|
934 |
Already used theories persist in the session until purged explicitly. This
|
|
935 |
also means that repeated invocations of \<^verbatim>\<open>use_theories\<close> are idempotent: it
|
|
936 |
could make sense to do that with different values for \<open>pretty_margin\<close> or
|
|
937 |
\<open>unicode_symbols\<close> to get different formatting for \<open>errors\<close> or \<open>messages\<close>.
|
67917
|
938 |
\<close>
|
|
939 |
|
|
940 |
|
|
941 |
subsubsection \<open>Arguments\<close>
|
|
942 |
|
|
943 |
text \<open>
|
|
944 |
The \<open>session_id\<close> is the identifier provided by the server, when the session
|
|
945 |
was created (possibly on a different client connection).
|
|
946 |
|
|
947 |
\<^medskip>
|
67918
|
948 |
The \<open>theories\<close> field specifies theory names as in theory \<^theory_text>\<open>imports\<close> or in
|
|
949 |
ROOT \<^bold>\<open>theories\<close>. An explicit source position for these theory name
|
|
950 |
specifications may be given, which is occasionally useful for precise error
|
|
951 |
locations.
|
67917
|
952 |
|
|
953 |
\<^medskip>
|
|
954 |
The \<open>qualifier\<close> field provides an alternative session qualifier for theories
|
|
955 |
that are not formally recognized as a member of a particular session. The
|
|
956 |
default is \<^verbatim>\<open>Draft\<close> as in Isabelle/jEdit. There is rarely a need to change
|
|
957 |
that, as theory nodes are already uniquely identified by their physical
|
67918
|
958 |
file-system location. This already allows reuse of theory base names with
|
|
959 |
the same session qualifier --- as long as these theories are not used
|
|
960 |
together (e.g.\ in \<^theory_text>\<open>imports\<close>).
|
67917
|
961 |
|
67918
|
962 |
\<^medskip> The \<open>master_dir\<close> field explicit specifies the formal master directory of
|
|
963 |
the imported theory. Normally this is determined implicitly from the parent
|
|
964 |
directory of the theory file.
|
67917
|
965 |
|
|
966 |
\<^medskip>
|
|
967 |
The \<open>pretty_margin\<close> field specifies the line width for pretty-printing. The
|
67918
|
968 |
default is suitable for classic console output. Formatting happens at the
|
|
969 |
end of \<^verbatim>\<open>use_theories\<close>, when all prover messages are exported to the client.
|
67917
|
970 |
|
|
971 |
\<^medskip>
|
67918
|
972 |
The \<open>unicode_symbols\<close> field set to \<^verbatim>\<open>true\<close> renders message output for direct
|
|
973 |
output on a Unicode capable channel, ideally with the Isabelle fonts as in
|
|
974 |
Isabelle/jEdit. The default is to keep the symbolic representation of
|
|
975 |
Isabelle text, e.g.\ \<^verbatim>\<open>\<forall>\<close> instead of its rendering as \<open>\<forall>\<close>. This means the
|
|
976 |
client needs to perform its own rendering before presenting it to the
|
|
977 |
end-user.
|
67917
|
978 |
\<close>
|
|
979 |
|
67918
|
980 |
|
67917
|
981 |
subsubsection \<open>Results\<close>
|
|
982 |
|
|
983 |
text \<open>
|
|
984 |
The \<open>ok\<close> field indicates overall success of processing the specified
|
|
985 |
theories with all their dependencies.
|
|
986 |
|
67918
|
987 |
When \<open>ok\<close> is \<^verbatim>\<open>false\<close>, the \<open>errors\<close> field lists all errors cumulatively
|
|
988 |
(including imported theories). The messages contain position information for
|
|
989 |
the original theory nodes.
|
67917
|
990 |
|
|
991 |
\<^medskip>
|
67918
|
992 |
The \<open>nodes\<close> field provides detailed information about each imported theory
|
|
993 |
node. The individual fields are as follows:
|
67917
|
994 |
|
|
995 |
\<^item> \<open>node_name\<close>: the physical name for the theory node, based on its
|
67918
|
996 |
file-system location;
|
67917
|
997 |
|
67918
|
998 |
\<^item> \<open>theory\<close>: the logical theory name, e.g.\ \<^verbatim>\<open>HOL-Library.AList\<close>;
|
67917
|
999 |
|
|
1000 |
\<^item> \<open>status\<close>: the overall node status, e.g.\ see the visualization in the
|
|
1001 |
\<open>Theories\<close> panel of Isabelle/jEdit @{cite "isabelle-jedit"};
|
|
1002 |
|
67918
|
1003 |
\<^item> \<open>messages\<close>: the main bulk of prover messages produced in this theory
|
67917
|
1004 |
(\<^verbatim>\<open>writeln\<close>, \<^verbatim>\<open>warning\<close>, \<^verbatim>\<open>error\<close>, etc.).
|
|
1005 |
\<close>
|
|
1006 |
|
|
1007 |
|
|
1008 |
subsubsection \<open>Examples\<close>
|
|
1009 |
|
|
1010 |
text \<open>
|
|
1011 |
Process some example theory from the Isabelle distribution, within the
|
|
1012 |
context of an already started session for Isabelle/HOL (see also
|
|
1013 |
\secref{sec:command-session-start}):
|
|
1014 |
@{verbatim [display] \<open>use_theories {"session_id": ..., "theories": ["~~/src/HOL/Isar_Examples/Drinker"]}\<close>}
|
|
1015 |
|
|
1016 |
\<^medskip>
|
|
1017 |
Process some example theories that import other theories via
|
|
1018 |
session-qualified theory names:
|
|
1019 |
|
|
1020 |
@{verbatim [display] \<open>session_start {"session": "HOL", "all_known": true}
|
|
1021 |
use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
|
|
1022 |
session_stop {"session_id": ...}\<close>}
|
|
1023 |
|
|
1024 |
The option \<open>all_known\<close> has been used here to the full name space of
|
|
1025 |
session-qualified theory names accessible in this session. This is also the
|
|
1026 |
default in Isabelle/jEdit, although it requires significant startup time.
|
|
1027 |
|
|
1028 |
\<^medskip>
|
|
1029 |
Process some example theories in the context of their (single) parent
|
|
1030 |
session:
|
|
1031 |
|
|
1032 |
@{verbatim [display] \<open>session_start {"session": "HOL-Library"}
|
|
1033 |
use_theories {"session_id": ..., "theories": ["~~/src/HOL/Unix/Unix"]}
|
|
1034 |
session_stop {"session_id": ...}\<close>}
|
67904
|
1035 |
\<close>
|
|
1036 |
|
|
1037 |
end
|