From e93d4804f9d99150079728572c00a518af20a7c5 Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 30 Jul 2015 12:04:16 -0700 Subject: Implement a Dafny server. The Dafny server is a command line utility that allows non-.Net editors to take advantage of Dafny's caching facilities, as used by the Dafny extension for Visual Studio. The server is essentially a REPL, which produces output in the same format as the Dafny CLI; clients thus do not need to understand the internals of Dafny's caching. A typical editing session proceeds as follows: * When a new Dafny file is opened, the editor starts a new instance of the Dafny server. The cache is blank at that point. * The editor sends a copy of the buffer for initial verification. This takes some time, after which the server returns a list of errors. * The user makes modifications; the editor periodically sends a new copy of the buffer's contents to the Dafny server, which quickly returns an updated list of errors. The client-server protocol is sequential, uses JSON, and works over ASCII pipes by base64-encoding queries. It defines one type of query, and two types of responses: Queries are of the following form: verify [[DAFNY-CLIENT: EOM]] Responses are of the following form: [SUCCESS] [[DAFNY-SERVER: EOM]] or [FAILURE] [[DAFNY-SERVER: EOM]] The JSON payload is an array with 4 fields: * args: An array of Dafny arguments, as passed to the Dafny CLI * source: A Dafny program, or the path to a Dafny source file. * sourceIsFile: A boolean indicating whether the 'source' argument is a Dafny program or the path to one. * filename: The name of the original source file, to be used in error messages For small files, embedding the Dafny source directly into a message is convenient; for larger files, however, it is generally better for performance to write the source snapshot to a separate file, and to pass that to Dafny by setting the 'sourceIsFile' flag to true. --- Source/DafnyServer/App.config | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 Source/DafnyServer/App.config (limited to 'Source/DafnyServer/App.config') diff --git a/Source/DafnyServer/App.config b/Source/DafnyServer/App.config new file mode 100644 index 00000000..fad249e4 --- /dev/null +++ b/Source/DafnyServer/App.config @@ -0,0 +1,6 @@ + + + + + + \ No newline at end of file -- cgit v1.2.3