Z3
Granule needs the Z3 SMT solver for discharging verification conditions.
MacOS
Recommended: use homebrew.
brew install z3
If you don't have brew, first run
/usr/bin/ruby -e "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/master/install)"
Alternative: download the precompiled binary and put it on your path, e.g., assuming the binary is located in ~/Downloads/z3/bin/:
mv ~/Downloads/z3/bin/z3 /usr/local/bin/z3
Linux and Windows
Recommended: install Z3 via your package manager of choice.
Alternative: download the precompiled binary and put it on your path.
Granule Binary Release
See binary releases.
Build Granule From Source
Haskell Stack
Stack can manage all the Haskell-related build dependencies for you automatically, with sandboxing.
Linux and MacOS
curl -sSL https://get.haskellstack.org/ | sh
Windows
See https://docs.haskellstack.org/en/stable/install_and_upgrade/
Get Granule
To build the Granule frontend gr and the interactive mode grepl just run:
git clone https://github.com/granule-project/granule && cd granule && stack setup && stack install :gr && stack install :grepl
Troubleshooting
If you have any problems building, this may be due to an outdated version of
Stack; you can update Stack via stack upgrade.
If this doesn't resolve the problem, please open an issue giving all relevant
details.