liquidhaskell 0.9.12.2.1 → 0.9.14.1
raw patch · 8 files changed
+67/−29 lines, 8 filesdep ~liquidhaskell-bootPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: liquidhaskell-boot
API changes (from Hackage documentation)
Files
- CHANGES.md +35/−7
- README.md +21/−9
- liquidhaskell.cabal +3/−3
- src/Data/Bits_LHAssumptions.hs +1/−1
- src/GHC/Num/Integer_LHAssumptions.hs +3/−3
- src/GHC/Real_LHAssumptions.hs +4/−4
- src/GHC/Types_LHAssumptions.hs +0/−1
- src/Prelude_LHAssumptions.hs +0/−1
CHANGES.md view
@@ -2,6 +2,34 @@ ## Next +## 0.9.14.1 (2026-05-06)++- Upgrade to GHC 9.14.1 [#2604](https://github.com/ucsd-progsys/liquidhaskell/pull/2604)+- Expand defines in define bodies, allowing defines to reference other defines [#2666](https://github.com/ucsd-progsys/liquidhaskell/pull/2666)+- Add `--modern` flag that bundles recommended defaults for new projects [#2637](https://github.com/ucsd-progsys/liquidhaskell/pull/2637)+- Rename `--exact-data-cons` to `--adt` and remove `--no-adt` [#2642](https://github.com/ucsd-progsys/liquidhaskell/pull/2642)+- Strengthen data constructor specs independently of `--adt` [#2628](https://github.com/ucsd-progsys/liquidhaskell/pull/2628)+- Always strengthen environment of case alternatives during constraint generation [#2642](https://github.com/ucsd-progsys/liquidhaskell/pull/2642)+- Only produce selectors for data constructors in use [#2642](https://github.com/ucsd-progsys/liquidhaskell/pull/2642)+- Reject conflicting selector types across constructors [#2642](https://github.com/ucsd-progsys/liquidhaskell/pull/2642)+- Add `--warn-on-term-holes` flag for typed holes support [#2486](https://github.com/ucsd-progsys/liquidhaskell/pull/2486)+- Add PLE sort-compatibility check for measure application [#2663](https://github.com/ucsd-progsys/liquidhaskell/pull/2663)+- Add Core pass to eliminate `(?)` operator after ANF [#2664](https://github.com/ucsd-progsys/liquidhaskell/pull/2664)+- Remove refinement type signature of `(?)` and document it [#2664](https://github.com/ucsd-progsys/liquidhaskell/pull/2664)+- Add support for fractional literals in the logic [#2619](https://github.com/ucsd-progsys/liquidhaskell/pull/2619)+- Add `Bool` embed always, regardless of imports [#2642](https://github.com/ucsd-progsys/liquidhaskell/pull/2642)+- Preserve dead bindings by marking Ids as exported [#2661](https://github.com/ucsd-progsys/liquidhaskell/pull/2661)+- Keep dependent binds in scope regardless of their types [#2627](https://github.com/ucsd-progsys/liquidhaskell/pull/2627)+- Fix LHAssumptions module lookup with `-plugin-package` [#2665](https://github.com/ucsd-progsys/liquidhaskell/pull/2665)+- Fix spurious invariant propagation for measures on type synonyms [#2660](https://github.com/ucsd-progsys/liquidhaskell/pull/2660)+- Fix polymorphic kvar type variable mismatch [#2649](https://github.com/ucsd-progsys/liquidhaskell/issues/2649) [#2651](https://github.com/ucsd-progsys/liquidhaskell/pull/2651)+- Fix shifted argument binding when lambda has fewer args than predicate [#2657](https://github.com/ucsd-progsys/liquidhaskell/pull/2657)+- Propagate abstract refinement predicates on parenthesized types [#2657](https://github.com/ucsd-progsys/liquidhaskell/pull/2657)+- Improve error messages for predicate arity mismatch and misplaced abstract refinement arguments [#2657](https://github.com/ucsd-progsys/liquidhaskell/pull/2657)+- Add constraint IDs to termination check error messages [#2659](https://github.com/ucsd-progsys/liquidhaskell/pull/2659)+- Add an indication of precedence to checkBind errors [#2631](https://github.com/ucsd-progsys/liquidhaskell/pull/2631)+- Remove stack support (stack.yaml removed) [#2616](https://github.com/ucsd-progsys/liquidhaskell/pull/2616)+ ## 0.9.12.2.1 (2026-01-14) - Disable LH when collecting Haddock comments and the noBackend is set [#2611](https:://github.com/ucsd-progsys/liquidhaskell/pull/2611)@@ -131,17 +159,17 @@ - Support for GHC 8.2.2 - Support for GADTs and TypeFamilies, see- - `tests/{pos,neg}/ExactGADT*.hs`+ - `tests/{pos,neg}/ExactGADT*.hs` - Add support for Bags/Multisets, see- - `tests/pos/bag.hs`- - `tests/neg/bag.hs`- - `tests/pos/ListISort-bag.hs`+ - `tests/pos/bag.hs`+ - `tests/neg/bag.hs`+ - `tests/pos/ListISort-bag.hs` - Add support for *inductive predicates* see- - `tests/pos/IndEven.hs`- - `tests/pos/IndPerm.hs`- - `tests/pos/IndStar.hs`+ - `tests/pos/IndEven.hs`+ - `tests/pos/IndPerm.hs`+ - `tests/pos/IndStar.hs` ## 0.8.0.1
README.md view
@@ -9,8 +9,8 @@ ## Trying it from Hackage -Assuming the [Z3](https://github.com/Z3Prover/z3) SMT solver is installed and-available in your `PATH`, you can run+Assuming the [Z3](https://github.com/Z3Prover/z3) SMT solver version `4.8.17` or+newer is installed and available in your `PATH`, you can run ``` cabal install --lib liquidhaskell liquid-prelude liquid-vector --package-env . --force-reinstalls@@ -27,7 +27,8 @@ ## Trying it from GitHub -The github repo only builds with GHC 9.12.2, which must be in your `PATH`.+The github repo builds with GHC `9.14.1`, cabal-install `3.16.1.0`, and `z3` `9.8.17` or newer, all of+which must be in your `PATH`. ``` git clone https://github.com/ucsd-progsys/liquidhaskell.git@@ -40,7 +41,7 @@ ## Asking for Help -If you have questions or you just need help, you can always reach out on our [slack channel](https://join.slack.com/t/liquidhaskell/shared_invite/enQtMjY4MTk3NDkwODE3LTFmZGFkNGEzYWRkNDJmZDQ0ZGU1MzBiZWZiZDhhNmY3YTJiMjUzYTRlNjMyZDk1NDU3ZGIxYzhlOTIzN2UxNWE), [google groups mailing list](https://groups.google.com/forum/#!forum/liquidhaskell), [GitHub issue tracker](https://github.com/ucsd-progsys/liquidhaskell/issues), or by emailing [Ranjit Jhala](https://github.com/ranjitjhala), [Niki Vazou](https://github.com/nikivazou).+If you have questions or you just need help, you can always reach out on our [zulip space](https://liquidhaskell.zulipchat.com/), [google groups mailing list](https://groups.google.com/forum/#!forum/liquidhaskell), [GitHub issue tracker](https://github.com/ucsd-progsys/liquidhaskell/issues), or by emailing [Ranjit Jhala](https://github.com/ranjitjhala), [Niki Vazou](https://github.com/nikivazou). # Contributing @@ -128,6 +129,12 @@ Tests run in parallel, unless the flag `--measure-timings` is specified to `test_plugin.sh`. +### How to add a new test++Select a folder where to add the test, for instance `tests/ple/pos` and add a+new file `MyTest.hs` with the test module. Then add the module to the+corresponding executable in `tests/tests.cabal`.+ ## How to create performance comparison charts Firstly, make sure to remove previous compilation artifacts of tests before measuring performance,@@ -147,17 +154,17 @@ converted to json data with ```bash-cabal v2-build ghc-timings-cabal v2-exec ghc-timings dist-newstyle+cabal build ghc-timings+cabal exec ghc-timings dist-newstyle ``` which will produce `tmp/*.json` files. Then a csv report can be generated from the json files with ```-cabal v2-run benchmark-timings -- tmp/*.json --phase LiquidHaskellCPU -o summary.csv+cabal run benchmark-timings -- tmp/*.json --phase LiquidHaskellCPU -o summary.csv ```-On each line, the report will contain the the wall-clock time taken by each test.+On each line, the report will contain the CPU time taken by each test. Use `--phase LiquidHaskell` to get the wall-clock time instead. Although in that case you need to use the `--measure-timings-j1` option when running the tests, which validates modules one at a time.@@ -165,7 +172,7 @@ 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+cabal run plot-performance -- -b path_to_before_summary.csv -a path_to_after_summary.csv -s 50 ``` This will generate two files `top.svg` and `bot.svg` containing the top 50 speedups and slowdowns@@ -393,3 +400,8 @@ Reference: [Implementing a GHC Plugin for Liquid Haskell](https://well-typed.com/blog/2020/08/implementing-a-ghc-plugin-for-liquid-haskell/).++# Sponsors++### [](https://zulip.com)+**[Zulip](https://zulip.com)** — Zulip Cloud Standard generously provided free of charge.
liquidhaskell.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: liquidhaskell-version: 0.9.12.2.1+version: 0.9.14.1 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.12.2+tested-with: GHC == 9.14.1 extra-doc-files: CHANGES.md README.md @@ -79,7 +79,7 @@ hs-source-dirs: src build-depends: base >= 4.11.1.0 && < 5,- liquidhaskell-boot == 0.9.12.2.1,+ liquidhaskell-boot == 0.9.14.1, bytestring, containers, ghc-prim
src/Data/Bits_LHAssumptions.hs view
@@ -3,6 +3,6 @@ {-@ // TODO: cannot use this because `Bits` is not a `Num`-// Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat +// Data.Bits.shiftR :: (Data.Bits.Bits a) => x:a -> d:Nat // -> {v:a | ((d=1) => (x <= 2*v + 1 && 2*v <= x)) } @-}
src/GHC/Num/Integer_LHAssumptions.hs view
@@ -4,13 +4,13 @@ module GHC.Num.Integer_LHAssumptions() where import GHC.Prim-import GHC.Num.Integer+import GHC.Num import GHC.Types_LHAssumptions() {-@-assume GHC.Num.Integer.IS :: x:Int# -> {v: Integer | v = (x :: int) }+assume IS :: x:Int# -> {v: Integer | v = (x :: int) } -define GHC.Num.Integer.IS x = (x)+define IS x = (x) embed Integer as int @-}
src/GHC/Real_LHAssumptions.hs view
@@ -51,11 +51,11 @@ define div x y = (x / y) define mod x y = (x mod y) define quot x y = if x >= 0- then (if y >= 0 then x / y else -(x / -y))- else -(-x / y)+ then (if y >= 0 then x / y else -(x / abs y))+ else -(abs x / y) define rem x y = if x >= 0- then (if y >= 0 then x mod y else x mod -y)- else - (-x mod y)+ then (if y >= 0 then x mod y else x mod (abs y))+ else - ((abs x) mod y) define fromIntegral x = (x) @-}
src/GHC/Types_LHAssumptions.hs view
@@ -22,7 +22,6 @@ embed Word64# as int embed Int as int embed Int# as int-embed Bool as bool embed Char as Char embed Char# as Char embed Addr# as Str
src/Prelude_LHAssumptions.hs view
@@ -9,7 +9,6 @@ import GHC.Maybe_LHAssumptions() import GHC.Num_LHAssumptions() import GHC.Num.Integer_LHAssumptions()-import GHC.Num.Integer() import GHC.Real_LHAssumptions() import Liquid.Prelude.Real_LHAssumptions() import Liquid.Prelude.Totality_LHAssumptions()