blob: dbc63410d70b73be2229d26c15d9508b3fa25121 (
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
58
59
60
|
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.
|
