Building on Linux
=================

(Tested on a fresh Linux Mint 17.2)

0. Dependencies

    apt install mono-devel g++

1. Create an empty base directory

    mkdir BASE-DIRECTORY
    cd BASE-DIRECTORY

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

3. Download and build Dafny:

   hg clone https://hg.codeplex.com/dafny
   cd dafny/Sources/
   xbuild Dafny.sln

4. Download and build Z3

   git clone https://github.com/Z3Prover/z3.git
   cd z3
   git checkout z3-4.4.0
   ./configure
   cd build
   make -j4
   cd ../..

5. Copy (or symlink) the z3 binary so that Dafny can find it:

   cd BASE-DIRECTORY
   rm -f dafny/Binaries/z3
   rm -f boogie/Binaries/z3.exe
   ln -s /usr/bin/z3 dafny/Binaries/z3
   ln -s /usr/bin/z3 boogie/Binaries/z3.exe

6. Run Dafny using the `dafny` shell script in the Binaries directory.

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/")

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