Bump the upper version bounds on `base` in the various `what4` packages, and
bump the `aig` submodule to bring in the changes from
https://github.com/GaloisInc/aig/pull/18.
This patch contains a variety of fixes needed to build the libraries in the
what4 repo with GHC 9.8:
* Bump the upper version bounds on `base` and `text` to allow building with the
versions that are bundled with GHC 9.8 (`base-4.19.*` and `text-2.1.*`,
respectively).
* Replace uses of `head` and `tail` (which trigger `-Wx-partial` warnings with
GHC 9.8) with total functions or `panic`s, depending on what is appropriate.
* Bump the `aig` submodule to bring in the changes from GaloisInc/aig#16 and
GaloisInc/aig#17.
This patch contains a variety of fixes needed to build the libraries in the
`what4` repo with GHC 9.6:
* GHC 9.6 bundles `mtl-2.3.*`, which no longer re-exports `Control.Monad`,
`Control.Monad.IO.Class`, and similar modules from `mtl`-related modules.
To accommodate this, various imports have been made more explicit.
* `MonadTrans t` now has a quantified `forall m. Monad m => Monad (t m)`
superclass in `mtl-2.3.*`. As a result, the `MonadTrans (PartialT sym)`
instance must now have an `IsExpr (SymExpr sym)` instance context in order
for it to typecheck, as this is the same instance context that `PartialT`'s
`Monad` instance has.
This is technically a breaking change, so I have noted it in the `what4`
changelog. That being said, this change is unlikely to affect many people
in practice, considering that the `MonadTrans` instance for `PartialT` is
usually used in tandem with the `Monad` instance.
* Various upper version bounds on `base` have been lifted to allow building
with `base-4.18`.
* The `aig` submodule has been bumped to bring in the changes from
GaloisInc/aig#15, which allows it to build with GHC 9.6.
This contains a variety of changes needed to make the libraries in the `what4`
compile warning-free with GHC 9.2:
* GHC 9.2 includes `-Woperator-whitespace-ext-conflict` as a part of `-Wall`,
which causes `Test.Verification` to warn when built with GHC 9.2. The fix is
simple: just add spaces after certain uses of the `$` character.
* GHC 9.2 includes `-Wincomplete-uni-patterns` as a part of `-Wall`, which
causes `GenWhat4Expr` to warn when built with GHC 9.2. I fixed the warnings
by introducing new `from{Bool,Int,BV8,BV16,BV32,BV64}TestExpr` functions to
extract the payloads of different `TestExpr` constructors. This is no less
partial than before, but at least this way any accidental partiality will
result in a more descriptive error message than
`Non-exhaustive patterns in ...`.
* In `base-4.16.*`, `Nat` is now a type synonym for `Natural`, and
`GHC.TypeNats` now re-exports `Natural`. This causes an import of
`Numeric.Natural` in `What4.SemiRing` (previously required to bring `Natural`
into scope) trigger an `-Wunused-imports` warning. I fixed the warning by
using explicit imports from `GHC.TypeNats` and `Numeric.Natural`.
* The `aig` and `abcBridge` submodules were bumped to bring in the changes
from GaloisInc/aig#12 and GaloisInc/abcBridge#19, respectively, which allows
them to build with `base-4.16.*`.
* The upper version bounds on `base` were raised in `what4-abc`, `what4-blt`,
and `what4-transition-system` to allow them to build with `base-4.16.*`.
This contains a variety of tweaks needed to make `what4`, `what4-abc`, and
`what4-blt` build warning-free on GHC 9.0:
* GHC's constraint solver now solves constraints in each top-level group
sooner (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#the-order-of-th-splices-is-more-important)).
This affects `what4`'s `What4.Expr.App` module, as it separates top-level
groups with a Template Haskell `$(return [])` splice. The previous location
of this splice made it so that the TH-generated instances in that module
(e.g., the `TraversableFC` instance for `App`) were not available to any code
before the splice, resulting in type errors when compiled with GHC 9.0.
I implemented a fairly involved fix of moving each of the affected data
types, as well as their corresponding TH-generated instances, to the top of
the module to ensure that subsequent top-level groups have access to this
code.
* GHC 9.0 implements simplified subsumption (see
[here](https://gitlab.haskell.org/ghc/ghc/-/wikis/migration/9.0?version_id=5fcd0a50e0872efb3c38a32db140506da8310d87#simplified-subsumption)).
This affects the use of the `freshBoundTermFn` function in `what4`'s
`What4.Protocol.SMTWriter` module, as `freshBoundTermFn`'s type signature
contains a nested `forall`. Fortunately, repairing this code is as simple as
a single eta expansion.
* Raise the upper version bounds on `base` in `what4-abc` and `what4-blt` to
permit building with `base-4.15` (bundled with GHC 9.0).
* Bump the `aig` submodule commit so that it does not emit `-Wstar-is-type`
warnings when built with GHC 9.0, where `-Wall` implies `-Wstar-is-type`.
Bump the `language-sally` submodule commit to allow building with
`base-4.15` (see GaloisInc/language-sally#6).
* Update/imporove Haddock comments and bump copyright years
* Bump copyright dates in LICENSE files
* Add .cabal package lower bounds. These appear to be reasonable, but
I haven't exhaustively tested the various configurations.
* Bump copyright dates in .cabal files
* Start a basic changelog
