Can't figure out how to build a project with GHC 9.6.3

[lylek]

Hi folks,

I'm new to LiquidHaskell. I was able to get the LH Plugin Demo to build and run using stack. But I wanted to try making my own project, using GHC 9.6.3. The installation instructions said to add a dependency on liquidhaskell to your .cabal file, and to "follow the examples" for how to set up your stack.yaml.

Well, the LH Plugin Demo's stack.yaml references particular commits for liquidhaskell and liquid-fixpoint. So I looked up the v0.9.6.3 tag, and copied the commit ID for liquidhaskell, and used the submodule commit ID for liquid-fixpoint. But when I build with stack, it terminated with this error:

liquidhaskell     > Error: setup: '/Users/lyle/.ghcup/ghc/9.6.3/bin/ghc' exited with an error:
liquidhaskell     > <command line>: Could not find module ‘LiquidHaskellBoot’
liquidhaskell     > Use -v (or `:set -v` in ghci) to see a list of the files searched for.

This is the stack.yaml I'm using for my project:

resolver:
  url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/22/6.yaml

packages:
- .

extra-deps:
  - smtlib-backends-0.3
  - smtlib-backends-process-0.3
  - git: https://github.com/ucsd-progsys/liquidhaskell
    commit: 6aeb737d47d10734d74d193e176eef95dce65d57
    subdirs:
      - .
      - liquidhaskell-boot
      - liquid-prelude
      - liquid-vector
  - git: https://github.com/ucsd-progsys/liquid-fixpoint
    commit: 28c6d943a18d8d636385a7ff1fa10e81a7b4a0ab

In package.yaml, I just made sure to set up dependencies like this:

dependencies:
- base >= 4.7 && < 5
- liquidhaskell
- liquid-prelude

I also added -fplugin=LiquidHaskell under ghc-options.

Since that failed, I tried to work from the other direction. What if I tried to upgrade the LH Plugin Demo to GHC 9.6.3? So I copied that project, and just edited the stack.yaml. I used the same stackage resolver that was set in the stack.yaml within the liquidhaskell project (at the v0.9.6.3 tag):

resolver: nightly-2023-11-27
packages:
  - .
extra-deps:
  - smtlib-backends-0.3
  - smtlib-backends-process-0.3
  - git: https://github.com/ucsd-progsys/liquidhaskell
    commit: fc4a89b91fad8b7a02b72901381d4358a470e230
    subdirs:
      - .
      - liquidhaskell-boot
      - liquid-prelude
      - liquid-vector
  - git: https://github.com/ucsd-progsys/liquid-fixpoint
    commit: eb339f9abdf073f8d9f0c446c309006fdf49ed42

nix:
  packages: [cacert, git, hostname, z3]

That failed to build, but with a different problem... stack couldn't construct a build plan:

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 liquid-fixpoint-0.9.0.2.1:
         * vector must match <0.13, but vector-0.13.1.0 is in the Stack configuration (latest matching version is 0.12.3.1).
       needed due to lh-plugin-demo-0.1.0.0 -> liquid-fixpoint-0.9.0.2.1

       In the dependencies for liquid-vector-0.12.3.1:
         * vector must match >=0.12.3.1 && <0.13, but vector-0.13.1.0 is in the Stack configuration (latest matching version is 0.12.3.1).
       needed due to lh-plugin-demo-0.1.0.0 -> liquid-vector-0.12.3.1

       In the dependencies for liquidhaskell-0.9.2.5.0:
         * bytestring must match ==0.11.3.1, but bytestring-0.11.5.2 is in the Stack configuration (latest matching version is 0.11.3.1).
         * containers must match ==0.6.5.1, but containers-0.6.7 is in the Stack configuration (latest matching version is 0.6.5.1).
       needed due to lh-plugin-demo-0.1.0.0 -> liquidhaskell-0.9.2.5.0

       In the dependencies for liquidhaskell-boot-0.9.2.5.0:
         * Cabal must match <3.7, but Cabal-3.10.1.0 is in the Stack configuration (latest matching version is 3.6.3.0).
         * ghc must match ^>=9.2, but ghc-9.6.3 is in the Stack configuration (latest matching version is 9.2.8).
         * hashable must match >=1.3 && <1.4, but hashable-1.4.3.0 is in the Stack configuration (latest matching version is 1.3.5.0).
         * optparse-applicative must match <0.18, but optparse-applicative-0.18.1.0 is in the Stack configuration (latest matching version is 0.17.1.0).
       needed due to lh-plugin-demo-0.1.0.0 -> liquidhaskell-boot-0.9.2.5.0

