From 7f90421a0fc200f47ffd731e1c09a5e98f28b68c Mon Sep 17 00:00:00 2001 From: fendor Date: Sun, 2 Jun 2019 15:29:44 +0200 Subject: [PATCH] Add liquid haskell smt solver to README --- README.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/README.md b/README.md index 78504f791..4fc8addd2 100644 --- a/README.md +++ b/README.md @@ -63,6 +63,7 @@ we talk to clients.__ - [Is there a hash (#) after \?](#is-there-a-hash--after-package) - [Otherwise](#otherwise) - [Nix: cabal-helper, No such file or directory](#nix-cabal-helper-no-such-file-or-directory) + - [Liquid Haskell](#liquid-haskell) ## Features @@ -629,4 +630,7 @@ cabal-helper-wrapper: /home/<...>/.cache/cabal-helper/cabal-helper<...>: createP can happen because cabal-helper compiles and runs above executable at runtime without using nix-build, which means a Nix garbage collection can delete the paths it depends on. Delete ~/.cache/cabal-helper and restart HIE to fix this. +### Liquid Haskell +Liquid Haskell requires an SMT solver on the path. We do not take care of installing one, thus, Liquid Haskell will not run until one is installed. +The recommended SMT solver is [z3](https://github.com/Z3Prover/z3). To run the tests, it is also required to have an SMT solver on the path, otherwise the tests will fail for Liquid Haskell.