summaryrefslogtreecommitdiff
path: root/INSTALL
blob: 830a89f499b6fffa6917204169f40b10626e9bd1 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
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-DRIECTORY
    cd BASE-DRIECTORY

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
   xbuild dafny/Source/Dafny.sln
   xbuild dafny/Source/DafnyServer.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 and Boogie can find it:

   cd BASE-DIRECTORY
   rm dafny/Binaries/z3 # Dafny already packages z3
   cp z3/build/z3 dafny/Binaries/z3
   cp z3/build/z3 boogie/Binaries/z3.exe