Skip to content

Latest commit

 

History

History
92 lines (70 loc) · 3.49 KB

File metadata and controls

92 lines (70 loc) · 3.49 KB

Local installation of Liquid Haskell

Installing Haskell and Cabal

The most straightforward way is using ghcup, the Haskell tool chain installer. You can install ghcup by running the following command in your terminal on Linux, WSL or macOS:

curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh

And then follow the instructions to install GHC and Cabal.

ghcup install ghc
ghcup install cabal

Installing Z3

Liquid Haskell can work with multiple SMT solvers, but Z3 is the most commonly used one. You can download Z3 from its GitHub releases page. But it is very likely that your system’s package manager has Z3 available.

For example, on Ubuntu you can install it with:

sudo apt-get install z3

On macOS, you can use Homebrew:

brew install z3

Installing Liquid Haskell

We will use Liquid Haskell inside a Cabal project, that is, a directory that contains a .cabal file like the one included in this zip file.

We also provide a test file Test.hs where we can write our Liquid Haskell code.

To install Liquid Haskell and verify that everything is working, run:

cabal build

The first time this might take a while as Cabal will download, install and compile all the necessary dependencies.

If everything is set up correctly, you should see Liquid Haskell verifying the test file without any errors. You should see something similar to this at the end of the output:

[1 of 1] Compiling Test             ( Test.hs, dist/build/Test.o )

LIQUID: SAFE (1 constraints checked) **************************************

And that’s it! You have successfully installed Liquid Haskell.

Online Liquid Haskell

There is an online version of Liquid Haskell (https://liquidhaskell.goto.ucsd.edu/index.html) that you can use instead (but we recommend the local installation, if possible).

Contacts

If you have any questions, please feel free to send us an email (alessio.ferrarini@imdea.org, pablo.castellanos@imdea.org), or ask in the Liquid Haskell slack.