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

[swt2c]

In Debian, we're updating to GHC 9.4 and LTS 21. As part of that, one of what4's dependencies had to be updated, and thus what4 had to be updated to 1.5.1. Can copilot please support what4 >= 1.5.1 so we can update it in Debian?

[ivanperez-keera]

Thank you, @swt2c . I'll look into putting this in the next release, which goes out in a week.

[ivanperez-keera]

Description

what4 has seen a new release 1.5.1, but copilot-theorem needs versions strictly lower than 1.5. This is preventing copilot from being included in the new updates to Debian and, by extension, Ubuntu, which will require what4>=1.5.1

Type

• Management: update versions of dependencies.

Additional context

None.

Requester

• Scott Talbert.

Method to check presence of bug

Not applicable (not a bug).

Expected result

Copilot can be installed with what4-1.5.1.

Desired result

Copilot can be installed with what4-1.5.1.

Proposed solution

Modify copilot-theorem's cabal file to accept what4 versions >= 1.5 and <1.6.

Adjust copilot-theorem as needed to work with that version of what4.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that versions are overly constrained and upper bounds should be relaxed.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Bug scheduled for fixing in Copilot 3.17.

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/267041967

  • [X] The solution proposed produces the expected result. Details: The following Dockerfile checks Copilot can be installed with what4-1.5.1, in which case it prints the message Success:

    
    FROM ubuntu:focal

  RUN apt-get update

  RUN apt-get install --yes libz-dev RUN apt-get install --yes git

  RUN apt-get install --yes wget RUN mkdir -p $HOME/.ghcup/bin RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.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/ RUN apt-get install --yes curl RUN apt-get install --yes gcc g++ make libgmp3-dev

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

  RUN ghcup install ghc 9.4 RUN ghcup install cabal 3.8 RUN ghcup set ghc 9.4.7 RUN cabal update

  CMD git clone $REPO \ && cd $NAME \ && git checkout $COMMIT \ && cabal install --lib copilot**/ \ --constraint="what4==1.5.1" \ && 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=9ef909503cba54d1df741292230d716dbf30b2fb" -it copilot-verify-461

• [X] Implementation is documented. Details: No documentation needed.
• [X] Change history is clear.
• [X] Commit messages are clear.
• [X] Changelogs are updated.
• [X] Examples are updated. Details: No updates needed.
• [X] Required version bumps are evaluated. Details: Bump not needed (new versions allowed but not required).

[ivanperez-keera]

Change Manager: Implementation ready to be merged.