Skip to content

INSTALL

Jump to bottom
Alex Chew edited this page Nov 15, 2024 · 98 revisions

This page has instructions for installing Dafny for developers.

User installation instructions are in the project's repository. Those instructions are a necessary precursor to these.

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:

To install pre-commit checks to verify the style of C# files, run:

pip install pre-commit
pre-commit install

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

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.12.1, 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 text area "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

To install pre-commit checks to verify the style of the source code, perform

   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.12.1 (not the most recent version of Z3)

    make z3-ubuntu

    OR

    cd dafny/Binaries
wget https://github.com/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-ubuntu-20.04-bin.zip
unzip z3-4.12.1-x64-ubuntu-20.04-bin.zip
mv z3-4.12.1 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
make exe

To install pre-commit checks to verify the style of the source code, perform

   brew install pre-commit
   pre-commit install

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.12.1 (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/dafny-lang/solver-builds/releases/download/snapshot-2023-08-02/z3-4.12.1-x64-macos-11-bin.zip
   unzip z3-4.12.1-x64-macos-11-bin.zip
   mv z3-4.12.1 z3

  1. Install the compiler dependences as described here.

  2. Install backend-dependencies as needed.

  3. To compile to JavaScript, make sure you have Node.js installed and run

    npm install bignumber.js

  4. 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

  5. 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

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.

Steps to use:

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.

Clone this wiki locally