diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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 + +### [![Zulip logo](https://static.zulipchat.com/static/images/logo/zulip-icon-128x128.png)](https://zulip.com) +**[Zulip](https://zulip.com)** — Zulip Cloud Standard generously provided free of charge. 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.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 diff --git a/src/Data/Bits_LHAssumptions.hs b/src/Data/Bits_LHAssumptions.hs --- a/src/Data/Bits_LHAssumptions.hs +++ b/src/Data/Bits_LHAssumptions.hs @@ -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)) } @-} 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 @@ -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 @-} diff --git a/src/GHC/Real_LHAssumptions.hs b/src/GHC/Real_LHAssumptions.hs --- a/src/GHC/Real_LHAssumptions.hs +++ b/src/GHC/Real_LHAssumptions.hs @@ -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) @-} 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 @@ -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 diff --git a/src/Prelude_LHAssumptions.hs b/src/Prelude_LHAssumptions.hs --- a/src/Prelude_LHAssumptions.hs +++ b/src/Prelude_LHAssumptions.hs @@ -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()