doesn't find files needed for check

[bonds]

I am attempting to check this project: https://github.com/bonds/winot. I am running liquid from the project root like so:

~/s/winot (master|…) ❯❯❯ stack exec -- liquid src/Wwan.hs 
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Parsed All Specifications ******************************************

**** DONE:  Loaded Targets *****************************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

Invalid Source

 src/Wwan.hs:3:1-16: Error: GHC Error

 3 | import Protolude
     ^^^^^^^^^^^^^^^^

     attempting to use module `Protolude' (/home/scott/src/winot/src/Protolude.hs) which is not loaded

 src/Wwan.hs:5:1-11: Error: GHC Error

 5 | import Util
     ^^^^^^^^^^^

     attempting to use module `Util' (/home/scott/src/winot/src/Util.hs) which is not loaded

 src/Wwan.hs:6:1-12: Error: GHC Error

 6 | import World
     ^^^^^^^^^^^^

     attempting to use module `World' (/home/scott/src/winot/src/World.hs) which is not loaded
~/s/winot (master|…) ❯❯❯

It doesn't seem to figure out which files to include on its own. Trying stack exec -- liquid -i src src/Wwan.hs yields the same result. Adding --cabal-dir with or without -i src yields the same result. Using --c-files= in reference to one of the files in the error message seems to be a step in the right direction:

~/s/winot (master|…) ❯❯❯ stack exec -- liquid --c-files=src/World.hs src/Wwan.hs

LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Parsed All Specifications ******************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

Invalid Source

 /home/scott/src/winot/src/World.hs:3:1-16: Error: GHC Error

 3 | import Protolude
     ^^^^^^^^^^^^^^^^

     attempting to use module `Protolude' (/home/scott/src/winot/src/Protolude.hs) which is not loaded
~/s/winot (master|…) ❯❯❯

So I include another like so:

~/s/winot (master|…) ❯❯❯ stack exec -- liquid --c-files=src/Protolude.hs --c-files=src/World.hs src/Wwan.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Parsed All Specifications ******************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

