Merge pull request #273 from GaloisInc/T272-ghc-9.10

Support building with GHC 9.10

.github/workflows/gen_matrix.pl

@@ -94,6 +94,7 @@ main_version(abc, "2021_12_30").
 
 version(ubuntu, "ubuntu-latest").
 
+version(ghc, "9.10.1").
 version(ghc, "9.8.1").
 version(ghc, "9.6.2").
 version(ghc, "9.4.4").

.github/workflows/test.yml

@@ -24,7 +24,7 @@ on:
 # (e.g. cabal complains it can't find a valid version of the "happy"
 # tool).
 env:
-  CACHE_VERSION: 3
+  CACHE_VERSION: 4
 
 jobs:
   genmatrix:
@@ -105,9 +105,16 @@ jobs:
             9.4.4) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;;
             9.6.2) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.05 ;;
             9.8.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-23.11 ;;
+            9.10.1) GHC_NIXPKGS=github:nixos/nixpkgs/nixos-24.05 ;;
             *)     GHC_NIXPKGS=github:nixos/nixpkgs/21.11 ;;
           esac
-          echo NS="nix shell ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} nixpkgs#gmp nixpkgs#zlib nixpkgs#zlib.dev" >> $GITHUB_ENV
+          echo "GHC_NIXPKGS=${GHC_NIXPKGS}" >> $GITHUB_ENV
+          echo NS="nix shell ${GHC_NIXPKGS}#pkg-config ${GHC_NIXPKGS}#cabal-install ${GHC_NIXPKGS}#${GHC} ${GHC_NIXPKGS}#gmp ${GHC_NIXPKGS}#zlib ${GHC_NIXPKGS}#zlib.dev" >> $GITHUB_ENV
+          # In a normal nix derivation, there is a pkgconfig hook that automatically
+          # handles this, but since we are just using a nix shell this must be setup
+          # manually so that if the haskell zlib package is built, it finds the right
+          # zlib packge config.
+          echo PKG_CONFIG_PATH=$(nix eval --raw ${GHC_NIXPKGS}#zlib.dev)/lib/pkgconfig >> $GITHUB_ENV
 
       - name: Cabal update
         shell: bash
@@ -146,12 +153,13 @@ jobs:
         # following adds a zlib package-specific stanza for these.
         run: |
           cd what4
-          $NS -c cabal configure --enable-tests -fdRealTestDisable -fsolverTests --extra-lib-dirs=$(nix eval --raw nixpkgs#zlib)/lib --extra-include-dirs=$(nix eval --raw nixpkgs#zlib.dev)/include
+          $NS -c cabal configure --enable-tests -fdRealTestDisable -fsolverTests --extra-lib-dirs=$(nix eval --raw ${GHC_NIXPKGS}#zlib)/lib --extra-include-dirs=$(nix eval --raw ${GHC_NIXPKGS}#zlib.dev)/include
           echo "" >> ../cabal.project.local
           echo package zlib >> ../cabal.project.local
-          echo "  extra-lib-dirs: $(nix eval --raw nixpkgs#zlib)/lib" >> ../cabal.project.local
-          echo "  extra-include-dirs: $(nix eval --raw nixpkgs#zlib.dev)/include" >> ../cabal.project.local
+          echo "  extra-lib-dirs: $(nix eval --raw ${GHC_NIXPKGS}#zlib)/lib" >> ../cabal.project.local
+          echo "  extra-include-dirs: $(nix eval --raw ${GHC_NIXPKGS}#zlib.dev)/include" >> ../cabal.project.local
           cp ../cabal.project.local ./
+          cat ../cabal.project.local
 
       - name: Build
         shell: bash

dependencies/aig

@@ -1 +1 @@
-Subproject commit 372d533621b24ffdc7e911b92f66ddb0fdc361a9
+Subproject commit f8d96d733865791f2a950a46477c359f33c29c01

what4-abc/what4-abc.cabal

@@ -17,7 +17,7 @@ Description:
 
 library
   build-depends:
-    base >= 4.7 && < 4.20,
+    base >= 4.7 && < 4.21,
     aig,
     abcBridge >= 0.11,
     bv-sized >= 1.0.0,

what4-blt/what4-blt.cabal

@@ -26,7 +26,7 @@ common bldflags
 library
   import: bldflags
   build-depends:
-    base >= 4.7 && < 4.20,
+    base >= 4.7 && < 4.21,
     blt >= 0.12.1,
     containers,
     what4 >= 0.4,

what4-transition-system/what4-transition-system.cabal

@@ -13,7 +13,7 @@ build-type:    Simple
 common dependencies
   build-depends:
     , ansi-wl-pprint       ^>=0.6
-    , base                 >=4.12 && <4.20
+    , base                 >=4.12 && <4.21
     , bytestring
     , containers           ^>=0.6
     , io-streams

what4/src/What4/Expr/BoolMap.hs

@@ -34,7 +34,7 @@ module What4.Expr.BoolMap
 
 import           Control.Lens (_1, over)
 import           Data.Hashable
-import           Data.List (foldl')
+import qualified Data.List as List (foldl')
 import           Data.List.NonEmpty (NonEmpty(..))
 import           Data.Kind (Type)
 import           Data.Parameterized.Classes
@@ -150,7 +150,7 @@ addVar x p1 (BoolMap bm) = maybe InconsistentMap BoolMap $ AM.alterF f (Wrap x)
 -- | Generate a bool map from a list of terms and polarities by repeatedly
 --   calling @addVar@.
 fromVars :: (HashableF f, OrdF f) => [(f BaseBoolType, Polarity)] -> BoolMap f
-fromVars = foldl' (\m (x,p) -> addVar x p m) (BoolMap AM.empty)
+fromVars = List.foldl' (\m (x,p) -> addVar x p m) (BoolMap AM.empty)
 
 -- | Merge two bool maps, performing resolution as necessary.
 combine :: OrdF f => BoolMap f -> BoolMap f -> BoolMap f

what4/src/What4/Expr/WeightedSum.hs

@@ -74,7 +74,7 @@ import           Control.Monad (unless)
 import qualified Data.BitVector.Sized as BV
 import           Data.Hashable
 import           Data.Kind
-import           Data.List (foldl')
+import qualified Data.List as List (foldl')
 import           Data.Maybe
 import           Data.Parameterized.Classes
 
@@ -432,7 +432,7 @@ traverseProdVars f pd =
     traverse (_1 (traverseWrap f)) (AM.toList (_prodMap pd))
  where
   sr = prodRepr pd
-  rebuild = foldl' (\m (WrapF t, occ) -> AM.insert (WrapF t) (mkProdNote sr occ t) occ m) AM.empty
+  rebuild = List.foldl' (\m (WrapF t, occ) -> AM.insert (WrapF t) (mkProdNote sr occ t) occ m) AM.empty
 
 
 -- | This returns a variable times a constant.

what4/src/What4/Solver/CVC5.hs

@@ -35,7 +35,6 @@ module What4.Solver.CVC5
 
 import           Control.Monad (forM_, when)
 import           Data.Bits
-import           Data.String
 import           System.IO
 import qualified System.IO.Streams as Streams
 

what4/src/What4/Utils/AnnotatedMap.hs

@@ -44,7 +44,6 @@ module What4.Utils.AnnotatedMap
 
 import           Data.Functor.Identity
 import qualified Data.Foldable as Foldable
-import           Data.Foldable (foldl')
 import           Prelude hiding (null, filter, lookup)
 
 import qualified Data.FingerTree as FT
@@ -57,19 +56,19 @@ filterFingerTree ::
   FT.Measured v a =>
   (a -> Bool) -> FT.FingerTree v a -> FT.FingerTree v a
 filterFingerTree p =
-  foldl' (\xs x -> if p x then xs FT.|> x else xs) FT.empty
+  Foldable.foldl' (\xs x -> if p x then xs FT.|> x else xs) FT.empty
 
 mapMaybeFingerTree ::
   (FT.Measured v2 a2) =>
   (a1 -> Maybe a2) -> FT.FingerTree v1 a1 -> FT.FingerTree v2 a2
 mapMaybeFingerTree f =
-  foldl' (\xs x -> maybe xs (xs FT.|>) (f x)) FT.empty
+  Foldable.foldl' (\xs x -> maybe xs (xs FT.|>) (f x)) FT.empty
 
 traverseMaybeFingerTree ::
   (Applicative f, FT.Measured v2 a2) =>
   (a1 -> f (Maybe a2)) -> FT.FingerTree v1 a1 -> f (FT.FingerTree v2 a2)
 traverseMaybeFingerTree f =
-   foldl' (\m x -> rebuild <$> m <*> f x) (pure FT.empty)
+   Foldable.foldl' (\m x -> rebuild <$> m <*> f x) (pure FT.empty)
  where
  rebuild ys Nothing  = ys
  rebuild ys (Just y) = ys FT.|> y

what4/src/What4/Utils/Environment.hs

@@ -24,7 +24,7 @@ import Control.Monad.Fail( MonadFail )
 
 import Control.Monad.IO.Class
 import Data.Char
-import Data.List (foldl')
+import qualified Data.List as List (foldl')
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified System.Directory as Sys
@@ -81,7 +81,7 @@ expandEnvironmentPath base_map path = do
   let init_map = Map.fromList [ ("MSS_BINPATH", prog_path) ]
   -- Extend init_map with environment variables.
   env <- getEnvironment
-  let expanded_map = foldl' (\m (k,v) -> Map.insert k v m) init_map env
+  let expanded_map = List.foldl' (\m (k,v) -> Map.insert k v m) init_map env
   -- Return expanded path.
   expandVars (Map.union base_map expanded_map) path
 

what4/src/What4/Utils/Word16String.hs

@@ -20,7 +20,9 @@ module What4.Utils.Word16String
 , take
 , append
 , length
-, foldl'
+-- Qualify this name to disambiguate it from the Prelude version of foldl'
+-- (defined in base-4.20 or later).
+, What4.Utils.Word16String.foldl'
 , findSubstring
 , isInfixOf
 , isPrefixOf
@@ -91,7 +93,7 @@ showsWord16String (Word16String xs0) tl = '"' : go (BS.unpack xs0)
 --   where the 16bit words are encoded as two bytes
 --   in little-endian order.
 --
---   PRECONDITION: the input bytestring must 
+--   PRECONDITION: the input bytestring must
 --   have a length which is a multiple of 2.
 fromLEByteString :: ByteString -> Word16String
 fromLEByteString xs

what4/test/InvariantSynthesis.hs

@@ -13,7 +13,6 @@ import           Test.Tasty.HUnit
 import           Data.Maybe
 import           System.Environment
 
-import qualified Data.BitVector.Sized as BV
 import           Data.Parameterized.Context
 import           Data.Parameterized.Map (MapF)
 import           Data.Parameterized.Nonce

what4/what4.cabal

@@ -9,7 +9,7 @@ License-file:  LICENSE
 Build-type:    Simple
 Homepage:      https://github.com/GaloisInc/what4
 Bug-reports:   https://github.com/GaloisInc/what4/issues
-Tested-with:   GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.4, GHC==9.6.2, GHC==9.8.1
+Tested-with:   GHC==8.8.4, GHC==8.10.7, GHC==9.0.2, GHC==9.2.2, GHC==9.4.4, GHC==9.6.2, GHC==9.8.1, GHC==9.10.1
 Category:      Formal Methods, Theorem Provers, Symbolic Computation, SMT
 Synopsis:      Solver-agnostic symbolic values support for issuing queries
 Description: