Comments (7)
Description
The Copilot API offers the function Copilot.Language.Spec.forall
, which future versions of GHC will disallow.
To ensure that Copilot keeps working with future versions of the compiler, this function should be renamed.
Type
- Management: change to keep Copilot working with future versions of the language/compiler.
Additional context
The proposal was filed in ghc-proposals/ghc-proposals#281, and subsequently accepted in GHC. Details are also available at: https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wforall-identifier.
Requester
- Ivan Perez
Method to check presence of bug
Although not a bug, it is possible to detect the presence of this issue by compiling with GHC >= 9.4. Using -Werror=forall-identifier
will make the issue become a compile-time error.
Expected result
Compiling with GHC >= 9.4 and --ghc-options='-Werror=forall-identifier'
should complete without errors.
Desired result
Compiling with GHC >= 9.4 and --ghc-options='-Werror=forall-identifier'
should complete without errors.
Proposed solution
Introduce a new function forAll
that implements the behavior currently implemented by forall
.
Replace all references of forall
to point to forAll
.
Deprecate forall
, and schedule for removal in a future release of Copilot.
Further notes
None.
from copilot.
Change Manager: Confirmed that the issue manifests.
from copilot.
Technical Lead: Confirmed that the issue should be addressed.
from copilot.
Technical Lead: Bug scheduled for fixing in Copilot 3.18.
Fix assigned to: @ivanperez-keera.
from copilot.
Implementor: Solution implemented, review requested.
from copilot.
Change Manager: Verified that:
- Solution is implemented:
-
The code proposed compiles and passes all tests. Details:
Build log: https://app.travis-ci.com/github/Copilot-Language/copilot/builds/268053781 -
The solution proposed produces the expected result. Details:
The following Dockerfile checks that the functionforall
has been deprecated and that the new function is offered, in which case prints the messageSuccess
. We cannot yet use a test that will produce a failure (expected) ifforall
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 $NAME/**/ \ && ! 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
-
- Implementation is documented. Details:
The new function copies the documentation from the prior one. - Change history is clear.
- Commit messages are clear.
- Changelogs are updated.
- Examples are updated. Details:
Multiple examples in thecopilot
andcopilot-theorem
repos useforall
, and they are updated to useforAll
. - Required version bumps are evaluated. Details:
Bump needed. This alters the public API.
from copilot.
Change Manager: Implementation ready to be merged.
from copilot.
Related Issues (20)
- `copilot-c99`: compiler warnings during tests HOT 10
- `copilot-c99`: compliance with MISRA C 2012 HOT 8
- `copilot-theorem`: Introduce testing infrastructure HOT 6
- `copilot-libraries`: Introduce testing infrastructure HOT 6
- `copilot`: Update README to reflect new contribution process
- `copilot-core`: record field `uTypeType` is unnecessary
- Release 3.18 HOT 6
- `copilot`: Extend range of versions `optparse-applicative` HOT 6
- `copilot-theorem`: Failure to compile with GHC 9.6.3 HOT 6
- Release 3.18.1 HOT 6
- `copilot-theorem`: `kind2Prover` gives parse error when disproving a property HOT 10
- ' ' is not a nondigit error HOT 4
- Formal methods with stateful functions HOT 4
- `copilot-core`: Remove deprecated functions in `Copilot.Core.Type` and `Copilot.Core.Type.Array` HOT 6
- `copilot-core`: Increase test coverage HOT 6
- Release 3.19 HOT 6
- `copilot-c99`: Can C99 generator declare stream functions as static? HOT 12
- Release 3.19.1 HOT 6
- `copilot-theorem`: Extend range of versions `what4` to include 1.6 HOT 7
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from copilot.