diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-27 19:46:36 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-08-27 19:46:36 -0700 |
| commit | 1239f6ac97178dba507d89982b3ab0caf7b3ed4d (patch) | |
| tree | cce533d5218cc12173b61fd21cf814cc5a272776 /INSTALL | |
| parent | 4c71672823dfac1cd352f0da6a61b83680d7eb31 (diff) | |
Update INSTALL to reflect the latest packaging changes
Diffstat (limited to 'INSTALL')
| -rw-r--r-- | INSTALL | 27 |
1 files changed, 12 insertions, 15 deletions
@@ -1,7 +1,9 @@ Building on Linux
=================
-(Tested on a fresh Linux Mint 17.2)
+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
@@ -28,25 +30,20 @@ Building on Linux cd dafny/Sources/
xbuild Dafny.sln
-4. Download and build Z3
+4. Download and unpack z3 (Dafny looks for `z3` in Binaries/z3/bin/)
- git clone https://github.com/Z3Prover/z3.git
- cd z3
- git checkout z3-4.4.0
- ./configure
- cd build
- make -j4
- cd ../..
+ 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. Copy (or symlink) the z3 binary so that Dafny can find it:
+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 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
+ cp dafny/Binaries/z3/bin/z3 boogie/Binaries/z3.exe
-6. Run Dafny using the `dafny` shell script in the Binaries directory.
+6. Run Dafny using the `dafny` shell script in the Binaries directory (it calls mono as appropriate)
Editing in Emacs
================
@@ -55,6 +52,6 @@ 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/")
+ (setq flycheck-dafny-executable "BASE-DIRECTORY/dafny/Binaries/dafny")
Do look at the README, though! It's full of useful tips.
|