diff options
| author |  Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-05-30 17:58:02 -0400 |
| commit | e67c951ad9c5c637e36a6f025ba3d6e3ad945416 (patch) | |
| tree | 0cfb5c339602e4bdebf4bf97f3f0ccc3923c14d1 /INSTALL | |
| parent | 000aa762e1fee4b9bd83ec3d7c8b61fd203e2c9d (diff) | |
| parent | df5c5f547990c1f80ab7594a1f9287ee03a61754 (diff) | |
Merge commit 'df5c5f5'
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 57 |
1 files changed, 57 insertions, 0 deletions
diff --git a/INSTALL b/INSTALL new file mode 100644 index 00000000..e62332db --- /dev/null +++ b/INSTALL @@ -0,0 +1,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.
|