Merge pull request #2231 from ucsd-progsys/fd/update-lf

Update liquid-fixpoint
ucsd-progsys · Oct 18, 2023 · 770c26b · 770c26b
2 parents c55c331 + fd5b5be
commit 770c26b
Show file tree

Hide file tree

Showing 8 changed files with 32 additions and 24 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -2,6 +2,16 @@
 
 ## NEXT 0.9.XX
 
+## 0.9.2.5
+
+- Introduce package liquidhaskell-boot and eliminate wrapper packages for boot libraries
+- List all definitions used from the GHC API
+- Allow LH to verify modules in parallel (remove withArgs call)
+- Remove some calls to HashMap.toList which caused some non-determinisms in different machines
+- Implement a Haskell script to plot performance without gnuplot
+
+## 0.9.0.2
+
 - **breaking change** Remove the implicit types mechanism and corresponding tests
 - **breaking change** Remove the `decrease` keyword and mechanism in favor of the terminating expressions syntax (`/ [a,b]`)
 

diff --git a/docs/mkDocs/docs/install.md b/docs/mkDocs/docs/install.md
@@ -19,20 +19,15 @@ 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.5`: 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
 
 Newer versions of GHC aren't supported yet.
 
-When using liquidhaskell from github, add `liquidhaskell` to the `build-depends`
-section of your `.cabal` file, and configure `stack` or `cabal`-install to
-look for the package there. The following section points to an example project
-that does this.
-
-When using liquidhaskell from Hackage, add `liquidhaskell` and
-`liquid-base` to the `build-depends` section of your `.cabal` file, as you would
-any other dependency.
+To use liquidhaskell from Hackage, add `liquidhaskell` to the `build-depends`
+section of your `.cabal` file, as you would any other dependency. `liquid-base`
+needs to be added only if using a GHC version older than 9.2.5.
 
 This causes `stack` (or `cabal`) to automatically:
 

diff --git a/liquid-fixpoint b/liquid-fixpoint
diff --git a/liquid-parallel/liquid-parallel.cabal b/liquid-parallel/liquid-parallel.cabal
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-parallel
-version:            3.2.2.0.1
+version:            3.2.2.0.2
 synopsis:           LiquidHaskell specs for the parallel package
 description:        LiquidHaskell specs for the parallel package.
 license:            BSD3
@@ -20,7 +20,7 @@ library
   hs-source-dirs:     src
   build-depends:      base          < 5
                     , parallel             >= 3.2.2.0 && < 3.3
-                    , liquidhaskell        >= 0.9.0.2
+                    , liquidhaskell        >= 0.9.2.5
   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
@@ -1,6 +1,6 @@
 cabal-version:      1.22
 name:               liquid-platform
-version:            0.9.0.2
+version:            0.9.2.5
 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.0.2
-                      , liquid-vector     >= 0.12.3.1 && < 0.13
-                      , liquidhaskell     >= 0.9.0.2
-                      , liquidhaskell-boot >= 0.9.0.2
+                      , liquid-prelude    >= 0.9.2.5
+                      , liquid-vector     >= 0.12.3.1.2
+                      , liquidhaskell     >= 0.9.2.5
+                      , liquidhaskell-boot >= 0.9.2.5
                       , 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
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-prelude
-version:            0.9.0.2
+version:            0.9.2.5
 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.0.2
+                    , liquidhaskell        >= 0.9.2.5
   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
@@ -1,6 +1,6 @@
 cabal-version:      1.24
 name:               liquid-vector
-version:            0.12.3.1
+version:            0.12.3.1.2
 synopsis:           LiquidHaskell specs for the vector package
 description:        LiquidHaskell specs for the vector package.
 license:            BSD3
@@ -19,8 +19,8 @@ library
   exposed-modules:    Data.Vector_LHAssumptions
   hs-source-dirs:     src
   build-depends:      base          < 5
-                    , vector               >= 0.12.3.1 && < 0.13
-                    , liquidhaskell        >= 0.9.0.2
+                    , vector               >= 0.12.3.1 && < 0.14
+                    , liquidhaskell        >= 0.9.2.5
   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
@@ -2,7 +2,10 @@ cabal-version:      2.4
 name:               liquidhaskell-boot
 version:            0.9.2.5.0
 synopsis:           Liquid Types for Haskell
-description:        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)
+                    instead, which rexports this plugin together with necessary
+                    specifications for definitions in the boot libraries.
 license:            BSD-3-Clause
 copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
 author:             Ranjit Jhala, Niki Vazou, Eric Seidel
@@ -140,7 +143,7 @@ library
                     , gitrev
                     , hashable             >= 1.3 && < 1.5
                     , hscolour             >= 1.22
-                    , liquid-fixpoint      == 0.9.0.2.1
+                    , liquid-fixpoint      == 0.9.2.5
                     , mtl                  >= 2.1
                     , optparse-applicative < 0.18
                     , githash
+2 −2		liquid-fixpoint.cabal
+1 −1		src/Language/Fixpoint/Horn/Types.hs
+6 −4		src/Language/Fixpoint/Misc.hs
+2 −2		src/Language/Fixpoint/Solver/Instantiate.hs
+1 −1		src/Language/Fixpoint/Solver/Sanitize.hs
+6 −7		src/Language/Fixpoint/Types/Config.hs
+3 −3		stack.yaml
+11 −11		stack.yaml.lock
+25 −0		tests/horn/pos/maps00.smt2
+12 −0		tests/horn/pos/str00.smt2