Skip to content

INSTALL

Jump to bottom
Bryan Parno edited this page Mar 30, 2022 · 98 revisions

This page has instructions for installing Dafny:

Using an IDE

The easiest way to get started with Dafny is using the Dafny IDEs, since they continuously run the verifier in the background. Be sure to check out the Dafny tutorial!

For most users, we recommend using Dafny with VS Code, which has an easy installation, as explained next:

Visual Studio Code

  1. Install Visual Studio Code
  2. If you are on a Mac or Linux, install .NET 6.0, as described under those platforms below.
  3. In Visual Studio Code, press Ctrl+P (or ⌘P on a Mac), and enter ext install dafny-lang.ide-vscode.
  4. If you open a .dfy file, Dafny VSCode will offer to download and install the latest Dafny. You can also browse extensions: vs-code-dafny-2 0 1-install

Emacs

The README at https://github.com/boogie-org/boogie-friends has plenty of information on how to set-up Emacs to work with Dafny. In short, it boils down to running [M-x package-install RET boogie-friends RET] and adding the following to your .emacs:

(setq flycheck-dafny-executable "[path to dafny]/dafny/Scripts/dafny")

Do look at the README, though! It's full of useful tips.

Install the binaries

The following instructions tell you how to install Dafny so that you can run it from various operating systems or as a command-line tool.

If you wish to compile to target languages other than .NET, see the instructions in a subsequent section to install the correct dependencies for the desired language.

Windows (Binary)

To install Dafny on your own machine,

  • Install (if not already present) .NET Core 6.0: https://dotnet.microsoft.com/download/dotnet/6.0
  • download the windows zip file from the releases page and save it to your disk.
  • Then, before you open or unzip it, right-click on it and select Properties; at the bottom of the dialog, click the Unblock button and then the OK button.
  • Now, open the zip file and copy its contents into a directory on your machine. (You can now delete the zip file.)

Then:

  • To run Dafny from the command line, simply run Dafny.exe.

Linux (Binary)

To install a binary installation of dafny on Linux (e.g., Ubuntu), do the following:

  • Install .NET 6.0. See: https://docs.microsoft.com/dotnet/core/install/linux or sudo apt install dotnet-sdk-6.0
  • Install the Linux binary version of Dafny, from https://github.com/dafny-lang/dafny/releases/latest
  • Unzip the downloaded file in a (empty) location of your choice

Within the unzipped Linux distribution, the dafny executable is dafny/dafny

If you intend to use the Dafny compiler, install the appropriate tools as described here

After the compiler dependencies are installed, you can run a quick test of the installation by running the script $INSTALL/dafny/quicktest.sh

Mac (Binary)

To install a binary installation of dafny on Mac OS, do the following:

  • Install .NET 6.0: brew install dotnet-sdk or from https://docs.microsoft.com/dotnet/core/install/macos
  • Install the Mac binary version of Dafny, from https://github.com/dafny-lang/dafny/releases/latest
  • Unzip the downloaded file in a (empty) location of your choice ($INSTALL)
  • cd into the installation directory ($INSTALL/dafny) and run xattr -d com.apple.quarantine *.dylib dafny DafnyServer *.dll z3/bin/z3 or, more easily, run the script $INSTALL/dafny/allow_on_mac.sh

Alternatively, you can use Homebrew to install Dafny: brew install dafny though this version can lag the release on the Dafny github releases page

Within the unzipped Mac distribution, the dafny executable is dafny/dafny

If you intend to use the Dafny compiler, install the appropriate tools as described here.

After the compiler dependencies are installed, you can run a quick test of the installation by running the script $INSTALL/dafny/quicktest.sh

Building (and developing) from source code

If you want access to the very latest Dafny developments or you want to extend Dafny yourself, install the source code, as explained here.

Note that the Dafny integration tests are mainly written using the syntax defined by the LLVM Integrated Tester (LIT) tool, but are actually run using a custom xUnit adaptor in the IntegrationTests package. The configuration files for LIT are still temporarily present in the Test directory and therefore LIT is still likely to work, but its use is deprecated and will not be supported in the future. See here for more details.

Windows (Source)

First, install the following external dependencies:

Second, clone the Dafny source code.

git clone https://github.com/dafny-lang/dafny --recurse-submodules

Third, build the Dafny project, either on the command line: dotnet build dafny\Source\Dafny.sln or open Visual Studio, and open dafny/Source/Dafny.sln, and click on Build > Build solution while the project Dafny Runtime is still the startup project (in bold)

To run Dafny on a particular file, or to run the tests, you'll have to install a prover such as CVC4 or z3. For z3, do the following:

  1. Go to the release of version 4.8.5, download the zip according to your system
  2. Unzip the content of the Z3 folder into dafny\Binaries\z3 so that dafny\Binaries\z3\bin\z3.exe exists.
  3. (optional, depending on configuration) Make sure the dafny\Binaries\z3\bin folder is accessible from the command line by updating the PATH environment variable.

