ucsd-progsys · nikivazou · Oct 31, 2023 · Jul 28, 2023 · Jul 28, 2023 · Jul 28, 2023
diff --git a/.circleci/config.yml b/.circleci/config.yml
@@ -116,7 +116,7 @@ commands:
           command: |
             wget -qO- https://get.haskellstack.org/ | sudo sh
             stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> setup
-            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> build -j4 --only-dependencies --test --no-run-tests << parameters.extra_build_flags >> 
+            stack --no-terminal --stack-yaml << parameters.stack_yaml_file >> build -j4 --only-dependencies --test --no-run-tests << parameters.extra_build_flags >>
       - save_cache:
           key: stack-cache-v1-{{ checksum "<< parameters.stack_yaml_file >>" }}-{{ checksum "liquidhaskell-boot/liquidhaskell-boot.cabal" }}-{{ checksum "liquidhaskell.cabal" }}-{{ checksum "liquid-fixpoint-commit" }}
           paths:
@@ -158,7 +158,7 @@ jobs:
       image: ubuntu-2004:202107-02
     steps:
       - cabal_build_and_test:
-          ghc_version: "9.2.5"
+          ghc_version: "9.2.8"
 
 workflows:
   version: 2

diff --git a/CHANGES.md b/CHANGES.md
@@ -1,6 +1,8 @@
 # Changes
 
-## NEXT 0.9.XX
+## 0.9.2.8.0
+
+- Support for GHC 9.2.8
 
 ## 0.9.2.5
 

diff --git a/README.md b/README.md
@@ -165,14 +165,15 @@ On each line, the report will contain the time taken by each test.
 Comparison charts in `svg` format can be generated by invoking
 
 ```
-cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 -f "benchmark" -o outdir
+cabal v2-run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 -f "benchmark"
 ```
 
 This will generate three files `filtered.svg` (a subset of tests with a `benchmark` prefix, enabled by the `-f` option),
