Constrains on Crucible to be able to install Copilot

[ivanperez-keera]

I had lots of problems during the release with crucible-related libraries.

Specifically, I had to add constraints to use older versions of crucible-syntax and crucible-debug. Without these, the packages would error due to missing symbols.

FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive
RUN apt-get update

RUN apt-get install --yes \
      libz-dev \
      git \
      curl \
      gcc \
      g++ \
      make \
      libgmp3-dev  \
      pkg-config

RUN mkdir -p $HOME/.ghcup/bin
RUN curl https://downloads.haskell.org/~ghcup/0.1.50.2/x86_64-linux-ghcup-0.1.50.2 -o $HOME/.ghcup/bin/ghcup
RUN chmod a+x $HOME/.ghcup/bin/ghcup
ENV PATH=$PATH:/root/.ghcup/bin/
ENV PATH=$PATH:/root/.cabal/bin/

SHELL ["/bin/bash", "-c"]

RUN ghcup install ghc 9.6
RUN ghcup install cabal 3.14
RUN ghcup set ghc 9.6.7
RUN cabal update

SHELL ["/bin/bash", "-c"]
CMD git clone $REPO \
    && cd $NAME \
    && git checkout $COMMIT \
    && echo "  copilot-verifier/copilot-verifier.cabal" >> cabal.project \
    && echo "  copilot-visualizer/copilot-visualizer.cabal" >> cabal.project \
    && cabal install \
         --package-env . \
         --lib \
         --constraint="aeson<2.2" \
         --constraint="crucible-syntax<0.5.0.0" \
         --constraint="crucible-debug<0.1.2.0" \
         --constraint="copilot==4.6.1" \
         --constraint="copilot-bluespec==4.6.1" \
         --constraint="copilot-c99==4.6.1" \
         --constraint="copilot-core==4.6.1" \
         --constraint="copilot-prettyprinter==4.6.1" \
         --constraint="copilot-interpreter==4.6.1" \
         --constraint="copilot-language==4.6.1" \
         --constraint="copilot-libraries==4.6.1" \
         --constraint="copilot-theorem==4.6.1" \
         --constraint="copilot-verifier==4.6.1" \
         --constraint="copilot-visualizer==4.6.1" \
         copilot**/ \
    && echo "Success"

@RyanGlScott @chathhorn-galois @tkann-galois Since crucible is a Galois system, can you please take a look or talk with whoever is maintaining crucible these days?

In case it helps, we want to keep Copilot working with as many versions of GHC as reasonably possible. I specifically use 8.6.5 regularly and would love to be able to continue using that. We are normally on older versions of everything.

[RyanGlScott]

I am a Crucible maintainer, so I can take a look at the build failures you're experiencing. Most likely, we need to revise some of the Hackage versions of crucible* to avoid invalid build plans. (We try to prevent these bad build plans from making onto Hackage, but sometimes things slip through the cracks.)

In case it helps, we want to keep Copilot working with as many versions of GHC as reasonably possible. I specifically use 8.6.5 regularly and would love to be able to continue using that. We are normally on older versions of everything.

See the discussion on GaloisInc/crucible#1525. While making Crucible support all the way back to 8.6.5 would be nice, doing so would require a non-trivial amount of work, and development cycles are limited. If we wanted to make this a high priority, we would need to have a conversation about how what level of support we should aim to provide for old GHC versions.

[RyanGlScott]

I am able to reproduce this, and I've opened GaloisInc/crucible#1702 on the Crucible side. My immediate plan is to revise the current Hackage releases of Crucible and friends to only support building with the specific library versions that they were uploaded alongside. Going forward, I'd also like to be more rigid about using tight version bounds in the Crucible .cabal files to avoid this issue in the future.

[RyanGlScott]

I've revised the version bounds for current Hackage releases of crucible and friends, so I believe it should now be possible to build copilot-verifier without manually constraining version bounds. I'll work on adding tighter version bounds to the upstream crucible code next.