Granule needs the Z3 SMT solver for discharging verification conditions.
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
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
Currently we have binary releases only for MacOS.
Build Granule From Source
Stack can manage all the Haskell-related build dependencies for you automatically, with sandboxing.
Linux and MacOS
curl -sSL https://get.haskellstack.org/ | sh
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
If you have any problems building, this may be due to an outdated version of
Stack; you can update Stack via
If this doesn't resolve the problem, please open an issue giving all relevant details.