`copilot-theorem`: Extend range of versions of `what4`

[ivanperez-keera]

Description

In order to keep Copilot effectively working in the current Haskell ecosystem, as well as new versions of GHC, we need to extend the versions of dependencies that Copilot can be installed with. The package what4 has seen release 1.7, but we depend on versions prior to 1.7.

Type

• Management: update versions of dependencies.

Additional context

None.

Requester

• Ivan Perez.

Method to check presence of bug

Not applicable (not a bug).

Expected result

Copilot can be installed with the most recent version of what4 published on hackage that do not require a change to the Haskell code.

Desired result

Copilot can be installed with the most recent version of what4 published on hackage that do not require a change to the Haskell code.

Proposed solution

Bump version bounds on what4.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Copilot 4.5.

Fix assigned to: @ivanperez-keera .

[ivanperez-keera]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • [X] The code proposed compiles and passes all tests. Details: Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/275675175
  • [X] The solution proposed produces the expected result. Details: The following Dockerfile installs copilot forcing the version of what4 to be greater than or equal to 1.7, after which it prints the message "Success":

    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 \
          z3
    
    RUN mkdir -p $HOME/.ghcup/bin
    RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -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.10.1
    RUN ghcup install cabal 3.2
    RUN ghcup set ghc 9.10.1
    RUN cabal update
    
    SHELL ["/bin/bash", "-c"]
    CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \
      && cabal v1-sandbox init \
      && cabal v1-install alex happy --constraint='happy <= 2' \
      && cabal v1-install --constraint='what4 >= 1.7' \
                          $NAME/copilot/ \
                          $NAME/copilot-c99/ \
                          $NAME/copilot-core/ \
                          $NAME/copilot-prettyprinter/ \
                          $NAME/copilot-interpreter/ \
                          $NAME/copilot-language/ \
                          $NAME/copilot-libraries/ \
                          $NAME/copilot-theorem/ \
      && echo "Success"
    

    Command (substitute variables based on new path after merge):

    $ docker run -e REPO=https://github.com/ivanperez-keera/copilot -e NAME=copilot -e COMMIT=1f68f7e9d5f09a2a0e6cdd902cfd20d637c30fef copilot-verify-611
    

• [X] Implementation is documented. Details: No updates needed.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed.
• [X] Author is internal or has provided signed CLA.
• [X] Required version bumps are evaluated. Details: Bump not needed (relaxes version constraints).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.