To run Dafny on a particular file:

  • Right-click the project DafnyDriver, and set as startup project
  • Click Debug > DafnyDriver Debug properties...
  • In the textarea "Application arguments", write the path to the file you would like to run Dafny on, e.g. "..\..\Test.dfy" with the double quotes, if the file Test.dfy is next to the dafny folder, and save
  • Now, press F5 to compile Dafny and run it on the specified file.

To run the integration tests, go to dafny/Source/IntegrationTests and run dotnet test -v:n. Make sure you install all the dependencies to compile Dafny to other languages and run them.

Linux (Source)

  1. Dependencies:

    • Install .NET 6.0 as described above
    • Install python3: e.g., sudo apt install python3 python3-pip
    • If you intend to compile to Java, install Java and gradle

  2. Download and build Dafny:

    git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
cd dafny
make exe
pip3 install pre-commit
pre-commit install

If you had any pre-commit scripts before, follow these steps to keep them.

  1. Install Z3 version 4.8.5 (not the most recent version of Z3)

    `make z3-ubuntu`

    OR

    cd dafny/Binaries
wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-ubuntu-16.04.zip
unzip z3-4.8.5-x64-ubuntu-16.04.zip
mv z3-4.8.5-x64-ubuntu-16.04 z3

  2. Install the compiler dependences as described here.

  3. Run Dafny using the dafny shell script in the Scripts directory: dafny/Scripts/dafny You can run a quick test of the installation by executing dafny/Scripts/quicktest.sh

  4. To execute the integration tests: cd dafny/Source/IntegrationTests; dotnet test -v:n. Make sure you install all the dependencies to compile Dafny to other languages and run them. The tests take a while, depending on your machine, but emit progress output.

Mac (Source)

  1. Dependencies:

    • Install .NET (6.0): brew install dotnet-sdk
    • [python3 and pip3 are needed but they are likely already part of the Mac installation]
    • (Optional) Install java (possibly use brew install openjdk@8)
    • (Optional) Install gradle (possibly use brew install gradle)

  2. Download and build Dafny:

    git clone https://github.com/dafny-lang/dafny.git --recurse-submodules
cd dafny
brew install pre-commit
pre-commit install
make exe

If you had any pre-commit scripts before, follow these steps to keep them.

  1. Download and unpack Z3 (Dafny looks for z3 in Binaries/z3/bin/) version 4.8.5 (note, this is not the latest version of Z3). You can use

    brew install wget
make z3-mac

or

   cd dafny/Binaries
   wget https://github.com/Z3Prover/z3/releases/download/Z3-4.8.5/z3-4.8.5-x64-osx-10.14.2.zip
   unzip z3-4.8.5-x64-osx-10.14.2.zip
   mv z3-4.8.5-x64-osx-10.14.2 z3

  1. Install the compiler dependences as described here.

  2. Run Dafny using the dafny shell script in the Scripts directory: dafny/Scripts/dafny You can run a quick test of the installation by executing dafny/Scripts/quicktest.sh

  3. To execute the integration tests: cd dafny/Source/IntegrationTests; dotnet test -v:n. Make sure you install all the dependencies to compile Dafny to other languages and run them. The tests take a while, depending on your machine, but emit progress output.

Keeping existing pre-commit hooks when building from source

If you install pre-commit, it will rename any existing pre-commit hook (./git/hooks/pre-commit) to a file namepre-commit.legacy, and put a python script named pre-commit instead. To keep any previous pre-commit hooks along with the new hook:

  • Rename pre-commit to pre-commit-python
  • Make pre-commit-python executable
  • Rename pre-commit.legacy to pre-commit
  • Add the line ./.git/hooks/pre-commit-python to the file pre-commit.

Compiling Dafny

By default, Dafny compiles to .NET. If you want to compile to other languages, make sure you have the appropriate dependencies installed (see below) and then use the /compileTarget: flag.

Note, the tests in the Test/comp folder run the Dafny compiler to produce code for .NET, Java, JavaScript, and Go. If you don't have all the dependencies installed, many tests will fail.

To set up Dafny to compile to JavaScript (node.js):

To set up Dafny to compile to Go:

  • Install Go from https://golang.org/dl or
    • Linux: sudo apt install golang
    • Mac: brew install golang
  • Make sure go is on your path

To set up Dafny to compile to Java:

