Thank you for your interest in contributing to Coq! There are many ways to contribute, and we appreciate all of them.
Bug reports are enormously useful to identify issues with Coq; we can't fix what we don't know about. To report a bug, please open an issue in the Coq issue tracker (you'll need a GitHub account). You can file a bug for any of the following:
- An anomaly. These are always considered bugs, so Coq will even ask you to file a bug report!
- An error you didn't expect. If you're not sure whether it's a bug or intentional, feel free to file a bug anyway. We may want to improve the documentation or error message.
- Missing documentation. It's helpful to track where the documentation should be improved, so please file a bug if you can't find or don't understand some bit of documentation.
- An error message that wasn't as helpful as you'd like. Bonus points for suggesting what information would have helped you.
- Bugs in CoqIDE should also be filed in the Coq issue tracker. Bugs in the Emacs plugin should be filed against ProofGeneral, or against company-coq if they are specific to company-coq features.
It would help if you search the existing issues before reporting a bug. This can be difficult, so consider it extra credit. We don't mind duplicate bug reports.
When it applies, it's extremely helpful for bug reports to include sample code, and much better if the code is self-contained and complete. It's not necessary to minimize your bug or identify precisely where the issue is, since someone else can often do this if you include a complete example. We tend to include the code in the bug description itself, but if you have a very large input file then you can add it as an attachment.
If you want to minimize your bug (or help minimize someone else's) for more extra credit, then you can use the Coq bug minimizer (specifically, the bug minimizer is the find-bug.py script in that repo).
Beginner's guide to hacking Coq: dev/doc/README.md
Development information and tools: dev/README.md
If you want to contribute a bug fix or feature yourself, pull requests on the GitHub repository are the way to contribute directly to the Coq implementation. We recommend you create a fork of the repository on GitHub and push your changes to a new "topic branch" in that fork. From there you can follow the GitHub pull request documentation to get your changes reviewed and pulled into the Coq source repository.
Documentation for getting started with the Coq sources is located in various
files in dev/doc (for example, debugging.md).
For further help with the Coq sources, feel free to join
the Coq Gitter chat and ask questions.
Please make pull requests against the master branch.
If it's your first significant contribution to Coq (significant means: more
than fixing a typo), your pull request should include a commit adding your name
to the CREDITS file (possibly with the name of your
institution / employer if relevant to your contribution, an ORCID if you have
one —you may log into https://orcid.org/ using your institutional account to
get one—, and the year of your contribution).
It's helpful to run the Coq test suite with make test-suite before submitting
your change. Our CI runs this test suite and lots of other tests, including
building external Coq developments, on every pull request, but these results
take significantly longer to come back (on the order of a few hours). Running
the test suite locally will take somewhere around 10-15 minutes. Refer to
dev/ci/README.md for more
information on CI tests, including how to run them on your private branches.
If your pull request fixes a bug, please consider adding a regression test as
well. See test-suite/README.md for how to do so.
If your pull request fixes a critical bug (a bug allowing a proof of False),
please add an entry to dev/doc/critical-bugs.
Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq master branch to take advantage of all the new features, improvements, and fixes.
Whitespace discipline (do not indent using tabs, no trailing spaces, text files end with newlines) is checked by Travis (using git diff --check). We ship a dev/tools/pre-commit git hook which fixes these errors at commit time. configure automatically sets you up to use it, unless you already have a hook at .git/hooks/pre-commit.
Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests.
- needs: rebase indicates the PR should be rebased on top of
the latest base branch (usually
master). See the GitHub documentation for a brief introduction to usinggit rebase. This label will be automatically added if you open or synchronize your PR and it is not up-to-date with the base branch. So please, do not forget to rebase your branch every time you update it. - needs: fixing indicates the PR needs a fix, as discussed in the comments.
- needs: benchmarking and needs: testing indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different infrastructure (documented in the wiki). Unless some followup is specifically requested you aren't expected to do this additional testing.
To learn more about the merging process, you can read the merging documentation for Coq maintainers.
Currently the process for contributing to the documentation is the same as for changing anything else in Coq, so please submit a pull request as described above.
Our issue tracker includes a flag to mark bugs related to documentation. You can view a list of documentation-related bugs using a GitHub issue search. Many of these bugs can be fixed by contributing writing, without knowledge of Coq's OCaml source code.
The sources for the Coq reference manual are at doc/sphinx. These are written in reStructuredText and compiled to HTML and PDF with Sphinx.
You may also contribute to the informal documentation available in Cocorico (the Coq wiki), and the Coq FAQ. Both of these are editable by anyone with a GitHub account.
If you want to follow the development activity around Coq, you are encouraged to subscribe to the Coqdev mailing list. This mailing list has reasonably low traffic.
You may also choose to use GitHub feature to "watch" this repository, but be advised that this means receiving a very large number of notifications. GitHub gives some advice on how to configure your e-mail client to filter these notifications. A possible alternative is to deactivate e-mail notifications and manage your GitHub web notifications using a tool such as Octobox.
There are many useful ways to contribute to the Coq ecosystem that don't involve the Coq repository.
Tutorials to teach Coq, and especially to teach particular advanced features, would be much appreciated. Some tutorials are listed on the Coq website. If you would like to add a link to this list, please make a pull request against the Coq website repository at https://github.com/coq/www.
External plugins / libraries contribute to create a successful ecosystem around Coq. If your external development is mature enough, you may consider submitting it for addition to our CI tests. Refer to dev/ci/README.md for more information.
Ask and answer questions on Stack Exchange which has a helpful community of Coq users.
Hang out on the Coq IRC channel, irc://irc.freenode.net/#coq, and help answer questions.