liquidhaskell

![LiquidHaskell](/resources/logo.png)


[![Hackage](https://img.shields.io/hackage/v/liquidhaskell.svg)](https://hackage.haskell.org/package/liquidhaskell) [![Build Status](https://img.shields.io/circleci/project/ucsd-progsys/liquidhaskell/develop.svg)]([https://circleci.com/gh/ucsd-progsys/liquidhaskell](https://app.circleci.com/pipelines/github/ucsd-progsys/liquidhaskell?branch=develop))

This is the **development** site of the LiquidHaskell formal verification tool.

If you're a LiquidHaskell **user** (or just curious), you probably want to go to [the documentation website](https://ucsd-progsys.github.io/liquidhaskell/) instead.

## Trying it from Hackage

Assuming the [Z3](https://github.com/Z3Prover/z3) SMT solver version `4.15.1` or
newer is installed and available in your `PATH`, you can run

```
cabal install --lib liquidhaskell liquid-prelude liquid-vector --package-env . --force-reinstalls
ghc -fplugin=LiquidHaskell FILE.hs
```

`--package-env .` creates a `.ghc.environment*` file in the current folder that makes
`ghc` find the `LiquidHaskell` plugin only when invoking it from there.
Otherwise, global user configuration would be affected.

Note that the installation step is influenced by the dependencies that are
already installed in your system, so different results may be obtained by
different users.

## Trying it from GitHub

The github repo builds with GHC `9.14.1`, cabal-install `3.16.1.0`, and `z3` `4.15.1` or newer, all of
which must be in your `PATH`.

```
git clone https://github.com/ucsd-progsys/liquidhaskell.git
cd liquidhaskell
git submodule update --init
cabal build liquidhaskell liquid-prelude liquid-vector

cabal exec -- ghc -fplugin=LiquidHaskell FILE.hs
```

## Asking for Help

If you have questions or you just need help, you can always reach out on our [zulip space](https://liquidhaskell.zulipchat.com/), [google groups mailing list](https://groups.google.com/forum/#!forum/liquidhaskell), [GitHub issue tracker](https://github.com/ucsd-progsys/liquidhaskell/issues), or by emailing [Ranjit Jhala](https://github.com/ranjitjhala), [Niki Vazou](https://github.com/nikivazou).

# Contributing

This is an open-source project, and we love getting feedback (and patches)!

## Reporting a Bug

If something doesn't work as it should, please consider opening a [github issue](https://github.com/ucsd-progsys/liquidhaskell/issues)
to let us know. If possible, try to:

* Try to use a descriptive title;
* State as clearly as possible what is the problem you are facing;
* Provide a small Haskell file producing the issue;
* Write down the expected behaviour vs the actual behaviour;
* Please, let us know which liquidhaskell version you are using.

## Your first Pull Request

We are thrilled to get PRs! Please follow these guidelines, as doing so will increase the chances of
having your PR accepted:

* The main LH repo [lives here](https://github.com/ucsd-progsys/liquidhaskell)
* Please create pull requests against the `develop` branch.
* Ple