How to install and build the sources using Mono
Boogie can be built and run on Mac OS X and Linux machines following the instructions below.
Building from command line
Go to the Sources
directory and use the
command to build the Boogie.sln
$ cd /path/to/boogie/Source
# Restore the NuGet packages used by Boogie
$ wget https://nuget.org/nuget.exe
$ mono ./nuget.exe restore Boogie.sln
# Build Boogie
$ xbuild Boogie.sln
# Run unit tests (replace "Release" with the build type of Boogie)
$ UnitTests/run-unittests.py Release
Building in Monodevelop
- Start Monodevelop
- If you don't have the NuGet add-in installed then install it (
Tools > Add-in Manager )
- Open Source/Boogie.sln and select
Build > Build All from the menu
- Run the unit tests by going to the Unit Tests panel and clicking on
Note that projects other than Boogie itself (i.e. Dafny, Chalice, BCT) have not yet been tested under Mono.
Boogie will try to find Z3 in its Binaries
. You can make this available by creating a symlink as below:
ln -s /path/to/z3/bin/z3 /path/to/boogie/Binaries/z3.exe
Now you can run Boogie using mono
mono /path/to/boogie/Binaries/Boogie.exe input.bpl
You may wish to create an alias for easy access in your .bashrc or similar:
alias boogie='mono /path/to/boogie/Binaries/Boogie.exe'
Running the driver test suite
To make sure your build of Boogie is working correctly you should run the driver test suite.
See here for details