Support building with GHC 9.8 #2098
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
As of `aeson-2.2.*`, the `json'` function has been removed and migrated to a new package, `attoparsec-aeson`. Adapt to this change accordingly in `verif-viewer`, which uses `json'`.
In `sbv-10.3`, `UINone` gained an additional `Bool` field to represent if the `UICodeKind` is curried or not. (See LeventErkok/sbv@46fb932) This usually defaults to `True`, so we follow suit in `saw-core-sbv`.
`sbv-10.3` adds support for the OpenSMT solver (https://verify.inf.usi.ch/opensmt). Annoyingly, it's not possible to query the OpenSMT version number from the command line, which is the one operation that SAW's SMT caching requires. As such, we do the bare minimum to fix warnings related to missing pattern match cases on `OpenSMT`, but without going as far as adding full support for OpenSMT.
GHC 9.8 is better about reporting orphan type family instances, which are used in various spots in Macaw. Enable `-Wno-orphans` to suppress these warnings.
`base-4.19.0.0` (GHC 9.8) adds `unzip` to `Data.Functor`, which clashes with the `unzip` function defined in `Data.List`. We resolve the ambiguity by using explicit imports from `Data.Functor` to avoid importing `Data.Functor.unzip`.
Really, we should be throwing a proper error message here instead of throwing a `panic`, and we should document the requirement that the list of mutually recursive functions must be non-empty. That is left as future work (see #2096).
Really, we should be throwing a proper error message here instead of throwing a `panic`, and we should document the requirement that `__breakpoint__` functions must end with `#<parent_name>`. That is left as future work (see #2097).
`pkg-config` is needed for the Haskell `zlib` library to locate the system's `zlib` installation.
These are needed to install shared libraries for `zlib`, which SAW depends on an runtime.
kquick
approved these changes
Aug 22, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR contains a variety of tweaks needed to make the libraries in the
saw-scriptrepo support building with GHC 9.8. This includes:-Wx-partialand-Worphanswarnings that were uncovered by the version of-Wallimplemented in GHC 9.8. Note that some particular occurrences of-Wx-partialwarnings have their own SAW issues associated with them (Heapster:Prelude.head: empty listcrash when invokingheapster_typecheck_mut_funson empty list #2096 andllvm_verifycrashes (Prelude.tail: empty list) when verifying a function whose name contains "__breakpoint__" without a#afterwards #2097), as it is possible to observe the partiality in SAW scripts.cabalbuild plan that is compatible with GHC 9.8. Note that in order to supportaeson-2.2.*(required for GHC 9.8 support), I had to tweakverif-viewerto adapt toaeson-2.2.*removing thejson'function and moving it to the newattoparsec-aesonpackage instead.sbv-10.3.