Could not find module ‘LiquidHaskellBoot’

[jwaldmann]

(see #2258 )

using a project-specific environment file, I still get

$ cabal install --lib liquidhaskell-boot  --package-env=lh

$ cabal install liquid-platform  --package-env=lh
...
Error: setup: '/opt/ghc/latest/bin/ghc-9.6.3' exited with an error:
<command line>: Could not find module ‘LiquidHaskellBoot’
Use -v (or `:set -v` in ghci) to see a list of the files searched for.

Error: cabal: Failed to build liquidhaskell-0.9.4.7.0 (which is required by
exe:liquidhaskell from liquid-platform-0.9.2.8). See the build log above for
details

I guess the env file is not used by the plugin.

with stack, same thing:

$ stack install
...
liquidhaskell  > Error: setup: '/opt/ghc/ghc-9.6.3/bin/ghc-9.6.3' exited with an error:
liquidhaskell  > <command line>: Could not find module ‘LiquidHaskellBoot’

[facundominguez]

Thanks @jwaldmann.

I'm moving here a comment from #2258.

It is looking like a bug in Cabal (the library) too.

Running cabal install --lib ./ --verbose leads to the following failing invocation of ghc.

As far as I can see, the liquidhaskell-boot package is not being exposed, but ghc is still given -fplugin=LiquidHaskellBoot.

It looks a lot like this issue: haskell/cabal#9375, and I don't think cabal 3.10.2.1 includes the fix.

...
Installing
dist/build/libHSliquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167.a
to
/home/facundo/.cabal/store/ghc-9.6.3/incoming/new-2588540/home/facundo/.cabal/store/ghc-9.6.3/liquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167/lib/libHSliquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167.a
creating
/home/facundo/.cabal/store/ghc-9.6.3/incoming/new-2588540/home/facundo/.cabal/store/ghc-9.6.3/liquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167/lib
Installing executable
dist/build/libHSliquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167-ghc9.6.3.so
to
/home/facundo/.cabal/store/ghc-9.6.3/incoming/new-2588540/home/facundo/.cabal/store/ghc-9.6.3/liquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167/lib/libHSliquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167-ghc9.6.3.so
Running: /nix/store/xavd6yb7irpx2m6jxy4kidcxx7r0ldh4-ghc-9.6.3/bin/ghc-9.6.3 --abi-hash -fbuilding-cabal-package -O -outputdir dist/build -odir dist/build -hidir dist/build -stubdir dist/build -i -idist/build -isrc -idist/build/autogen -idist/build/global-autogen -Idist/build/autogen -Idist/build/global-autogen -Idist/build -optP-include -optPdist/build/autogen/cabal_macros.h -this-unit-id liquidhaskell-0.9.4.7.0-57bc104bc828a52993a1b05e41edf388812486990679f05e37c552c73c312167 -hide-all-packages -Wmissing-home-modules -no-user-package-db -XHaskell98 LiquidHaskell GHC.Classes_LHAssumptions GHC.CString_LHAssumptions GHC.Types_LHAssumptions Data.Bits_LHAssumptions Data.Either_LHAssumptions Data.Foldable_LHAssumptions Data.Int_LHAssumptions Data.Maybe_LHAssumptions Data.String_LHAssumptions Data.Tuple_LHAssumptions Data.Word_LHAssumptions Foreign.C.String_LHAssumptions Foreign.C.Types_LHAssumptions Foreign.Concurrent_LHAssumptions Foreign.Marshal.Alloc_LHAssumptions Foreign.ForeignPtr_LHAssumptions Foreign.Ptr_LHAssumptions Foreign.Storable_LHAssumptions GHC.Base_LHAssumptions GHC.Exts_LHAssumptions GHC.Float_LHAssumptions GHC.ForeignPtr_LHAssumptions GHC.Int_LHAssumptions GHC.IO.Handle_LHAssumptions GHC.List_LHAssumptions GHC.Num_LHAssumptions GHC.Num.Integer_LHAssumptions GHC.Maybe_LHAssumptions GHC.Ptr_LHAssumptions GHC.Real_LHAssumptions GHC.Word_LHAssumptions Liquid.Prelude.Real_LHAssumptions Liquid.Prelude.Totality_LHAssumptions Prelude_LHAssumptions Data.ByteString_LHAssumptions Data.ByteString.Char8_LHAssumptions Data.ByteString.Lazy.Char8_LHAssumptions Data.ByteString.Lazy_LHAssumptions Data.ByteString.Short_LHAssumptions Data.ByteString.Unsafe_LHAssumptions Data.Set_LHAssumptions -Wall '-fplugin=LiquidHaskellBoot' -Werror -hide-all-packages -j

[facundominguez]

I just merged a workaround in 5fbff05. Although it goes with the switch to ghc-9.8.1. It wouldn't be difficult to backport if it needs to work in an earlier compiler.

Please, let me know if this doesn't fix it.

[jwaldmann]

Thanks for working on this. For commit 5fbff05 , I am trying

$ PATH=/opt/ghc/ghc-9.8.1/bin:$PATH stack install
...
Error: [S-4804]
       Stack failed to construct a build plan.
       
       While constructing the build plan, Stack encountered the following errors. The 'Stack configuration' refers to the set of
       package versions specified by the snapshot (after any dropped packages, or pruned GHC boot packages; if a boot package is
       replaced, Stack prunes all other such packages that depend on it) and any extra-deps:
       
       In the dependencies for liquidhaskell-boot-0.9.6.3:
         * liquid-fixpoint must match ==0.9.6.3, but liquid-fixpoint-0.9.4.7 is in the Stack configuration (latest matching
           version is 0.9.6.3).
       needed since liquidhaskell-boot is a build target.

and

$ cabal install -w /opt/ghc/ghc-9.8.1/bin/ghc liquid-platform
Error: cabal: Could not resolve dependencies:
[__0] next goal: liquid-fixpoint (user goal)
[__0] rejecting: liquid-fixpoint-0.9.6.3 (constraint from user target requires
==0.9.4.7)
[__0] trying: liquid-fixpoint-0.9.4.7
[__1] next goal: liquidhaskell-boot (user goal)
[__1] rejecting: liquidhaskell-boot-0.9.6.3 (conflict:
liquid-fixpoint==0.9.4.7, liquidhaskell-boot => liquid-fixpoint==0.9.6.3)
[__1] rejecting: liquidhaskell-boot-0.9.4.7.0, liquidhaskell-boot-0.9.2.8.0,
liquidhaskell-boot-0.9.2.5.0 (constraint from user target requires ==0.9.6.3)

[facundominguez]

head liquid-fixpoint/liquid-fixpoint.cabal should show version 0.9.6.3. If that's not the case, it may be fixed by git submodule update.

[jwaldmann]

Now,

$ PATH=/opt/ghc/ghc-9.8.1/bin:$PATH stack install
...
prover-ple-lib                   > *** WriteIface [.stack-work/dist/x86_64-linux/ghc-9.8.1/build/Helper.dyn_hi]:
prover-ple-lib                   > *** systool:as:
liquid-platform                  > Installing executable liquidhaskell in /home/waldmann/software/constraint/liquidhaskell/.stack-work/install/x86_64-linux/51d6dd043fe4fc1350590b6678d4751c58dbf20ac98665576bbb3a0dc2350f87/9.8.1/bin
prover-ple-lib                   >               
prover-ple-lib                   > copy/register
prover-ple-lib                   > Installing library in /home/waldmann/software/constraint/liquidhaskell/.stack-work/install/x86_64-linux/51d6dd043fe4fc1350590b6678d4751c58dbf20ac98665576bbb3a0dc2350f87/9.8.1/lib/x86_64-linux-ghc-9.8.1/prover-ple-lib-0.1.0.0-3KxWv8GiLgY1qUAsIcbT4J
prover-ple-lib                   > Error: Cabal-simple_9p6GVs8J_3.10.2.0_ghc-9.8.1:
prover-ple-lib                   > '/opt/ghc/ghc-9.8.1/bin/ghc-9.8.1' exited with an error:
prover-ple-lib                   > <command line>: Could not find module ‘LiquidHaskell’.
prover-ple-lib                   > Use -v to see a list of the files searched for.
prover-ple-lib                   > 
Completed 139 action(s).        

Error: [S-7282]
       Stack failed to execute the build plan.

And

$ cabal install -w /opt/ghc/ghc-9.8.1/bin/ghc liquid-platform
...
Completed    liquid-platform-0.9.2.8 (exe:liquidhaskell)
Copying 'liquidhaskell' to '/home/waldmann/.cabal/bin/liquidhaskell'

Yay! I guess? But then -

$ PATH=/opt/ghc/ghc-9.8.1/bin:$PATH liquidhaskell  -v
Glasgow Haskell Compiler, Version 9.8.1, stage 2 booted by GHC version 9.6.3
<command line>: cannot satisfy -plugin-package liquidhaskell
    (use -v for more information)

I am able to load this package in ghci (I think)

$ /opt/ghc/ghc-9.8.1/bin/ghci
GHCi, version 9.8.1: https://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/waldmann/software/constraint/liquidhaskell/.ghci
λ> :set -package liquidhaskell
package flags have changed, resetting and loading new packages...
λ> :set -plugin-package liquidhaskell
package flags have changed, resetting and loading new packages...

[facundominguez]

The liquidhaskell executable is not well supported and it is not intended to be used standalone (without stack or cabal-install).

But then -

It is unclear to me what you are trying to accomplish. Testing Liquid Haskell entails writing a cabal package that uses the plugin. Like here.

If you don't want to write a cabal package, then this might work:

# from the LH root folder
$ stack exec -- ghc -fplugin=LiquidHaskell FILE.hs

Or installing liquidhaskell first.

$ cabal install --lib liquidhaskell
$ ghc -package base -fplugin=LiquidHaskell FILE.hs

Or just run some of the automated tests

$ scripts/test/test_plugin.sh basic-pos

[jwaldmann]

unclear to me what you are trying to accomplish

running (and then perhaps modifying) a minimal liquidhaskell example to see (and show to my students, lecture "constraint programming") how SMT is used for software analysis (#2259)

As for running, this seems fine now:

$ /opt/ghc/ghc-9.8.1/bin/ghc -fforce-recomp -package base -fplugin=LiquidHaskell tests/neg/Fail.hs 
Loaded package environment from /home/waldmann/.ghc/x86_64-linux-9.8.1/environments/default
[1 of 1] Compiling Fail             ( tests/neg/Fail.hs, tests/neg/Fail.o )

**** LIQUID: UNSAFE ************************************************************

A crude way of running z3 on the generated constraint:

cat tests/neg/.liquid/Fail.hs.smt2 |sed -e 's/Str/String/g' -e 's/strLen/str.len/g' | z3 /dev/stdin 
unsat
sat

if confirms what's in the file ("SMT Says Unsat", "SMT Says Sat").

I do get lots of failures, e.g., Illegal type specification for Even.notEven, Unknown type constructor Nat (for pos/GCD). Is this supposed to work? Do you want this reported?

[facundominguez]

Is this supposed to work?

If "this" means running ghc with the plugin directly on source files instead of using cabal or stack, it is likely to fail for reasons other than bugs in Liquid Haskell. But we can analyse some of the failures if you really need to run ghc directly and understanding the failures is helpful.

[jwaldmann]

really need to run ghc directly ...

"need" ... it seems like the most direct thing to do. By analogy - if I want to demonstrate (in a lecture) some Hindley/Milner types, I start ghci. If I want to demonstrate some refinement types, I start ... ghc with the plugin? Writing a cabal file is not the first thing that comes to mind.

we can analyse some of the failures

Thanks. I will submit one or two, then you could perhaps indicate what's happening

#2263 #2264

[facundominguez]

I cannot reproduce either of those failures. Verification passes fine for me. Which hints at differences in the installation or the environment. Do they fail as well if you run ghc with stack:

stack exec -- ghc -fplugin=LiquidHaskell tests/pos/GCD.hs

?

[jwaldmann]

yes, works via stack. I updated and closed the two issues. Thanks.

[facundominguez]

I'm closing this as I think all questions have been addressed. @jwaldmann, please, let me know if I dropped anything, and feel free to open more issues.