Dafny's command-line option /compile:3 verifies, compiles, and runs your program. It works with any compilation target. If you want to do some of these steps manually (say, for a verifying program named MyProgram.dfy that has a Main method), here's how:

  • To separately compile and run your program for .NET:
    • dafny MyProgram.dfy
    • MyProgram.exe
  • Dafny can also output your .NET-compiled program as a C# program, which you can then compile yourself:
    • dafny /spillTargetCode:1 MyProgram.dfy
    • See the generated MyProgram.cs file for how to invoke csc on MyProgram.cs
  • To separately compile and run your program for JavaScript:
    • dafny /compileTarget:js /spillTargetCode:1 MyProgram.dfy
    • node MyProgram.js
  • To separately compile and run your program for Go:
    • dafny /compileTarget:go MyProgram.dfy
    • This creates a folder MyProgram-go with the target files. You must set the GOPATH to point to this folder, and Go insists that the path you give is an absolute path (including the C: on Windows).
    • After setting GOPATH, do go run MyProgram-go/src/MyProgram.go
  • To separately compile and run your program for Java:
    • If you are compiling dafny from source, make sure the Java runtime library is built. This should be done automatically by building the C# DafnyRuntime project, so just double-check that the ${DAFNY}/Binaries/DafnyRuntime.jar exists.
    • dafny /compileTarget:java MyProgram.dfy
    • java MyProgram ${DAFNY}/Binaries/DafnyRuntime.jar

Building the reference manual

The reference manual is only buildable on Linux or Mac and requires some tools to be installed

On Mac:

  • brew install --cask basictex
  • brew install pandoc
  • eval "$(/usr/libexec/path_helper)"
  • sudo tlmgr update --self
  • sudo tlmgr install framed tcolorbox environ trimspaces

Then, in the top-level directory of the source distribution: make refman

Build against a custom Boogie

Dafny is tightly integrated with Boogie. Sometimes we want to make Boogie changes and test those changes against Dafny. To do that, you must replace the Boogie NuGet package reference with project references to a locally checked out Boogie. We've added the git patch customBoogie.patch to the Dafny repository to make this easier. The patch requires that a Boogie repository with directory boogie is a sibling of the Dafny repository.

Step to use:

  • git clone git@github.com:dafny-lang/dafny.git --recurse-submodules
  • cd dafny
  • git clone git@github.com:boogie-org/boogie.git
  • git apply customBoogie.patch
  • dotnet build Source/Dafny.sln

You can then use git checkout Source/Dafny.sln Source/Directory.Build.props to return to the version of Boogie that Dafny regularly builds with.

Alternatively, you can build a local checkout of Boogie separately and copy the binaries into the Dafny Binaries directory with the Scripts/use-local-boogie.sh script:

  • ln -s <your checkout of Boogie> Source/boogie (or clone it there directly)
  • dotnet build Source/Dafny.sln
  • Scripts/use-local-boogie.sh

This can be useful for certain debugging scenarios in which you want to temporarily use a custom Boogie version, because cleaning and rebuilding automatically reverts to the standard version, and because Boogie can then easily be built with different compilation flags than Dafny.

Running DafnyLanguageServer and DafnyPipeline tests

The tests are in the projects DafnyLanguageServer.Test and DafnyPipeline.Test. You can either run them through most IDEs or on the command line:

  • IDE: For example, in Visual Studio you can open the Test Explorer view: This view allows you to run (and debug) the whole test suite using the Play button or individual tests by right-clicking them.

image

  • Command line: You can also execute the tests through the command line:
dotnet test .\Source\DafnyLanguageServer.Test\DafnyLanguageServer.Test.csproj

It's important to note that you may have to place z3 in the build directory of the tests. That's DafnyLanguageServer.Test/bin/Debug/net6.0 and DafnyLanguageServer.Test/bin/Release/net6.0, depending on your build settings. Alternatively, you can ensure that z3/bin's directory is accessible from the PATH environment variable.

Measuring code coverage of the Dafny implementation

We are working towards being able to effectively measure the code coverage of the regression test suite: switching to the xUnit-based LIT test runner was a helpful first step, but we still need to be able to execute multiple test cases with the same .NET process, and/or merge coverage results in CI.

It is fairly straightforward to measure what code is hit when handling a particular set of Dafny files, however. The steps here are the most flexible since they can be used on arbitrary inputs and not just regression test cases, but it's likely possible to get an easier and smoother workflow working within an IDE for test cases - edits welcome!

  1. (one time only) Install the coverlet and reportgenerator .NET tools.
dotnet tool install --global coverlet.console
dotnet tool install --global dotnet-reportgenerator-globaltool

  1. cd to the directory containing the Dafny DLLs (either an unzipped release or the Binaries directory of a git clone).

  2. Invoke the Dafny CLI using the coverlet tool, which will store the raw coverage data to the given file path.

coverlet . --target "dotnet" --targetargs "Dafny.dll <dafny CLI arguments>" -f covertura -o /path/to/output/coverage.cobertura.xml
  1. Run the reportgenerator tool to create a HTML report from the raw data.
reportgenerator -reports:/path/to/output/coverage.cobertura.xml -targetdir:/path/to/report/directory -reporttypes:HTML
  1. Navigate to /path/to/report/directory/index.html in a browser and enjoy!
Clone this wiki locally