From 2e93ec8ece4d029809bf092c779756e0b18d7a6c Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 16 Jul 2015 11:16:44 -0700 Subject: Add license text and Linux setup notes --- INSTALL | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 INSTALL (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL new file mode 100644 index 00000000..2a70587e --- /dev/null +++ b/INSTALL @@ -0,0 +1,34 @@ +Building on Linux +================= + +1. Create an empty base directory + + mkdir BASE-DRIECTORY + cd BASE-DRIECTORY + +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 + +3. Download and build Dafny: + + hg clone https://hg.codeplex.com/dafny + cd dafny/Sources/ + xbuild Dafny.sln + +4. Download and build Z3 + + git clone https://github.com/Z3Prover/z3.git + cd z3 + ./configure && make && sudo make install + +5. Symlink the z3 binaries so that Boogie and Z3 can find them: + + cd BASE-DIRECTORY + ln -s /usr/bin/z3 boogie/Binaries/z3.exe + ln -s /usr/bin/z3 dafny/Binaries/z3.exe -- cgit v1.2.3 From ce07a29685a27f01c596271e03d6a39a7090d12e Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Fri, 31 Jul 2015 16:45:25 -0700 Subject: Update install notes and test them --- INSTALL | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 2a70587e..830a89f4 100644 --- a/INSTALL +++ b/INSTALL @@ -1,6 +1,12 @@ Building on Linux ================= +(Tested on a fresh Linux Mint 17.2) + +0. Dependencies + + apt install mono-devel g++ + 1. Create an empty base directory mkdir BASE-DRIECTORY @@ -14,21 +20,27 @@ Building on Linux 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/Sources/ - xbuild Dafny.sln + xbuild dafny/Source/Dafny.sln + xbuild dafny/Source/DafnyServer.sln 4. Download and build Z3 git clone https://github.com/Z3Prover/z3.git cd z3 - ./configure && make && sudo make install + git checkout z3-4.4.0 + ./configure + cd build + make -j4 + cd ../.. -5. Symlink the z3 binaries so that Boogie and Z3 can find them: +5. Copy (or symlink) the z3 binary so that Dafny and Boogie can find it: cd BASE-DIRECTORY - ln -s /usr/bin/z3 boogie/Binaries/z3.exe - ln -s /usr/bin/z3 dafny/Binaries/z3.exe + rm dafny/Binaries/z3 # Dafny already packages z3 + cp z3/build/z3 dafny/Binaries/z3 + cp z3/build/z3 boogie/Binaries/z3.exe -- cgit v1.2.3 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 From 1239f6ac97178dba507d89982b3ab0caf7b3ed4d Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel 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 From e56054fce562213ef34ed6a3d99b0cb036c2bf23 Mon Sep 17 00:00:00 2001 From: leino Date: Wed, 23 Sep 2015 03:54:37 -0700 Subject: Fixed typo in INSTALL file --- INSTALL | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'INSTALL') diff --git a/INSTALL b/INSTALL index 488060f6..e62332db 100644 --- a/INSTALL +++ b/INSTALL @@ -27,7 +27,7 @@ Dafny's sources. 3. Download and build Dafny: hg clone https://hg.codeplex.com/dafny - cd dafny/Sources/ + cd dafny/Source/ xbuild Dafny.sln 4. Download and unpack z3 (Dafny looks for `z3` in Binaries/z3/bin/) -- cgit v1.2.3