-`top.svg` and `bot.svg` (top 50 speedups and slowdowns over the entire test set, both enabled by the `-s` option) under
-the `outdir` directory. The `-f` and `-s` options can be used/omitted independently. If both are omitted, a single
-`perf.svg` will be produced covering the full input test set. Additionally, their effects can be combined by providing
-a third `-c` option (this will produce 2 files `filtered-top.svg` and `filtered-bot.svg` instead of 3).
+`top.svg` and `bot.svg` (top 50 speedups and slowdowns over the entire test set, both enabled by the `-s` option) in the
+current directory. The `-f` and `-s` options can be used/omitted independently. If both are omitted, a single `perf.svg`
+will be produced covering the full input test set. Additionally, their effects can be combined by providing a third `-c`
+option (this  will produce 2 files `filtered-top.svg` and `filtered-bot.svg` instead of 3). An optional key `-o` can be
+supplied to specify an output directory for the generated files.
 
 There is also a legacy script `scripts/plot-performance/chart_perf.sh` that can be used to generate comparison charts
 in both `svg` and `png` formats. It requires [gnuplot](http://www.gnuplot.info/) to run and assumes both files contain
@@ -357,14 +358,14 @@ using**.
 [BareSpec]:            liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L362
 [LiftedSpec]:          liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L559
 [TargetSrc]:           liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Specs.hs#L158
-[Ghc monad]:           https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:Ghc
-[HscEnv]:              https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:HscEnv
-[DynFlags]:            https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:DynFlags
-[GhcMonad]:            https://hackage.haskell.org/package/ghc-9.2.5/docs/GHC.html#t:GhcMonad
+[Ghc monad]:           https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:Ghc
+[HscEnv]:              https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:HscEnv
+[DynFlags]:            https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:DynFlags
+[GhcMonad]:            https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC.html#t:GhcMonad
 [typechecking phase]:  liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L211-L226
 [ghcide]:              https://github.com/haskell/ghcide
 [findRelevantSpecs]:   liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin/SpecFinder.hs#L65
-[core binds]:          https://hackage.haskell.org/package/ghc-9.2.5/docs/CoreSyn.html#t:CoreBind
+[core binds]:          https://hackage.haskell.org/package/ghc-9.2.8/docs/GHC-Core.html#t:CoreBind
 [configureGhcTargets]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L254
 [processTargetModule]: liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Interface.hs#L483
 [processModule]:       liquidhaskell-boot/src/Language/Haskell/Liquid/GHC/Plugin.hs#L509

diff --git a/cabal.project b/cabal.project
@@ -1,4 +1,4 @@
-with-compiler: ghc-9.2.5
+with-compiler: ghc-9.2.8
 
 packages: .
           ./liquid-fixpoint

diff --git a/docs/mkDocs/docs/install.md b/docs/mkDocs/docs/install.md
@@ -19,6 +19,7 @@ LiquidHaskell itself is installed&enabled by adding it as a dependency in your p
 
 Depending on your version of GHC, you might want to use a build of LiquidHaskell from github or from Hackage.
 
+* `ghc-9.2.8`: use LiquidHaskell from github
 * `ghc-9.2.5`: use liquidhaskell-0.9.2.5.0 from Hackage
 * `ghc-9.0.2`: use liquidhaskell-0.9.0.2.1 and liquid-base-0.4.15.1.0 from Hackage
 * `ghc-8.10.7`: use liquidhaskell-0.8.10.7 and liquid-base-0.4.15.0.0 from Hackage

diff --git a/liquid-parallel/liquid-parallel.cabal b/liquid-parallel/liquid-parallel.cabal
@@ -20,7 +20,7 @@ library
   hs-source-dirs:     src
   build-depends:      base          < 5
                     , parallel             >= 3.2.2.0 && < 3.3
-                    , liquidhaskell        >= 0.9.2.5
+                    , liquidhaskell        >= 0.9.2.8
   default-language:   Haskell2010
   default-extensions: PackageImports
   if impl(ghc >= 8.10)

diff --git a/liquid-platform/liquid-platform.cabal b/liquid-platform/liquid-platform.cabal
@@ -1,6 +1,6 @@
 cabal-version:      1.22
 name:               liquid-platform
-version:            0.9.2.5
+version:            0.9.2.8
 synopsis:           A battery-included platform for LiquidHaskell
 description:        A battery-included platform for LiquidHaskell.
 license:            BSD3
@@ -27,10 +27,10 @@ executable liquidhaskell
     buildable: True
     build-depends:      base       >= 4.15.1.0 && < 5
                       , containers >= 0.6.4.1  && < 0.7
-                      , liquid-prelude    >= 0.9.2.5
+                      , liquid-prelude    >= 0.9.2.8
                       , liquid-vector     >= 0.12.3.1.2
-                      , liquidhaskell     >= 0.9.2.5
-                      , liquidhaskell-boot >= 0.9.2.5
+                      , liquidhaskell     >= 0.9.2.8
+                      , liquidhaskell-boot >= 0.9.2.8
                       , filepath
                       , process           >= 1.6.0.0 && < 1.7
                       , cmdargs           >= 0.10    && < 0.11

diff --git a/liquid-prelude/liquid-prelude.cabal b/liquid-prelude/liquid-prelude.cabal
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-prelude
-version:            0.9.2.5
+version:            0.9.2.8
 synopsis:           General utility modules for LiquidHaskell
 description:        General utility modules for LiquidHaskell.
 license:            BSD3
@@ -31,7 +31,7 @@ library
                     , ghc-prim
                     , bytestring           >= 0.10.12.1 && < 0.12
                     , containers           >= 0.6.4.1  && < 0.7
-                    , liquidhaskell        >= 0.9.2.5
+                    , liquidhaskell        >= 0.9.2.8
   default-language:   Haskell2010
   if impl(ghc >= 8.10)
     ghc-options: -fplugin=LiquidHaskell
diff --git a/liquid-vector/liquid-vector.cabal b/liquid-vector/liquid-vector.cabal
@@ -20,7 +20,7 @@ library
   hs-source-dirs:     src
   build-depends:      base          < 5
                     , vector               >= 0.12.3.1 && < 0.14
-                    , liquidhaskell        >= 0.9.2.5
+                    , liquidhaskell        >= 0.9.2.8
   default-language:   Haskell2010
   default-extensions: PackageImports
   if impl(ghc >= 8.10)

diff --git a/liquidhaskell-boot/liquidhaskell-boot.cabal b/liquidhaskell-boot/liquidhaskell-boot.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquidhaskell-boot
-version:            0.9.2.5.0
+version:            0.9.2.8.0
 synopsis:           Liquid Types for Haskell
 description:        This package provides a plugin to verify Haskell programs.
                     But most likely you should be using the [liquidhaskell package](https://hackage.haskell.org/package/liquidhaskell)
@@ -13,7 +13,7 @@ maintainer:         Ranjit Jhala <[email protected]>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
 build-type:         Simple
-tested-with:        GHC == 9.2.5
+tested-with:        GHC == 9.2.8
 
 data-files:         include/CoreToLogic.lg
                     syntax/liquid.css

diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Equality.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Types/Equality.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE FlexibleInstances    #-}
 
--- Syntactic Equality of Types up tp forall type renaming
+-- Syntactic Equality of Types up to forall type renaming
 
 module Language.Haskell.Liquid.Types.Equality where
 

diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal
@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               liquidhaskell
-version:            0.9.2.5.0
+version:            0.9.2.8.0
 synopsis:           Liquid Types for Haskell
 description:        Liquid Types for Haskell.
 license:            BSD-3-Clause
@@ -11,7 +11,7 @@ maintainer:         Ranjit Jhala <[email protected]>
 category:           Language
 homepage:           https://github.com/ucsd-progsys/liquidhaskell
 build-type:         Custom
-tested-with:        GHC == 9.2.5
+tested-with:        GHC == 9.2.8
 extra-source-files: CHANGES.md
                     README.md
 
@@ -77,9 +77,9 @@ library
   hs-source-dirs:     src
 
   build-depends:      base                 >= 4.11.1.0 && < 5,
-                      liquidhaskell-boot   == 0.9.2.5.0,
-                      bytestring == 0.11.3.1,
-                      containers == 0.6.5.1,
+                      liquidhaskell-boot   == 0.9.2.8.0,
+                      bytestring           == 0.11.4.0,
+                      containers           == 0.6.5.1,
                       ghc-prim
   default-language:   Haskell98
   ghc-options:        -Wall -fplugin=LiquidHaskellBoot

diff --git a/src/Data/ByteString_LHAssumptions.hs b/src/Data/ByteString_LHAssumptions.hs
@@ -12,6 +12,8 @@ invariant { bs : Data.ByteString.ByteString  | 0 <= bslen bs }
 
 invariant { bs : Data.ByteString.ByteString | bslen bs == stringlen bs }
 
+assume Data.ByteString.Internal.Type.empty :: { bs : Data.ByteString.ByteString | bslen bs == 0 }
+
 assume Data.ByteString.singleton :: _ -> { bs : Data.ByteString.ByteString | bslen bs == 1 }
 
 assume Data.ByteString.pack :: w8s : [_]

diff --git a/src/GHC/Types_LHAssumptions.hs b/src/GHC/Types_LHAssumptions.hs
@@ -26,15 +26,15 @@ embed GHC.Prim.Addr#    as Str
 embed GHC.Integer.Type.Integer as int
 embed GHC.Num.Integer as int
 
-assume GHC.Types.True  :: {v:GHC.Types.Bool | v     }
-assume GHC.Types.False :: {v:GHC.Types.Bool | (~ v) }
-assume GHC.Types.isTrue#  :: n:_ -> {v:GHC.Types.Bool | (n = 1 <=> v)}
+assume GHC.Types.True    :: {v:GHC.Types.Bool | v     }
+assume GHC.Types.False   :: {v:GHC.Types.Bool | (~ v) }
+assume GHC.Types.isTrue# :: n:_ -> {v:GHC.Types.Bool | (n = 1 <=> v)}
 
 assume GHC.Types.D# :: x:GHC.Prim.Double# -> {v: GHC.Types.Double | v = (x :: real) }
 assume GHC.Types.F# :: x:GHC.Prim.Float# -> {v: GHC.Types.Float | v = (x :: real) }
 assume GHC.Types.I# :: x:GHC.Prim.Int# -> {v: GHC.Types.Int | v = (x :: int) }
 assume GHC.Types.C# :: x:GHC.Prim.Char# -> {v: GHC.Types.Char | v = (x :: Char) }
-assume GHC.Types.W# :: w:_ -> {v:GHC.Types.Word | v == w }
+assume GHC.Types.W# :: w:GHC.Prim.Word# -> {v:GHC.Types.Word | v == w }
 
 measure addrLen :: GHC.Prim.Addr# -> GHC.Types.Int
 

diff --git a/stack.yaml b/stack.yaml
@@ -31,7 +31,7 @@ extra-deps:
 # for tests
 - strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628
 
-resolver: lts-20.1
+resolver: lts-20.26
 
 nix:
   packages: [cacert, git, hostname, z3]

diff --git a/stack.yaml.lock b/stack.yaml.lock
@@ -5,12 +5,12 @@
 
 packages:
 - completed:
-    hackage: hashable-1.3.5.0@sha256:3a2beeafb220f9de706568a7e4a5b3c762cc4c9f25c94d7ef795b8c2d6a691d7,4240
+    hackage: hashable-1.4.2.0@sha256:585792335d5541dba78fa8dfcb291a89cd5812a281825ff7a44afa296ab5d58a,4520
     pantry-tree:
-      sha256: 4df2f6b536a0fcc5f7d562cb29e373f27dc4a2747452ac5cc74c1599cab22fc5
+      sha256: 792a6cab3f15c5db29d759c8ca735d0be5f4c94f363329652f8b9780009d0829
       size: 1248
   original:
-    hackage: hashable-1.3.5.0
+    hackage: hashable-1.4.2.0
 - completed:
     hackage: rest-rewrite-0.4.1@sha256:1254960c0a595cf4c9d5a3b986f42644407c63c74578d75b3568a6a12e5143f0,3886
     pantry-tree:
@@ -52,7 +52,7 @@ packages:
     hackage: strip-ansi-escape-0.1.0.0@sha256:08f2ed93b16086a837ec46eab7ce8d27cf39d47783caaeb818878ea33c2ff75f,1628
 snapshots:
 - completed:
-    sha256: b73b2b116143aea728c70e65c3239188998bac5bc3be56465813dacd74215dc5
-    size: 648424
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/1.yaml
-  original: lts-20.1
+    sha256: 5a59b2a405b3aba3c00188453be172b85893cab8ebc352b1ef58b0eae5d248a2
+    size: 650475
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/20/26.yaml
+  original: lts-20.26