blob: e62332db642460bb4d83d5f77e2ce7f8e7a80b40 (
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
47
48
49
50
51
52
53
54
55
56
57
|
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.
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/Source/
xbuild Dafny.sln
4. 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
5. (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
6. 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.
|
