First class support for Liquid Haskell?

[mgsloan]

Should we add first class support for Liquid Haskell in stack? I have not used Liquid Haskell much yet, so I don't know how much sense this makes. It could be as simple as stack liquid, and it will automatically install it appropriately if necessary, and run the tool on your code. I will send an email to the Liquid Haskell authors and get them involved in this discussion.

It is quite possible that first class support is unnecessary. I just found this project - https://github.com/spinda/liquidhaskell-cabal/blob/0.1.1.0/README.md - but I have not yet tried it, sounds like it supports stack decently. Perhaps it would be helpful to streamline things for usage with stack?

In mgsloan/store#71 , @kantp added use of liquid haskell to verify that we stay within the bounds of the bytebuffer! This allows us to have code that is both fast and trustworthy. Fantastic!

Considering we are now maintaining code that uses Liquid Haskell, it only makes sense to have our Travis CI for store use it. To me, the most sensible implementation approach is by having direct support in stack.

[gridaphobe]

@mgsloan this is an exciting idea, thanks for suggesting it!

There are two modes I think we'd want to support.

1. Run LiquidHaskell as part of the build process, which is what the liquidhaskell-cabal package does.
2. Run LiquidHaskell on individual modules, e.g. as part of a linter for emacs/vim.

In both cases, I think the main support we'd want from stack is to ensure a version of LiquidHaskell is used that is compatible with the selected GHC. Specifically we want to ensure that LiquidHaskell was built with the same GHC that we're using to build the project. So perhaps a stack liquid command could just ensure that? (i.e. something equivalent to stack build liquidhaskell && stack exec liquid -- "$@" ought to work?)

[mgsloan]

That's correct Eric! stack build liquidhaskell will place the liquid executable in your local sandbox, and it will use the appropriate GHC version. Not quite as efficient as possible, but I think a more efficient approach will be implemented before the next release - #2643.

Run LiquidHaskell as part of the build process, which is what the liquidhaskell-cabal package does.

Makes sense! I suppose we can directly use the liquidhaskell-cabal project, or borrow its approach.

Run LiquidHaskell on individual modules, e.g. as part of a linter for emacs/vim.

This is not directly within the scope of stack, however I think it is within scope for intero! For example, intero plans support for hoogle: https://github.com/commercialhaskell/intero/issues/129

The real awesome-sauce would be to compile liquid haskell directly into intero, but I'm not sure how much effort that would take. We face a similar problem with support for ghcjs in intero: https://github.com/commercialhaskell/intero/issues/64

[gridaphobe]

Run LiquidHaskell on individual modules, e.g. as part of a linter for emacs/vim.
This is not directly within the scope of stack, however I think it is within scope for intero! For example, intero plans support for hoogle: commercialhaskell/intero#129

The real awesome-sauce would be to compile liquid haskell directly into intero, but I'm not sure how much effort that would take. We face a similar problem with support for ghcjs in intero: commercialhaskell/intero#64

Hmm, integration with intero is also a very cool idea, and could avoid some of the overhead from having multiple GHC's typecheck the source (one for GHC itself, and one for GHC via LH).

I think running liquid on a single file is well within the scope of stack though, that's the default mode for liquid, and doesn't seem to be any different from the stack ghc command.

[nikivazou]

Thanks for the suggestion @mgsloan!

One thing to keep in mind when you are using Liquid Haskell in a big library is that verification time can be long.

I did integrate Liquid Haskell verification in a real project (~73 modules) and I just added a command "runLiquidAll" in the Travis CI built. That ended up taking ~80 min that does not fit well in software building process.

Now, if there is a stack command that installs Liquid Haskell and runs liquid in all the .hs files, it would be definitely convenient. Moreover, if we can tell Travis CI to only run this in the nightly builds, this would be even more practical.

[mgsloan]

Hmm, integration with intero is also a very cool idea, and could avoid some of the overhead from having multiple GHC's typecheck the source (one for GHC itself, and one for GHC via LH).

Yep! I think it makes a lot of sense to turn intero into something that provides a shared GHC context for all the tools that need it. haskell-ide-engine has a similar goal and approach. We are taking the approach of extending GHCI, rather than starting fresh, because this is the easiest way to do it while retaining REPL capability.

One thing to keep in mind when you are using Liquid Haskell in a big library is that verification time can be long.

Good to know, @nikivazou ! It certainly makes sense to me to have it as a CI step. That way, most contributors do not need to run liquid haskell. Instead, there will be an async notification if they broke some property.

[chshersh]

@nikivazou Could you share your runLiquidAll command? I'm trying to configure LiquidHaskell on Travis CI and this is not an easy task...

[nikivazou]

I am using stack test for Travis integration. Check out this template: https://github.com/nikivazou/theorem-proving-template

…

On Mon, Mar 5, 2018 at 2:12 PM, Dmitry Kovanikov ***@***.***> wrote: @nikivazou <https://github.com/nikivazou> Could you share your runLiquidAll command? I'm trying to configure LiquidHaskell on Travis CI and this is not an easy task... — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#2641 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AArotaU7m69DEc8mGUT6VtymbnRwH-d9ks5tbY4xgaJpZM4KHQp4> .

-- Niki Vazou