diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -2,10 +2,20 @@ ## Next +## 0.9.8.2 (2024-08-21) + +- Support for GHC 9.8.2. +- Implement assume-reflect, a feature to assume the reflection of functions in dependencies [2313](https://github.com/ucsd-progsys/liquidhaskell/pull/2313). +- Fixed the polymorphism-related crash in liquid-fixpoint caused by a restrictive theory encoding [#2272](https://github.com/ucsd-progsys/liquidhaskell/issues/2272). + ## 0.9.8.1 (2024-02-05) - Set support for GHC 9.8.1 [#2248](https://github.com/ucsd-progsys/liquidhaskell/pull/2248) - Embedded files `include/CoreToLogic.lg` and `syntax/liquid.css` in the source code [#2265](https://github.com/ucsd-progsys/liquidhaskell/issues/2265) + +## 0.9.6.3.1 (2024-03-07) + +- Avoid enabling plugins in ghc-options (workaround for #9375) ## 0.9.6.3 (2024-01-29) diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -56,62 +56,39 @@ cabal exec ghc -- -fplugin=LiquidHaskell FILE.hs ``` -## Fast (re)compilation - -When working on the `liquidhaskell-boot` library, usually all we want is to make changes and quickly recompile -only the bare minimum, to try out new ideas. Using a fully-fledged GHC plugin doesn't help in this sense, -because packages like `liquidhaskell` or `liquid-prelude` have a direct dependency on `liquidhaskell-boot`, and -therefore every time the latter changes, an expensive rebuild of those packages is triggered, which -might become tedious overtime. To mitigate this, we offer a faster, "dev-style" build mode which is based -on the assumption that most changes to the `liquidhaskell` library do not alter the validity of -already-checked libraries, and therefore things like `liquid-prelude` can be considered -"static assets", avoiding the need for a recompilation. In other terms, we explicitly disable recompilation -of any of the `liquid-*` ancillary library in dev mode, so that rebuilds only affect the -`liquidhaskell-boot` library. - -### Usage and recommended workflow - -This is how you can use this: - -* To begin with, perform a **full** build of **all** the libraries, by doing either `cabal v2-build` or `stack build`, - **without** specifying any extra environment variables from the command line. This is needed to ensure that - things like `liquid-prelude` or `liquidhaskell` are compiled at least once, as we would need the - refinements they contain to correctly checks other downstream programs; - -* At this point, the content of the `liquid-*` packages is considered "trusted" and "frozen", until you won't - force another full, _non-dev_ build; - -* In order to quickly test changes to the `liquidhaskell-boot` library without recompiling the `liquid-*` packages, - we need to start a build passing the `LIQUID_DEV_MODE` env var as part of the build command. Examples: +## Building -#### Stack +### Stack ``` -LIQUID_DEV_MODE=true stack build +stack build ``` If on NixOS ``` -LIQUID_DEV_MODE=true stack --no-nix-pure build +stack --no-nix-pure build ``` With the above, `stack` will unregister and re-register the libraries, but hopefully it won't rebuild any modules. -#### Cabal +### Cabal ``` -LIQUID_DEV_MODE=true cabal v2-build +cabal v2-build ``` -It's also possible (but not recommended) to add `LIQUID_DEV_MODE` to .bashrc or similar, but this would -permanently disable building the `liquid-*` packages, and this might silently mask breaking changes to the -`liquidhaskell` library that would manifest only when compiling these other packages. +### Faster recompilation -If you wish to force building all the libraries again, it's sufficient to issue the same builds commands -without the `LIQUID_DEV_MODE`. +When changing the `liquidhaskell-boot` library, sometimes we don't want +to rebuild `liquidhaskell` or `liquid-vector` when testing the changes. +In these cases we can set the environment variable `LIQUID_DEV_MODE=true` +when running `stack` or `cabal` to skip rebuilding those packages. +DANGER: Note that this can give an invalid result if the changes to +`liquidhaskell-boot` do require rebuilding other `liquid*` packages. + ## How To Run Regression Tests For documentation on the `test-driver` executable itself, please refer to the @@ -124,23 +101,23 @@ You can run a bunch of particular test-groups instead by - $ LIQUID_DEV_MODE=true ./scripts/test/test_plugin.sh ... + $ ./scripts/test/test_plugin.sh ... and you can list all the possible test options with - $ LIQUID_DEV_MODE=true ./scripts/test/test_plugin.sh --help + $ ./scripts/test/test_plugin.sh --help or get a list of just the test groups, one per line, with - $ LIQUID_DEV_MODE=true ./scripts/test/test_plugin.sh --show-all + $ ./scripts/test/test_plugin.sh --show-all To pass in specific parameters, you can invoke cabal directly with - $ LIQUID_DEV_MODE=true cabal build tests: --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination + $ cabal build tests: --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination For example: - $ LIQUID_DEV_MODE=true cabal build tests:unit-neg --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination + $ cabal build tests:unit-neg --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination Or your favorite number of threads, depending on cores etc. diff --git a/liquidhaskell.cabal b/liquidhaskell.cabal --- a/liquidhaskell.cabal +++ b/liquidhaskell.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell -version: 0.9.8.1 +version: 0.9.8.2 synopsis: Liquid Types for Haskell description: Liquid Types for Haskell. license: BSD-3-Clause @@ -11,7 +11,7 @@ category: Language homepage: https://github.com/ucsd-progsys/liquidhaskell build-type: Custom -tested-with: GHC == 9.6.3 +tested-with: GHC == 9.8.2 extra-doc-files: CHANGES.md README.md @@ -78,8 +78,8 @@ hs-source-dirs: src build-depends: base >= 4.11.1.0 && < 5, - liquidhaskell-boot == 0.9.8.1, - bytestring == 0.12.0.2, + liquidhaskell-boot == 0.9.8.2, + bytestring == 0.12.1.0, containers == 0.6.8, ghc-bignum, ghc-prim diff --git a/src/GHC/Num/Integer_LHAssumptions.hs b/src/GHC/Num/Integer_LHAssumptions.hs --- a/src/GHC/Num/Integer_LHAssumptions.hs +++ b/src/GHC/Num/Integer_LHAssumptions.hs @@ -9,5 +9,5 @@ {-@ -assume GHC.Num.Integer.IS :: x:GHC.Prim.Int# -> {v: GHC.Num.Integer | v = (x :: int) } +assume GHC.Num.Integer.IS :: x:GHC.Prim.Int# -> {v: GHC.Num.Integer.Integer | v = (x :: int) } @-} diff --git a/src/GHC/Num_LHAssumptions.hs b/src/GHC/Num_LHAssumptions.hs --- a/src/GHC/Num_LHAssumptions.hs +++ b/src/GHC/Num_LHAssumptions.hs @@ -2,10 +2,9 @@ module GHC.Num_LHAssumptions where {-@ -embed GHC.Integer.Type.Integer as int -embed GHC.Num.Integer as int +embed GHC.Num.Integer.Integer as int -assume GHC.Num.fromInteger :: (GHC.Num.Num a) => x:Integer -> {v:a | v = x } +assume GHC.Num.fromInteger :: (GHC.Num.Num a) => x:GHC.Num.Integer.Integer -> {v:a | v = x } assume GHC.Num.negate :: (GHC.Num.Num a) => x:a diff --git a/src/GHC/Types_LHAssumptions.hs b/src/GHC/Types_LHAssumptions.hs --- a/src/GHC/Types_LHAssumptions.hs +++ b/src/GHC/Types_LHAssumptions.hs @@ -25,8 +25,7 @@ embed GHC.Prim.Char# as Char embed GHC.Prim.Addr# as Str -embed GHC.Integer.Type.Integer as int -embed GHC.Num.Integer as int +embed GHC.Num.Integer.Integer as int assume GHC.Types.True :: {v:GHC.Types.Bool | v } assume GHC.Types.False :: {v:GHC.Types.Bool | (~ v) } diff --git a/src/Prelude_LHAssumptions.hs b/src/Prelude_LHAssumptions.hs --- a/src/Prelude_LHAssumptions.hs +++ b/src/Prelude_LHAssumptions.hs @@ -14,8 +14,6 @@ assume GHC.Err.error :: {v:_ | false} -> a -// assume GHC.Integer.smallInteger :: x:GHC.Prim.Int# -> { v:GHC.Integer.Type | v = (x :: int) } - embed Integer as int predicate Max V X Y = if X > Y then V = X else V = Y