mirror of
https://github.com/GaloisInc/what4.git
synced 2024-11-29 05:45:01 +03:00
a1adde9685
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).
60 lines
1.3 KiB
Plaintext
60 lines
1.3 KiB
Plaintext
Cabal-version: 2.2
|
|
Name: what4-blt
|
|
Version: 0.2
|
|
Author: Galois Inc.
|
|
Maintainer: rdockins@galois.com
|
|
Copyright: (c) Galois, Inc 2014-2021
|
|
License: BSD-3-Clause
|
|
License-file: LICENSE
|
|
Build-type: Simple
|
|
Category: Language
|
|
Synopsis: What4 bindings to BLT
|
|
Description:
|
|
BLT is a library the solves bounded integer linear programs by
|
|
reducing the problem to bounded lattice search. This package
|
|
provides support for lowering Crucible formulae to linear systems
|
|
of the sort understood by BLT, and for executing the underlying solver.
|
|
|
|
common bldflags
|
|
ghc-options: -Wall
|
|
-Werror=incomplete-patterns
|
|
-Werror=missing-methods
|
|
-Werror=overlapping-patterns
|
|
ghc-prof-options: -fprof-auto-export
|
|
default-language: Haskell2010
|
|
|
|
library
|
|
import: bldflags
|
|
build-depends:
|
|
base >= 4.7 && < 4.16,
|
|
blt >= 0.12.1,
|
|
containers,
|
|
what4 >= 0.4,
|
|
lens >= 1.2,
|
|
parameterized-utils,
|
|
prettyprinter >= 1.7.0,
|
|
text,
|
|
transformers
|
|
|
|
hs-source-dirs: src
|
|
|
|
exposed-modules:
|
|
What4.Solver.BLT
|
|
|
|
test-suite test
|
|
import: bldflags
|
|
type: exitcode-stdio-1.0
|
|
hs-source-dirs: test
|
|
|
|
main-is: Test.hs
|
|
|
|
build-depends:
|
|
base,
|
|
containers,
|
|
what4-blt,
|
|
QuickCheck,
|
|
tasty >= 0.10,
|
|
tasty-hunit >= 0.9,
|
|
tasty-quickcheck >= 0.8,
|
|
blt
|