Update INSTALL to reflect the latest packaging changes

1 files changed, 12 insertions, 15 deletions

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.