Skip to content

Commit 320b471

Browse files
Merge branch 'develop-remove-forall'. Close #518.
**Description** The function `Copilot.Language.Spec.forall` was deprecated due to the function name not being allowed in newer versions of GHC. An alternative was provided, so the old function is not being used by any part of Copilot. The original functions was deprecated in Copilot 3.18 and no messages have been received requesting that they be kept in this library. As per our internal policy of waiting 3 versions from deprecation until a public interface declaration can be removed, these functions can now be removed. **Type** - Bug: unused code included in the implementation. **Additional context** - Issue #470 , addressed in Copilot 3.18, deprecated the function. **Requester** - Ivan Perez **Method to check presence of bug** Although this is not a bug per se, compiling with GHC >= 9.4 and --ghc-options='-Werror=forall-identifier' produces an error due to including a function called `forall`, which is not allowed in new versions of GHC. The following dockerfile installs copilot with GHC 9.8 and `--ghc-options='-Werror=forall-identifier'`, and prints the message "Success" if installation completes: ```Dockerfile FROM ubuntu:focal ENV DEBIAN_FRONTEND=noninteractive 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 RUN apt-get install --yes pkg-config SHELL ["/bin/bash", "-c"] RUN ghcup install ghc 9.8.2 RUN ghcup install cabal 3.2 RUN ghcup set ghc 9.8.2 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 --ghc-option="-Werror=forall-identifier" $NAME/**/ \ && 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-518 ``` **Expected result** Running the dockerfile above prints the message success, indicating that Copilot does not define the identifier `forall` anywhere. **Solution implemented** Remove the deprecated function `Copilot.Language.Spec.forall`, and any references to it (exports). Adjust README to indicate that copilot now compiles with GHC 9.8. **Further notes** None.
2 parents f5a96ce + 7c8e7dd commit 320b471

File tree

5 files changed

+9
-8
lines changed

5 files changed

+9
-8
lines changed

copilot-language/CHANGELOG

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
2024-07-06
2+
* Remove deprecated function Copilot.Language.Spec.forall. (#518)
3+
14
2024-05-07
25
* Version bump (3.19.1). (#512)
36

copilot-language/src/Copilot/Language.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ module Copilot.Language
3838
, prop
3939
, theorem
4040
, forAll
41-
, forall, exists
41+
, exists
4242
) where
4343

4444
import Data.Int hiding (Int)

copilot-language/src/Copilot/Language/Spec.hs

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ module Copilot.Language.Spec
2828
, prop, properties
2929
, theorem, theorems
3030
, forAll
31-
, forall, exists
31+
, exists
3232
, extractProp
3333
, Universal, Existential
3434
) where
@@ -165,11 +165,6 @@ data Prop a where
165165
forAll :: Stream Bool -> Prop Universal
166166
forAll = Forall
167167

168-
{-# DEPRECATED forall "Use forAll instead." #-}
169-
-- | Universal quantification of boolean streams over time.
170-
forall :: Stream Bool -> Prop Universal
171-
forall = forAll
172-
173168
-- | Existential quantification of boolean streams over time.
174169
exists :: Stream Bool -> Prop Existential
175170
exists = Exists

copilot/CHANGELOG

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
2024-07-06
2+
* Update README to reflect support for GHC 9.8. (#518)
3+
14
2024-05-07
25
* Version bump (3.19.1). (#512)
36

copilot/README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ ghci> ghci> Leaving GHCi.
8181
On other Linux distributions or older Debian-based distributions, to use
8282
Copilot you must install a Haskell compiler (GHC) and the package manager
8383
Cabal. We currently support all versions of GHC from 8.6.5 to modern versions
84-
(9.6 as of this writing). You can install the toolchain using
84+
(9.8 as of this writing). You can install the toolchain using
8585
[ghcup](https://www.haskell.org/ghcup/) or, if you are on Debian/Ubuntu,
8686
directly with `apt-get`:
8787

0 commit comments

Comments
 (0)