From 1239f6ac97178dba507d89982b3ab0caf7b3ed4d Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 27 Aug 2015 19:46:36 -0700
Subject: Update INSTALL to reflect the latest packaging changes

---
 INSTALL | 27 ++++++++++++---------------
 1 file changed, 12 insertions(+), 15 deletions(-)

(limited to 'INSTALL')

diff --git a/INSTALL b/INSTALL
index dbc63410..488060f6 100644
--- a/INSTALL
+++ b/INSTALL
@@ -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.
-- 
cgit v1.2.3