liquidhaskell 0.9.8.1 → 0.9.8.2
raw patch · 7 files changed
+37/−54 lines, 7 filesdep ~bytestringdep ~liquidhaskell-boot
Dependency ranges changed: bytestring, liquidhaskell-boot
Files
- CHANGES.md +10/−0
- README.md +19/−42
- liquidhaskell.cabal +4/−4
- src/GHC/Num/Integer_LHAssumptions.hs +1/−1
- src/GHC/Num_LHAssumptions.hs +2/−3
- src/GHC/Types_LHAssumptions.hs +1/−2
- src/Prelude_LHAssumptions.hs +0/−2
CHANGES.md view
@@ -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)
README.md view
@@ -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 <test-group-name1> <test-group-name2> ...+ $ ./scripts/test/test_plugin.sh <test-group-name1> <test-group-name2> ... 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:<test-group-name> --ghc-options=-fplugin-opt=LiquidHaskell:--no-termination+ $ cabal build tests:<test-group-name> --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.
liquidhaskell.cabal view
@@ -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
src/GHC/Num/Integer_LHAssumptions.hs view
@@ -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) } @-}
src/GHC/Num_LHAssumptions.hs view
@@ -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
src/GHC/Types_LHAssumptions.hs view
@@ -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) }
src/Prelude_LHAssumptions.hs view
@@ -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