mirror of
https://github.com/GaloisInc/what4.git
synced 2024-10-06 00:22:49 +03:00
aa61bf7579
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.*`.
|
||
|---|---|---|
| .. | ||
| src/What4/Solver | ||
| test | ||
| LICENSE | ||
| Setup.hs | ||
| what4-blt.cabal | ||