How to install and build the sources

After downloading the sources via the "Source Code" tab, check to make sure you have any External Dependencies that you need. Then use the following directions for the program(s) you want to build. Some of them have extra dependencies. Note:
  • Some users have reported problems when working under cygwin due to unexpected access permissions and file ownership; we strongly recommend using the Visual Studio 2008 Command Prompt.
  • The build process seems to work more smoothly if you start the build steps from the command line rather than Visual Studio.

Boogie

  1. To build Boogie: start by navigating to the Boogie/Source directory. Then either open Boogie.sln in Visual Studio and build the Debug configuration, or else from a command prompt type devenv Boogie.sln /build Debug. After building you should run the Boogie unit tests (see here) and driver test suite (See here).
  2. (Optional Step) If you want to change the parser, then you need to modify the grammar file (Source/Core/BoogiePL.atg) and run Coco/R. In order to do that, you will first need to get the "frame files" which Coco uses as input. Those are located on the Boogie Partners site.

BCT (Bytecode Translator)

  1. Currently, this can be installed and built completely separately from the rest of Boogie. If you do not have the rest of the Boogie sources installed, then install the Boogie binaries from the Downloads tab and copy them into the BCT/Imported/Boogie directory. If you have installed the Boogie sources and built them, you can either copy them from the Binaries directory there, or else change the references from the BytecodeTranslator project to point to the Boogie/Binaries directory.
  2. Install the sources for the CCI Code and Ast Components project. The recommended structure is to put the project in a directory CCICodePlex/Ast.
  3. The project references to the CCI projects assume that the CCICodePlex directory is a sibling to the parent of the BCT directory. If this is not the case, then the project references to the CCI projects will appear unavailable in Visual Studio. You can remove them from the solution and add the following existing projects from wherever you installed the CCI sources. (You will also have to re-add them as external references to the BytecodeTranslator project.)
    1. CCIROOT/Ast/Sources/CodeModel/CodeModel.csproj
    2. CCIROOT/Ast/Sources/ILToCodeModel/ILToCodeModel.csproj
    3. CCIROOT/Ast/Metadata/Sources/MetadataHelper/MetadataHelper.csproj
    4. CCIROOT/Ast/Metadata/Sources/MetadataModel/MetadataModel.csproj
    5. CCIROOT/Ast/Sources/MutableCodeModel/MutableCodeModel.csproj
    6. CCIROOT/Ast/Metadata/Sources/MutableMetadataModel/MutableMetadataModel.csproj
    7. CCIROOT/Ast/Metadata/Sources/PdbReader/PdbReader.csproj
    8. CCIROOT/Ast/Metadata/Sources/PeReader/PeReader.csproj
    9. CCIROOT/Ast/Metadata/Sources/SourceModel/SourceModel.csproj
  4. Build the Debug configuration. If it doesn’t succeed, let us know!

Visual Studio integration

You can edit Dafny and Chalice programs inside Microsoft Visual Studio 2010. This gives you syntax highlighting and runs the verifier in the background, producing red squigglies for errors. To install this mode, you need to build it, which is done in Visual Studio 2010.
  1. Install the Visual Studio 2010 SDK (or the Visual Studio 2010 SP1 SDK if you use Visual Studio 2010 SP1).
  2. Open Util/VS2010/Dafny/DafnyLanguageService.sln (or the analogous .sln file for Chalice in a parallel directory) in Visual Studio 2010.
  3. Build the project, which should report "Succeeded". Quit Visual Studio. Now, the Dafny (or Chalice) mode is available in the experimental instance of Visual Studio 2010. This experimental instance is part of the VS 2010 SDK you just installed.
  4. The integration calls out to Dafny (or Chalice) in a primitive fashion, namely by invoking c:\tmp\StartDafny.bat. This path is currently hard coded, so create a directory c:\tmp and copy into it the file Util/VS2010/Dafny/StartDafny.bat.
  5. Finally, open the experimental instance of Visual Studio 2010 and open any file with the .dfy (or .chalice) extension. You start it from Start -> All programs -> Microsoft Visual Studio 2010 SDK -> Tools. (You may want to right-click on it and select Pin To Start Menu for easy access.)

There is currently no project support for Dafny and Chalice programs, so if you want to add extra command-line options to the verifier, you have to do that by changing the batch file. Another limitation is that you have to create new .dfy files outside Visual Studio (you can then open them and edit them and save them inside Visual Studio, but you can't do the initial creation from inside Visual Studio, because then Visual Studio wants to append .txt to the end of the filename you're trying to create).

Last edited Nov 17, 2014 at 9:23 PM by danliew, version 27

Comments

No comments yet.