Invalid Source

 /home/scott/src/winot/src/Protolude.hs:18:1-26: Error: GHC Error

 18 | import qualified List as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `List' (/home/scott/src/winot/src/List.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:19:1-26: Error: GHC Error

 19 | import qualified Show as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Show' (/home/scott/src/winot/src/Show.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:20:1-26: Error: GHC Error

 20 | import qualified Bool as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Bool' (/home/scott/src/winot/src/Bool.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:21:1-27: Error: GHC Error

 21 | import qualified Debug as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Debug' (/home/scott/src/winot/src/Debug.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:22:1-27: Error: GHC Error

 22 | import qualified Monad as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Monad' (/home/scott/src/winot/src/Monad.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:23:1-33: Error: GHC Error

 23 | import qualified Applicative as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Applicative' (/home/scott/src/winot/src/Applicative.hs) which is not loaded
~/s/winot (master|…) ❯❯❯                            Sun Apr 10 07:07:04 PDT 2016

How about another?

~/s/winot (master|…) ❯❯❯ stack exec -- liquid --c-files=src/Protolude.hs --c-files=src/Applicative.hs --c-files=src/World.hs src/Wwan.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Parsed All Specifications ******************************************

**** DONE:  annotate ***********************************************************

**** RESULT: ERROR *************************************************************

Invalid Source

 /home/scott/src/winot/src/Protolude.hs:18:1-26: Error: GHC Error

 18 | import qualified List as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `List' (/home/scott/src/winot/src/List.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:19:1-26: Error: GHC Error

 19 | import qualified Show as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Show' (/home/scott/src/winot/src/Show.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:20:1-26: Error: GHC Error

 20 | import qualified Bool as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Bool' (/home/scott/src/winot/src/Bool.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:21:1-27: Error: GHC Error

 21 | import qualified Debug as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Debug' (/home/scott/src/winot/src/Debug.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:22:1-27: Error: GHC Error

 22 | import qualified Monad as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Monad' (/home/scott/src/winot/src/Monad.hs) which is not loaded

 /home/scott/src/winot/src/Protolude.hs:23:1-33: Error: GHC Error

 23 | import qualified Applicative as X
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

     attempting to use module `Applicative' (/home/scott/src/winot/src/Applicative.hs) which is not loaded
~/s/winot (master|…) ❯❯❯                            Sun Apr 10 07:07:56 PDT 2016

Hmm, that time including an additional file didn't do anything. Maybe the ordering matters?

~/s/winot (master|…) ❯❯❯ stack exec -- liquid --c-files=src/Applicative.hs --c-files=src/Protolude.hs --c-files=src/World.hs src/Wwan.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Parsed All Specifications ******************************************

liquid: liquid: panic! (the 'impossible' happened)
  (GHC version 7.10.3 for x86_64-unknown-openbsd):
        codeOutput: HscInterpreted

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

~/s/winot (master|…) ❯❯❯

Hmm. The 'impossible' happened. Not sure what to try next. Here's some info on my environment:

~/s/winot (master|…) ❯❯❯ which ghc                  Sun Apr 10 07:10:00 PDT 2016
/usr/local/bin/ghc
~/s/winot (master|…) ❯❯❯ stack exec which ghc       Sun Apr 10 07:10:10 PDT 2016
/usr/local/bin/ghc
~/s/winot (master|…) ❯❯❯ ghc --version              Sun Apr 10 07:10:23 PDT 2016
The Glorious Glasgow Haskell Compilation System, version 7.10.3
~/s/winot (master|…) ❯❯❯ which liquid               Sun Apr 10 07:10:29 PDT 2016
/home/scott/.local/bin/liquid
~/s/winot (master|…) ❯❯❯ stack exec which liquid    Sun Apr 10 07:10:44 PDT 2016
/home/scott/.local/bin/liquid
~/s/winot (master|…) ❯❯❯ liquid -V                  Sun Apr 10 07:12:26 PDT 2016
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.
~/s/liquidhaskell (master|✔) ❯❯❯ uname -mrsv        Sun Apr 10 07:16:16 PDT 2016
OpenBSD 5.9 GENERIC.MP#3 amd64

I am running liquid at commit 4adc84421e6cfed601c8202ee99191beb99e5576.

[ranjitjhala]

Odd thanks for filing this! Will take a look this afternoon!

[ranjitjhala]

@spinda and @gridaphobe any chance the panic is due to the missing z3 path?

[ranjitjhala]

@bonds what is the result of 'which z3'?

[bonds]

~/s/winot (master|✔) ❯❯❯ which z3                   Sun Apr 10 10:07:10 PDT 2016
/home/scott/.pyenv/shims/z3

liquid does seem to be working on certain files in the project, so it at least sometimes can find z3:

~/s/winot (master|✔) ❯❯❯ stack exec -- liquid app/Main.hs 
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Parsed All Specifications ******************************************

**** DONE:  Loaded Targets *****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  generateConstraints ************************************************

Done solving.
Safe

**** DONE:  solve **************************************************************

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************
~/s/winot (master|✔) ❯❯❯                            Sun Apr 10 10:18:55 PDT 2016

There is not much in that file, as you can see, but you can at least see that liquid isn't complaining that it can't find a solver.

[gridaphobe]

Ugh, the problem is that winot.cabal sets a few default extensions that we don't see. They need to be passed explicitly on the command-line, as for ghc-mod or hdevtools.

% stack exec liquid -- -isrc  src/Wwan.hs -g-XOverloadedStrings -g-XNoImplicitPrelude
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

**** DONE:  Parsed All Specifications ******************************************

**** DONE:  Loaded Targets *****************************************************

**** DONE:  Extracted Core using GHC *******************************************

**** DONE:  generateConstraints ************************************************

Done solving.
Safe

**** DONE:  solve **************************************************************

**** DONE:  annotate ***********************************************************

**** RESULT: SAFE **************************************************************

I try to avoid setting defaults in the .cabal file for this reason.

[gridaphobe]

@ranjitjhala this is a perfect example of the pain that we could avoid if we got LH working as a GHC plugin :)

[ranjitjhala]

Ah thanks! Wonder if there is some way to make this clear to users. At the very least we should make a troubleshooting /faq that explains the limitation...

On Apr 10, 2016, at 11:32 AM, Eric Seidel notifications@github.com wrote:

Ugh, the problem is that winot.cabal sets a few default extensions that we don't see. They need to be passed explicitly on the command-line, as for ghc-mod or hdevtools.

% stack exec liquid -- -isrc src/Wwan.hs -g-XOverloadedStrings -g-XNoImplicitPrelude LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.

\ DONE: Parsed All Specifications ****

** DONE: Loaded Targets ***

** DONE: Extracted Core using GHC *****

\ DONE: generateConstraints **

Done solving. Safe

\ DONE: solve ****

** DONE: annotate *****

\ RESULT: SAFE **** I try to avoid setting defaults in the .cabal file for this reason.

— You are receiving this because you commented. Reply to this email directly or view it on GitHub

[gridaphobe]

I think part of the problem is that we (probably) discard the result of the load LoadAllTargets call, which I believe would tell us that some modules failed to compile (and why).

Also, @spinda's new cabal integration probably sidesteps this issue entirely since it has easy access to the cabal info.

[spinda]

@bonds Can you give liquidhaskell-cabal a try? It should be a drop-in solution to this sort of problem.

The particular issue of not handling load failures correctly is fixed in the api-annotations branch.

@gridaphobe GHC plugin integration is getting closer! The pieces are starting to fall into place.