diff --git a/.circleci/config.yml b/.circleci/config.yml index 34b0fa761c..7a885dab31 100644 --- 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 index c9d98efea5..acc7584a2d 100644 --- 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 index 468dad4109..7322c6ad23 100644 --- 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 index bf01541083..29dbe99433 100644 --- 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 index add4802376..5fefbd3d76 100644 --- 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 index 13d1696557..94ac5490c1 100644 --- 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 index 6ff08bcee1..9a95ccc9eb 100644 --- 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 index d75f15416a..4288ae47e3 100644 --- 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 index e313e1d4df..931eaa1a3f 100644 --- 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 index 60c8a80f27..2c1118cae9 100644 --- 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 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 index 7a85e739bb..031bec9623 100644 --- 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 index 1e67904201..f9157478a9 100644 --- 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 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 index f4618e7f6a..562ddd4d64 100644 --- 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 index 9f48379298..ac15559ecd 100644 --- 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 index e67c5293f5..8a48386668 100644 --- 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 index 5816ee9712..b751e350be 100644 --- 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