From 7b982a26befa48de72e3f6f55a11eb1d724bd1ee Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 13 Aug 2015 10:40:18 -0700 Subject: Update INSTALL notes to mention the wrapper script --- INSTALL | 30 ++++++++++++++++++++++-------- 1 file changed, 22 insertions(+), 8 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 830a89f4..dbc63410 100644 --- a/INSTALL +++ b/INSTALL @@ -9,8 +9,8 @@ Building on Linux 1. Create an empty base directory - mkdir BASE-DRIECTORY - cd BASE-DRIECTORY + mkdir BASE-DIRECTORY + cd BASE-DIRECTORY 2. Download and build Boogie: @@ -25,8 +25,8 @@ Building on Linux 3. Download and build Dafny: hg clone https://hg.codeplex.com/dafny - xbuild dafny/Source/Dafny.sln - xbuild dafny/Source/DafnyServer.sln + cd dafny/Sources/ + xbuild Dafny.sln 4. Download and build Z3 @@ -38,9 +38,23 @@ Building on Linux make -j4 cd ../.. -5. Copy (or symlink) the z3 binary so that Dafny and Boogie can find it: +5. Copy (or symlink) the z3 binary so that Dafny can find it: cd BASE-DIRECTORY - rm dafny/Binaries/z3 # Dafny already packages z3 - cp z3/build/z3 dafny/Binaries/z3 - cp z3/build/z3 boogie/Binaries/z3.exe + 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. -- cgit v1.2.3