Merge pull request #27 from facundominguez/fd/all-ghcs

Build with all the supported ghc's

.github/workflows/cabal.yml

@@ -10,9 +10,17 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        cabal: ["3.6"]
+        cabal: ["3.10.3.0"]
         ghc:
-          - "9.2.5"
+          - "9.2.8"
+          - "9.4.7"
+          - "9.6.3"
+        include:
+          - repo: "hackage"
+          - ghc: "9.8.1"
+            repo: "github"
+          - ghc: "9.8.1"
+            repo: "hackage"
 
     steps:
       - uses: actions/checkout@v3
@@ -25,19 +33,29 @@ jobs:
           version: "4.8.7"
 
       - name: Setup GHC and cabal-install
-        uses: haskell/actions/setup@v2
+        uses: haskell-actions/setup@v2
         with:
           ghc-version: ${{ matrix.ghc }}
           cabal-version: ${{ matrix.cabal }}
 
+      - name: Configure the build
+        run: |
+          if [ ${{ matrix.repo }} == "github" ]
+          then
+            cp cabal.project.github cabal.project
+          fi
+          cabal configure --enable-tests --enable-benchmarks --disable-documentation
+          # generate dist-newstyle/cache/plan.json
+          cabal build all --dry-run
+
       - name: Cache ~/.cabal/packages, ~/.cabal/store and dist-newstyle
         uses: actions/cache@v3
         with:
           path: |
             ~/.cabal/packages
             ~/.cabal/store
             dist-newstyle
-          key: ${{ runner.os }}-${{ matrix.ghc }}-cabal-${{ hashFiles('**/*.cabal', '**/cabal.project', '**/cabal.project.freeze') }}
+          key: ${{ runner.os }}-${{ matrix.ghc }}-cabal-${{ hashFiles('**/*.cabal', './dist-newstyle/cache/plan.json') }}
 
       - name: Update package list
         run: cabal update

.github/workflows/stack.yml

@@ -6,14 +6,21 @@ on:
 
 jobs:
   build:
-    name: ghc ${{ matrix.ghc }}
+    name: ghc ${{ matrix.ghc }} - ${{ matrix.repo }}
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        cabal: ["3.6"]
+        cabal: ["3.10.3.0"]
         ghc:
-          - "9.2.5"
-          - "9.0.2"
+          - "9.2.8"
+          - "9.4.7"
+          - "9.6.3"
+        include:
+          - repo: "hackage"
+          - ghc: "9.8.1"
+            repo: "github"
+          - ghc: "9.8.1"
+            repo: "hackage"
 
     steps:
       - uses: actions/checkout@v3
@@ -26,20 +33,29 @@ jobs:
           version: "4.8.7"
 
       - name: Setup Stack
-        uses: haskell/actions/setup@v2
+        uses: haskell-actions/setup@v2
         with:
           ghc-version: ${{ matrix.ghc }}
           cabal-version: ${{ matrix.cabal }}
           enable-stack: true
           stack-version: "latest"
 
+      - name: Configure the build
+        run: |
+          if [ ${{ matrix.repo }} == "hackage" ]
+          then
+            sed "s/\.\././g" ./stack/stack-${{ matrix.ghc }}.yaml > stack.yaml
+          fi
+          # generate stack.yaml.lock
+          stack build --no-terminal --dry-run
+
       - name: Cache ~/.stack and .stack-work
         uses: actions/cache@v3
         with:
           path: |
             ~/.stack
             .stack-work
-          key: ${{ runner.os }}-${{ matrix.ghc }}-stack-${{ hashFiles('**/*.cabal', './stack/stack-${{ matrix.ghc }}.yaml', './stack/stack-${{ matrix.ghc }}.yaml.lock') }}
+          key: ${{ runner.os }}-${{ matrix.ghc }}-stack-${{ hashFiles('**/*.cabal', './stack.yaml', './stack.yaml.lock') }}
 
       - name: Build
-        run: stack build --no-terminal --stack-yaml=./stack/stack-${{ matrix.ghc }}.yaml
+        run: stack build --no-terminal

README.md

