Installing copilot-verifier

[ivanperez-keera]

I'm having lots of issues installing copilot-verifier.

Most of the issues have to do with crucible or related libraries. I suspect its related to the versions of GHC that it supports.

What versions of GHC are supported by copilot-verifier (without using the constraints on base in copilot-verifier.cabal as guide, but actually trying it)?

[RyanGlScott]

Can you describe what steps you are trying to build copilot-verifier? I was able to build it with GHC 9.4 through 9.8 by doing the following:

1. Apply this change to copilot's cabal.project file:

   diff --git a/cabal.project b/cabal.project
   index 812c95ba..9c0fae7f 100644
   --- a/cabal.project
   +++ b/cabal.project
   @@ -7,4 +7,5 @@ packages:
      copilot-libraries/copilot-libraries.cabal
      copilot-prettyprinter/copilot-prettyprinter.cabal
      copilot-theorem/copilot-theorem.cabal
   +  copilot-verifier/copilot-verifier.cabal
      copilot/copilot.cabal

2. Running cabal build copilot-verifier.

[ivanperez-keera]

Can we build it with any version prior to 9.4? (I frequently work with the 8.* series still.)

Can we build it with 9.10 or 9.12?

[ivanperez-keera]

I'm doing a cabal v1-sandbox init followed by a cabal v1-install copilot**/.

[RyanGlScott]

I frequently work with the 8.* series still.

OK. What is the oldest GHC version that you need to support? If you are experiencing issues building things, then I suspect the sticking point is the GHC version rather than the use of v1-style cabal sandboxes.

Can we build it with any version prior to 9.4?

I haven't tried, but I suspect that the answer is no, given crucible's adherence to a policy of generally only supporting three recent GHC releases at a time. See also GaloisInc/crucible#1525.

Can we build it with 9.10 or 9.12?

We recently added support for GHC 9.10 in crucible (see GaloisInc/crucible#1377), but we need to make a new Hackage release with these changes. GHC 9.12 support is still in progress (see GaloisInc/crucible#1308).