Exercism Coq Track
Exercism exercises in Coq.
Setup
There are 2 ways to install Coq:
- [Recommended] Using OPAM package manger: https://coq.inria.fr/opam/www/using.html
- [Alternative] Directly download Coq binaries from the official site: https://coq.inria.fr/download
For editing Coq sources we recomend using one of the following:
- [Recommended] Emacs editor with ProofGeneral and CompanyCoq. See https://github.com/cpitclaudel/company-coq for installation instructions.
- [Alternative] Using CoqIDE
Presently, exercises do not require any additional Coq libraries. Recommended version of Coq: 8.6
Contributing
Thank you so much for contributing!
Please read about how to get involved in a track. Be sure to read the Exercism Code of Conduct.
We welcome pull requests of all kinds. No contribution is too small.
We encourage contributions that provide fixes and improvements to existing exercises. Please note that this track's exercises must conform to the Exercism-wide standards described in the documentation. If you're unsure about how to make a change, then go ahead and open a GitHub issue, and we'll discuss it.
Exercise Tests
At the most basic level, Exercism is all about the tests. You can read more about how we think about test suites in the Exercism documentation.
Test files should use the following format:
Theorem TautologyExercise: True.
Proof.
(* Add your proof here *)
Qed.
Opening an Issue
If you plan to make significant or breaking changes, please open an issue so we can discuss it first. If this is a discussion that is relevant to more than just the Coq track, please open an issue in exercism/discussions.
Submitting a Pull Request
Pull requests should be focused on a single exercise, issue, or conceptually cohesive change. Please refer to Exercism's pull request guidelines.
Verifying Your Change
Before submitting your pull request, you'll want to verify the changes in two ways:
- Run all the tests for the Coq exercises
- Run an Exercism-specific linter to verify the track
All the tests for Coq exercises can be run from the top level of the repo with
# TODO: add this command
For the Exercism-specific linting, please see the documentation.
Contributing a New Exercise
Please see the documentation about adding new exercises.