@@ -11,14 +11,18 @@ This repo demonstrates how to use [LiquidHaskell](https://github.com/ucsd-progsy
 
 - how to point `stack` at the relevant LH repositories on **github**
 
-[stack/stack-9.0.2.yaml](stack/stack-9.0.2.yaml) shows
+[stack/stack-*.yaml](stack/) shows
 
 - how to point `stack` at the relevant LH packages on **hackage**
 
-[cabal.project](cabal.project) shows
+[cabal.project.github](cabal.project.github) shows
 
 - how to point `cabal` to the relevant LH repositories on **github**
-- only works with ghc-9.2.5
+- only works with ghc-9.8.1
+
+No `cabal.project` file is needed for the releases of `liquidhaskell` in hackage.
+`cabal-install` should pick the appropriate version for each compiler (supported GHCs:
+9.2.8, 9.4.7, 9.6.3, 9.8.1)
 
 ## GHCi Integration
 

cabal.project → cabal.project.github

@@ -1,12 +1,13 @@
 packages: .
 
+
 source-repository-package
     type: git
     location: https://github.com/ucsd-progsys/liquidhaskell
-    tag: fc4a89b91fad8b7a02b72901381d4358a470e230
+    tag: 4b20537529b2143cab0214564422c94fb93df9d9
     subdir: . liquidhaskell-boot liquid-prelude liquid-vector
 
 source-repository-package
     type: git
     location: https://github.com/ucsd-progsys/liquid-fixpoint
-    tag: eb339f9abdf073f8d9f0c446c309006fdf49ed42
+    tag: 5b39f1a3c49190f9e438f9cdefd7d2635c5bf7f2

lh-plugin-demo.cabal

@@ -22,15 +22,8 @@ library
   build-depends:
       liquid-prelude,
       liquid-vector,
-      liquidhaskell
-  if impl(ghc >= 9.2)
-    build-depends:
+      liquidhaskell,
       base,
       containers,
       vector
-  else
-    build-depends:
-      liquid-base,
-      liquid-containers
   default-language: Haskell2010
-  ghc-options: -fplugin=LiquidHaskell

src/Demo/Client.hs

@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+
 {-@ LIQUID "--reflection"     @-}
 {-@ LIQUID "--ple"            @-}
 {-@ LIQUID "--no-termination" @-}
@@ -23,4 +25,3 @@ testProof :: Proof
 testProof =
   test A ==. Just True
   *** QED
-

src/Demo/Erase.hs

@@ -1,3 +1,4 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
 {-@ LIQUID "--reflection" @-}
 {-@ LIQUID "--ple"        @-}
 

src/Demo/Lib.hs

@@ -1,3 +1,5 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+
 module Demo.Lib where
 
 import Data.Set
@@ -16,7 +18,7 @@ elts (x:xs) = singleton x `union` elts xs
 
 {-@ rev :: xs:_ -> {v:_ | elts v == elts xs} @-}
 rev :: [a] -> [a]
-rev = go [] 
+rev = go []
   where
     {-@ go :: acc:_ -> xs:_ -> {v:_ | elts v == union (elts acc) (elts xs)} @-}
     go acc []     = acc

stack.yaml

@@ -1,20 +1,23 @@
-resolver: lts-20.1
+# resolver: lts-20.1
+resolver: nightly-2024-01-26
+
 packages:
   - .
 extra-deps:
-  - hashable-1.3.5.0
-  - rest-rewrite-0.4.1
-  - smtlib-backends-0.3
-  - smtlib-backends-process-0.3
+  - store-0.7.18@sha256:af32079e0d31413b97a1759f8ad8555507857cd4ac4015e195fb5b0a27a3ce9f,8159
+  - store-core-0.4.4.7@sha256:a2ea427ff0dde30252474dcb0641cb6928cb8a93cd5ee27d4c22adba8e729683,1489
+  - rest-rewrite-0.4.3
+  - smtlib-backends-0.3@rev:2
+  - smtlib-backends-process-0.3@rev:2
   - git: https://github.com/ucsd-progsys/liquidhaskell
-    commit: fc4a89b91fad8b7a02b72901381d4358a470e230
+    commit: 4b20537529b2143cab0214564422c94fb93df9d9
     subdirs:
       - .
       - liquidhaskell-boot
       - liquid-prelude
       - liquid-vector
   - git: https://github.com/ucsd-progsys/liquid-fixpoint
-    commit: eb339f9abdf073f8d9f0c446c309006fdf49ed42
+    commit: 5b39f1a3c49190f9e438f9cdefd7d2635c5bf7f2
 
 nix:
   packages: [cacert, git, hostname, z3]

stack/stack-9.2.8.yaml

@@ -0,0 +1,15 @@
+resolver: lts-20.26
+packages:
+  - ..
+extra-deps:
+  - rest-rewrite-0.4.3
+  - smtlib-backends-0.3
+  - smtlib-backends-process-0.3
+  - liquidhaskell-0.9.2.8.0
+  - liquidhaskell-boot-0.9.2.8.0
+  - liquid-fixpoint-0.9.2.5
+  - liquid-prelude-0.9.2.8.1
+  - liquid-vector-0.12.3.1.2
+
+nix:
+  packages: [cacert, git, hostname, z3]

stack/stack-9.4.7.yaml

@@ -0,0 +1,15 @@
+resolver: lts-21.21
+packages:
+  - ..
+extra-deps:
+  - rest-rewrite-0.4.3
+  - smtlib-backends-0.3
+  - smtlib-backends-process-0.3
+  - liquidhaskell-0.9.4.7.0
+  - liquidhaskell-boot-0.9.4.7.0
+  - liquid-fixpoint-0.9.4.7
+  - liquid-prelude-0.9.2.8.1
+  - liquid-vector-0.12.3.1.2
+
+nix:
+  packages: [cacert, git, hostname, z3]