Skip to content

Latest commit

 

History

History
57 lines (40 loc) · 1.7 KB

INSTALL

File metadata and controls

57 lines (40 loc) · 1.7 KB
Raw

-- mode: markdown -- Building on Linux

Tested on a fresh Linux Mint 17.2. 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

    apt install mono-devel g++

  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 mozroots --import --sync wget https://nuget.org/nuget.exe mono ./nuget.exe restore Source/Boogie.sln xbuild Source/Boogie.sln cd ..

  4. Download and build Dafny:

    hg clone https://hg.codeplex.com/dafny xbuild 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.4.0/z3-4.4.0-x64-ubuntu-14.04.zip unzip z3-4.4.0-x64-ubuntu-14.04.zip mv z3-4.4.0-x64-ubuntu-14.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)

Editing in 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 "BASE-DIRECTORY/dafny/Binaries/dafny")

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