Closed ivanperez-keera closed 6 months ago
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/268053781
[X] The solution proposed produces the expected result. Details:
The following Dockerfile checks that the function forall
has been deprecated and that the new function is offered, in which case prints the message Success
. We cannot yet use a test that will produce a failure (expected) if forall is defined (i.e., with -Werror=forall-keyword
) because we have to deprecate the function before we remove it.
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.2 RUN ghcup set ghc 9.4.8 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 \ && cabal v1-install copilot/**/ \ && ! cabal v1-exec -- runhaskell -Werror=deprecations <<< 'import Copilot.Language (true, forall, theorem); spec = theorem "true" (forall true); main :: IO (); main = pure ();' \ && cabal v1-exec -- runhaskell -Werror=forall-identifier -Werror=deprecations <<< 'import Copilot.Language (true, forAll, theorem); spec = theorem "true" (forAll true); main :: IO (); main = pure ();' \ && echo "Success"
Command (adjust repo as necessary):
$ docker run -e "REPO=https://github.com/ivanperez-keera/copilot" -e "NAME=copilot" -e "COMMIT=a7aa7678d98de2be69dd4011cb2ddac373654798" -it copilot-verify-470
copilot
and copilot-theorem
repos use forall
, and they are updated to use forAll
.
Introduce a new function
Copilot.Language.Spec.forAll
that implements the behavior currently implemented byCopilot.Language.Spec.forall
, replacing all uses of the old function name and deprecating the old variant, as prescribed in the solution proposed for #470.