What am I missing? Is there an easier way to figure out how to configure my files? Could someone please add more instructions to the documentation?

Thanks,
Lyle

[ranjitjhala]

oops, let me try to update the plugin demo to work with the latest LH!

[lylek]

oops, let me try to update the plugin demo to work with the latest LH!

That's great, thanks!

Is there a general process by which one would do this? That is, If a new LH version that comes out supporting a new GHC version, is there some straightforward way I can update my stack.yaml to use that new version?

[ranjitjhala]

Hi @lylek -- I managed to update the lh-plugin-demo so it works with stack and the latest LH and GHC 9.8.1 here:

ucsd-progsys/lh-plugin-demo#23

I can't for the life of me figure out the cabal story, sadly -- but maybe the stack will get you unstuck?

[ranjitjhala]

The general process is simply pointing stack/cabal.project to the latest GH snapshots for LH/fixpoint (as in the stack.yaml) but IdK what is going on with cabal maybe @facundominguez has a clue?

[facundominguez]

This is a bug in the cabal/GHC interaction, which does not allow to register packages which list plugins in ghc-options. We have worked around that in liquidhaskell-0.9.8.1, but not in liquidhaskell-0.9.6.3.

As far as I could check, the fix is not in the latest Cabal yet. I backported the workaround and just released it as liquidhaskell-0.9.6.3.1. Please, let us know if it still doesn't fix it for you.

[OlaoluwaM]

I'm running into the same issue it seems. I followed the repo, but I still get this error on stack build

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 hashable-1.3.5.0:
         * base must match >=4.5 && <4.17, but base-4.18.2.1 is in the Stack configuration (latest matching version is 4.16.4.0).
         * ghc-bignum must match >=1.0 && <1.1 || >=1.1 && <1.2 || >=1.2 && <1.3, but ghc-bignum-1.3 is in the Stack configuration (latest matching version is 1.2).
         * text must match >=0.12 && <1.3, but text-2.0.2 is in the Stack configuration (latest matching version is 1.2.5.0).
       The above is/are needed due to liquid-haskell-tutorial-0.1.0.0 -> hashable-1.3.5.0
       
       In the dependencies for liquid-fixpoint-0.9.0.2.1:
         * vector must match <0.13, but vector-0.13.1.0 is in the Stack configuration (latest matching version is 0.12.3.1).
       The above is/are needed due to liquid-haskell-tutorial-0.1.0.0 -> liquid-fixpoint-0.9.0.2.1
       
       In the dependencies for liquidhaskell-0.9.2.5.0:
         * bytestring must match ==0.11.3.1, but bytestring-0.11.5.3 is in the Stack configuration (latest matching version is 0.11.3.1).
         * containers must match ==0.6.5.1, but containers-0.6.7 is in the Stack configuration (latest matching version is 0.6.5.1).
       The above is/are needed due to liquid-haskell-tutorial-0.1.0.0 -> liquidhaskell-0.9.2.5.0
       
       In the dependencies for liquidhaskell-boot-0.9.2.5.0:
         * Cabal must match <3.7, but Cabal-3.10.3.0 is in the Stack configuration (latest matching version is 3.6.3.0).
         * ghc must match ^>=9.2, but ghc-9.6.5 is in the Stack configuration (latest matching version is 9.2.8).
         * optparse-applicative must match <0.18, but optparse-applicative-0.18.1.0 is in the Stack configuration (latest matching version is 0.17.1.0).
       The above is/are needed due to liquid-haskell-tutorial-0.1.0.0 -> liquidhaskell-boot-0.9.2.5.0
       
       Some different approaches to resolving some or all of this:
       
         * To ignore all version constraints and build anyway, in /home/olaolu/.stack/config.yaml (global configuration) or /home/olaolu/Desktop/labs/liquid-haskell-tutorial/stack.yaml (project-level
           configuration), set allow-newer: true.
         
         * To ignore certain version constraints and build anyway, also add these package names under allow-newer-deps: hashable, liquid-fixpoint, liquidhaskell and liquidhaskell-boot.
         
         * Build requires unattainable version of the base package. Since base is a part of GHC, you most likely need to use a different GHC version with the matching base.

Using lts-22.21

[facundominguez]

Hello @OlaoluwaM! This stack configuration works with lts-22.6, which works with ghc-9.6.3. It may serve as a basis for your configuration. Though keep in mind that we haven't tested Liquid Haskell with ghc-9.6.5.

[facundominguez]

I'm closing this issue as resolved. But please, feel free to open a new one if builds aren't working for you yet.