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

Question

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

Closed this issue a year ago · 8 comments

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?

Answer 1 · 2023-10-31T06:27:07.000Z

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

Answer 2 · 2023-11-01T06:46:13.000Z

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.

Answer 3 · 2023-11-01T06:47:11.000Z

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

Answer 4 · 2023-11-01T06:47:29.000Z

Technical Lead: Confirmed that the issue should be addressed.

Answer 5 · 2023-11-01T07:11:55.000Z

Technical Lead: Bug scheduled for fixing in Copilot 3.17.

Fix assigned to: @ivanperez-keera.

Answer 6 · 2023-11-04T07:39:49.000Z

Implementor: Solution implemented, review requested.

Answer 7 · 2023-11-04T15:08:49.000Z

Change Manager: Verified that:

Solution is implemented:

The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/267041967
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

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

Answer 8 · 2023-11-04T15:09:09.000Z

Change Manager: Implementation ready to be merged.