crucible-0.7.1 Hackage release does not compile

[RyanGlScott]

As observed here:

[32 of 58] Compiling Lang.Crucible.Concretize ( src/Lang/Crucible/Concretize.hs, dist/build/Lang/Crucible/Concretize.o, dist/build/Lang/Crucible/Concretize.dyn_o )

src/Lang/Crucible/Concretize.hs:561:17: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
561 |     BoolRepr -> W4GE.groundToSym sym BaseBoolRepr v
    |                 ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:562:21: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
562 |     BVRepr width -> W4GE.groundToSym sym (BaseBVRepr width) v
    |                     ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:563:24: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
563 |     ComplexRealRepr -> W4GE.groundToSym sym BaseComplexRepr v
    |                        ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:569:17: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
569 |           sv <- W4GE.groundToSym sym (floatInfoToBVTypeRepr fi) v
    |                 ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:573:26: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
573 |     IEEEFloatRepr fpp -> W4GE.groundToSym sym (BaseFloatRepr fpp) v
    |                          ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:574:20: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
574 |     IntegerRepr -> W4GE.groundToSym sym BaseIntegerRepr v
    |                    ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:575:41: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
575 |     NatRepr -> W4I.integerToNat sym =<< W4GE.groundToSym sym BaseIntegerRepr v
    |                                         ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:576:20: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
576 |     RealValRepr -> W4GE.groundToSym sym BaseRealRepr v
    |                    ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:577:22: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
577 |     StringRepr si -> W4GE.groundToSym sym (BaseStringRepr si) v
    |                      ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:578:35: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
578 |     SymbolicArrayRepr idxs tp' -> W4GE.groundToSym sym (BaseArrayRepr idxs tp') v
    |                                   ^^^^^^^^^^^^^^^^

src/Lang/Crucible/Concretize.hs:579:31: error: [GHC-76037]
    Not in scope: W4GE.groundToSym
    NB: the module What4.Expr.GroundEval does not export groundToSym.
    |
579 |     SymbolicStructRepr tys -> W4GE.groundToSym sym (BaseStructRepr tys) v
    |                               ^^^^^^^^^^^^^^^^

This happens because there have been some changes to crucible's what4 submodule since the latest Hackage release of what4 (e.g., GaloisInc/what4#268) that end up being important in order to build crucible. To fix this, we should first make a new Hackage release of what4 that includes these changes, and then we should adjust crucible's lower bounds on what4 accordingly.

[RyanGlScott]

Relatedly, the .cabal file for crucible-llvm ought to reflect that it requires llvm-pretty-0.12.1 or later in order to build. Thankfully, that version of llvm-pretty is on Hackage, so the situation there isn't quite as dire. Still, you'd encounter a build failure if cabal picked a build plan with an older llvm-pretty Hackage release, so we should bump the lower version bounds to be on the safe side.

[langston-barrett]

Perhaps relatedly, it looks like the Haddocks aren't available online: https://hackage.haskell.org/package/crucible-0.7.1

[RyanGlScott]

I've restarted the documentation builds on Hackage, so the latest Hackage releases of crucible, crucible-llvm, crucible-symio, crux, and crux-llvm now have their Haddocks available.