Skip to content

Commit

Permalink
Merge branch 'develop-what4-versions'. Close #461.
Browse files Browse the repository at this point in the history
**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**

The following Dockerfile checks Copilot can be installed with what4-1.5.1, in
which case it prints the message Success:

```Dockerfile
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):
```sh
$ docker run -e "REPO=https://github.com/copilot-language/copilot" -e "NAME=copilot" -e "COMMIT=<commit_hash>" copilot-verify-461
```

**Expected result**

Running the docker image above prints the message "Success", indicating that
Copilot can be installed with `what4-1.5.1`.

**Solution implemented**

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

**Further notes**

None.
  • Loading branch information
ivanperez-keera committed Nov 4, 2023
2 parents 87c6a63 + 9ef9095 commit 526cb74
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 1 deletion.
3 changes: 3 additions & 0 deletions copilot-theorem/CHANGELOG
Original file line number Diff line number Diff line change
@@ -1,3 +1,6 @@
2023-11-03
* Relax version constraint on what4. (#461)

2023-09-07
* Version bump (3.16.1). (#455)

Expand Down
2 changes: 1 addition & 1 deletion copilot-theorem/copilot-theorem.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ library
, random >= 1.1 && < 1.3
, transformers >= 0.5 && < 0.7
, xml >= 1.3 && < 1.4
, what4 >= 1.3 && < 1.5
, what4 >= 1.3 && < 1.6

, copilot-core >= 3.16.1 && < 3.17
, copilot-prettyprinter >= 3.16.1 && < 3.17
Expand Down

0 comments on commit 526cb74

Please sign in to comment.