Skip to content

Commit a93f894

Browse files
Merge branch 'develop-bump-what4-1.7'. Close #611.
**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. 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": ```Dockerfile 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/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-611 ``` **Solution implemented** Bump version bounds on `what4`. **Further notes** None.
2 parents e95cc62 + 1f68f7e commit a93f894

File tree

2 files changed

+3
-2
lines changed

2 files changed

+3
-2
lines changed

copilot-theorem/CHANGELOG

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1-
2025-05-29
1+
2025-07-05
22
* Removed unused pragmas. (#613)
3+
* Relax version constraint on what4. (#611)
34

45
2025-05-07
56
* Version bump (4.4). (#618)

copilot-theorem/copilot-theorem.cabal

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,7 @@ library
6161
, random >= 1.1 && < 1.3
6262
, transformers >= 0.5 && < 0.7
6363
, xml >= 1.3 && < 1.4
64-
, what4 >= 1.3 && < 1.7
64+
, what4 >= 1.3 && < 1.8
6565

6666
, copilot-core >= 4.4 && < 4.5
6767
, copilot-prettyprinter >= 4.4 && < 4.5

0 commit comments

Comments
 (0)