Skip to content

Commit f5a96ce

Browse files
Merge branch 'develop-bump-what4-dependency'. Close #514.
**Description** `what4` has seen a new release 1.6, but `copilot-theorem` needs versions strictly lower than 1.6. This version is API-compatible for all features used by `copilot-theorem`, but it includes support for GHC 9.8, which we want to also support. **Type** - Management: update versions of dependencies. **Additional context** None. **Requester** - Ryan Scott. **Method to check presence of bug** The following dockerfile installs copilot forcing the use of what4-1.6, 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.8 RUN cabal update CMD git clone $REPO \ && cd $NAME \ && git checkout $COMMIT \ && cabal install --lib copilot**/ \ --constraint="what4>=1.6" \ && 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-514 ``` **Expected result** Executing the image above prints the message "Success", indicating that Copilot can be installed with `what4-1.6`. **Solution implemented** Modify `copilot-theorem`'s cabal file to _also_ accept `what4` versions `>= 1.6` and `<1.7`. No other changes needed to `copilot-theorem` to work with that version of `what4`. **Further notes** None.
2 parents 9e4b1cb + 4cf2dce commit f5a96ce

File tree

2 files changed

+4
-1
lines changed

2 files changed

+4
-1
lines changed

copilot-theorem/CHANGELOG

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
2024-07-06
2+
* What4 upper-bound dependency version bump. (#514)
3+
14
2024-05-07
25
* Version bump (3.19.1). (#512)
36
* Fix handling of unsatisfiable properties with Kind2. (#495)

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.6
64+
, what4 >= 1.3 && < 1.7
6565

6666
, copilot-core >= 3.19.1 && < 3.20
6767
, copilot-prettyprinter >= 3.19.1 && < 3.20

0 commit comments

Comments
 (0)