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
   <base64 encoded JSON payload>
   [[DAFNY-CLIENT: EOM]]

Responses are of the following form:
   <list of errors and usual output, as produced by the Dafny CLI>
   [SUCCESS] [[DAFNY-SERVER: EOM]]
or
   <error message>
   [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.

1 files changed, 36 insertions, 0 deletions

diff --git a/Source/DafnyServer/Properties/AssemblyInfo.cs b/Source/DafnyServer/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..5b996543
--- /dev/null
+++ b/Source/DafnyServer/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("Dafny Server")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("Microsoft Research")]

+[assembly: AssemblyProduct("Dafny Server")]

+[assembly: AssemblyCopyright("Copyright ©  2015")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("44d9c1c1-773b-47c1-b876-2de17e70152e")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]