Skip to content

Latest commit

 

History

History
96 lines (65 loc) · 3.08 KB

INSTALL.md

File metadata and controls

96 lines (65 loc) · 3.08 KB
Raw

Building on Linux

Tested on a fresh Ubuntu 16.04 image. Note that we now have official releases for Linux, so these instructions mostly apply to people interested in looking at Dafny's sources.

  1. Dependencies: Install Mono from the official repositories; the version in most distribution repositories is too out of date. The mono-devel package is what you need.

  2. Create an empty base directory

    mkdir BASE-DIRECTORY
cd BASE-DIRECTORY

  3. Download and build Boogie:

    git clone https://github.com/boogie-org/boogie
cd boogie
wget https://nuget.org/nuget.exe
mono ./nuget.exe restore Source/Boogie.sln
msbuild Source/Boogie.sln
cd ..

  4. Download and build Dafny:

    cd BASE-DIRECTORY
git clone https://github.com/Microsoft/dafny.git 
msbuild dafny/Source/Dafny.sln

  5. Download and unpack z3 (Dafny looks for z3 in Binaries/z3/bin/)

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

  6. (Optional) If you plan to use Boogie directly, copy (or symlink) the z3 binary so that Boogie, too, can find it:

    cd BASE-DIRECTORY
rm -f boogie/Binaries/z3.exe
cp dafny/Binaries/z3/bin/z3 boogie/Binaries/z3.exe

  7. Run Dafny using the dafny shell script in the Binaries directory (it calls mono as appropriate)

Building on Mac OS X

Tested on Mac OS X 10.12.6 (Sierra). Note that we now have official releases for Mac OS X, so these instructions mostly apply to people interested in looking at Dafny's sources.

  1. Dependencies (using Homebrew)

    brew install mono
brew cask install mono-mdk

  2. Create an empty base directory

    mkdir BASE-DIRECTORY
cd BASE-DIRECTORY

  3. Download and build Boogie:

    git clone https://github.com/boogie-org/boogie
cd boogie
wget https://nuget.org/nuget.exe
mono ./nuget.exe restore Source/Boogie.sln
msbuild Source/Boogie.sln
cd ..

    Note: If the xbuild step above fails, try running it again.

  4. Download and build Dafny:

    cd BASE-DIRECTORY
git clone https://github.com/Microsoft/dafny.git 
msbuild dafny/Source/Dafny.sln

  5. Download and unpack z3 (Dafny looks for z3 in Binaries/z3/bin/)

    cd BASE-DIRECTORY
wget https://github.com/Z3Prover/z3/releases/download/z3-4.6.0/z3-4.6.0-x64-osx-10.11.6.zip
unzip z3-4.6.0-x64-osx-10.11.6.zip
mv z3-4.6.0-x64-osx-10.11.6 dafny/Binaries/z3

  6. (Optional) If you plan to use Boogie directly, copy (or symlink) the z3 binary so that Boogie, too, can find it:

    cd BASE-DIRECTORY
rm -f boogie/Binaries/z3.exe
cp dafny/Binaries/z3/bin/z3 boogie/Binaries/z3.exe

  7. Run Dafny using the dafny shell script in the Binaries directory (it calls mono as appropriate)