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/Properties/AssemblyInfo.cs | 36 +++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 Source/DafnyServer/Properties/AssemblyInfo.cs (limited to 'Source/DafnyServer/Properties/AssemblyInfo.cs') 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")] -- cgit v1.2.3