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, 75 insertions, 0 deletions

diff --git a/Source/DafnyServer/DafnyServer.csproj b/Source/DafnyServer/DafnyServer.csproj
new file mode 100644
index 00000000..0aac88b2
--- /dev/null
+++ b/Source/DafnyServer/DafnyServer.csproj
@@ -0,0 +1,75 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProjectGuid>{AC9B21AE-EBC1-4A27-AD11-ED031FC7B4A2}</ProjectGuid>

+    <OutputType>Exe</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>DafnyServer</RootNamespace>

+    <AssemblyName>DafnyServer</AssemblyName>

+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <StartupObject>Microsoft.Dafny.Server</StartupObject>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <PlatformTarget>AnyCPU</PlatformTarget>

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="Core">

+      <HintPath>..\..\..\boogie\Binaries\Core.dll</HintPath>

+    </Reference>

+    <Reference Include="ExecutionEngine">

+      <HintPath>..\..\..\boogie\Binaries\ExecutionEngine.dll</HintPath>

+    </Reference>

+    <Reference Include="ParserHelper">

+      <HintPath>..\..\..\boogie\Binaries\ParserHelper.dll</HintPath>

+    </Reference>

+    <Reference Include="Provers.SMTLib">

+      <HintPath>..\..\..\boogie\Binaries\Provers.SMTLib.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Runtime.Serialization" />

+    <Reference Include="System.Xml.Linq" />

+    <Reference Include="Microsoft.CSharp" />

+    <Reference Include="DafnyPipeline">

+      <HintPath>..\..\Binaries\DafnyPipeline.dll</HintPath>

+    </Reference>

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="Properties\AssemblyInfo.cs" />

+    <Compile Include="Server.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <None Include="App.config" />

+    <None Include="DafnyPrelude.bpl">

+      <CopyToOutputDirectory>PreserveNewest</CopyToOutputDirectory>

+    </None>

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>