As with any documentation, this guide is most useful if it's promptly updated to reflect changes in processes, development tools, or the Coq ecosystem. If you notice anything inaccurate or outdated, please signal it in a new issue, or fix it in a new pull request. If you find some parts are not sufficiently clear, you may open an issue as well.
- Guide to contributing to the Standard Library of Coq
- Foreword
- Table of contents
- Introduction
- Issues
- Code changes
- Becoming a maintainer
- Release management
- Additional resources
Thank you for your interest in contributing to the Standard Library of Coq! There are many ways to contribute, and we appreciate all of them.
People often begin by making small contributions, and contributions to the ecosystem, before working their way up incrementally to the core parts of the system, and start to propose larger changes, or take an active role in maintaining the system. So this is the way this contributing guide is organized. However, it is by no means necessary that you go through these steps in this order. Feel free to use this guide as a reference and quickly jump to the part that is most relevant to you at the current time.
This document is specific to the Standard Library. For more generic information about contributing to the Coq ecosystem as a whole, one can browse the contributing guide of Coq itself.
Bug reports are enormously useful to identify issues; 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).
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. If unsure, you are always very welcome to ask on our Discourse forum or Zulip chat before, after, or while writing a bug report.
It is better if you can test that your bug is still present in the current testing or development version before reporting it, but if you can't, it should not discourage you from reporting it.
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). Nowadays, the easiest way to
use the Coq bug minimizer is to call it through @coqbot, as documented
here.
Coq has too many bug reports for its core developers alone to manage. You can help a lot by:
- confirming that reported bugs are still active with the current version of Coq;
- determining if the bug is a regression (new, and unexpected, behavior from a recent Coq version);
- more generally, by reproducing a bug, on another system, configuration, another version of Coq, and by documenting what you did;
- giving a judgement about whether the reported behavior is really a bug, or is expected but just improperly documented, or expected and already documented;
- producing a trace if it is relevant and you know how to do it;
- producing another example exhibiting the same bug, or minimizing the initial example using the bug minimizer mentioned above;
- using
git bisectto find the commit that introduced a regression; - fixing the bug if you have an idea of how to do so (see the following section).
Once you have some experience with the issue tracker, you can request to join the contributors team (any member of the maintainer team can give you access. Being in this team will grant you the following access:
- Updating labels: every open issue and pull request should
ideally get one or several
kind:andpart:labels. In particular, valid issues should generally get either akind: bug(the reported behavior can indeed be considered a bug, this can be completed with thekind: anomaly, andkind: regressionlabels),kind: documentation(e.g. if a reported behavior is expected but improperly documented),kind: enhancement(a request for enhancement of an existing feature), orkind: featurelabel (an idea for a new feature). - Creating new labels: if you feel a
part:label is missing, do not hesitate to create it. If you are not sure, you may discuss it with other contributors and developers on Zulip first. - Closing issues: if a bug cannot be reproduced anymore, is a
duplicate, or should not be considered a bug report in the first
place, you should close it. When doing so, try putting an
appropriate
resolved:label to indicate the reason. If the bug has been fixed already, and you know in which version, you can add a milestone to it, even a milestone that's already closed, instead of aresolved:label. When closing a duplicate issue, try to add all the additional info that could be gathered to the original issue. - Editing issue titles: you may want to do so to better reflect the current understanding of the underlying issue.
- Editing comments: feel free to do so to fix typos and formatting
only (in particular, some old comments from the Bugzilla era or
before are not properly formatted). You may also want to edit the
OP's initial comment (a.k.a. body of the issue) to better reflect
the current understanding of the issue, especially if the discussion
is long. If you do so, only add to the original comment, and mark
it clearly with an
EDITED by @YourNickname:. - Hiding comments: when the discussion has become too long, this can be done to hide irrelevant comments (off-topic, outdated or resolved sub-issues).
- Deleting things: please don't delete any comment or issue, our policy doesn't allow for comments to be deleted, unless done by the community moderators. You should hide them instead. An audit log is available to track deleted items if needed (but does not allow recovering them).
However, and contrary to most other repositories, it will not give you the ability to push new branches or tags to the repository. This is disabled because we prefer to use forks to work on feature branches.
Yet to be fully specified: use of priority, difficulty, help wanted,
and good first issue labels, milestones, assignments, and GitHub
projects.
If you want to contribute a documentation update, bug fix or feature
yourself, pull requests (PRs) on the GitHub
repository are the way to contribute directly to the
Coq implementation (all changes, even the smallest changes from core
developers, go through PRs). You will need to create a fork of the
repository on GitHub and push your changes to a new "topic branch" in
that fork (instead of using an existing branch name like master).
PRs should always target the master branch. Make sure that your
copy of this branch is up-to-date before starting to do your changes,
and that there are no conflicts before submitting your PR. If you
need to fix conflicts, we generally prefer that you rebase your branch
on top of master, instead of creating a merge commit.
If you are not familiar with git or GitHub, Sections Git
documentation, tips and tricks,
and GitHub documentation, tips and
tricks, should be helpful (and
even if you are, you might learn a few tricks).
Once you have submitted your PR, it may take some time to get feedback, in the form of reviews from maintainers, and test results from our continuous integration system. Our code owner system will automatically request reviews from relevant maintainers. Then, one maintainer should self-assign the PR (if that does not happen after a few days, feel free to ping the maintainers). The PR assignee will then become your main point of contact for handling the PR: they should ensure that everything is in order and merge when it is the case (you can ping them if the PR is ready from your side but nothing happens for a few days).
After your PR is accepted and merged, it may get backported to a
release branch if appropriate, and will eventually make it to a
release. You do not have to worry about this, it is the role of the
assignee and the release manager to do so (see Section Release
management). The milestone should give you an
indication of when to expect your change to be released (this could be
several months after your PR is merged). That said, you can start
using the latest master branch to take advantage of all the new
features, improvements, and fixes.
Before fixing a bug, it is best to check that it was reported before:
-
If it was already reported and you intend to fix it, self-assign the issue (if you have the permission), or leave a comment marking your intention to work on it (and a contributor with write-access may then assign the issue to you).
-
If the issue already has an assignee, you should check with them if they still intend to work on it. If the assignment is several weeks, months, or even years (!) old, there are good chances that it does not reflect their current priorities.
-
If the bug has not been reported before, it can be a good idea to open an issue about it, while stating that you are preparing a fix. The issue can be the place to discuss about the bug itself while the PR will be the place to discuss your proposed fix.
It is generally a good idea to add a regression test to the test-suite. See the test-suite README for how to do so.
Small fixes do not need any documentation, or changelog update. New,
or updated, user-facing features, and major bug fixes do. See the
corresponding section for
on how to contribute to the documentation, and the README in
[doc/changelog][user-changelog] for how to add a changelog entry.
You should always feel free to open your PR before the documentation, changelog entry and tests are ready. That's the purpose of the checkboxes in the PR template which you can leave unticked. This can be a way of getting reviewers' approval before spending time on writing the documentation (but you should still do it before your PR can be merged).
If even the implementation is not ready but you are still looking for early feedback on your code changes, please use the draft PR mechanism.
If you are looking for feedback on the design of your change, rather than on its implementation, then please refrain from opening a PR. You may open an issue to start a discussion.
When you open or update a PR, you get automatically some feedback. The tests will run on a commit merging your branch with the base branch, so if there is a conflict and this merge cannot be performed automatically, the tests won't run.
If a test fails, you will see in the GitHub PR interface, both the failure of the whole pipeline, and of the specific failed job. Most of these failures indicate problems that should be addressed, but some can still be due to synchronization issues out of your control. In case of doubt, ask the reviewers.
To re-run a specific failed job, you can use the Re-run jobs button in the GitHub interface (if you have the rights).
If you broke the test-suite, you should get many failed jobs, because
the test-suite is run multiple times in various settings. You should
get the same failure locally by running make test-suite
(after having done make and maje install). It's
helpful to run this locally and ensure the test-suite is not broken
before submitting a PR as this will spare a lot of runtime on distant
machines.
To learn more about the test-suite, you should refer to its README.
We have a linter that checks a few different things:
- Every commit can build. This is an important requirement to
allow the use of
git bisectin the future. It should be possible to build every commit, and in principle even the test-suite should pass on every commit (but this isn't tested in CI because it would take too long). A good way to test this locally is to usegit rebase master --exec "make". - No tabs or end-of-line spaces on updated lines. We are trying
to get rid of all tabs and all end-of-line spaces from the code base
(except in some very special files that need them). This checks not
only that you didn't introduce new ones, but also that updated lines
are clean (even if they were there before). You can avoid worrying
about tabs and end-of-line spaces by installing our pre-commit git
hook, which will fix these issues at commit time.
If you are
encountering these issues nonetheless, you can fix them by rebasing
your branch with
git rebase --whitespace=fix. - All files should end with a single newline. See the section Style guide for additional style recommendations.
You may run the linter yourself with dev/lint-repository.sh.
Such a failure can indicate either a bug in your branch, or a breaking change that you introduced voluntarily. All such breaking changes should be properly documented in the [user changelog][user-changelog]. Furthermore, a backward-compatible fix should be found, properly documented in the changelog when non-obvious, and this fix should be merged in the broken projects before your PR to the Coq repository can be.
Note that once the breaking change is well understood, it should not feel like it is your role to fix every project that is affected: as long as reviewers have approved and are ready to integrate your breaking change, you are entitled to (politely) request project authors / maintainers to fix the breakage on their own, or help you fix it. Obviously, you should leave enough time for this to happen (you cannot expect a project maintainer to allocate time for this as soon as you request it) and you should be ready to listen to more feedback and reconsider the impact of your change.
The reviews you get are highly dependent on the kind of changes you did. In any case, you should always remember that reviewers are friendly volunteers that do their best to help you get your changes in. But at the same time, they try to ensure that code that is introduced or updated is of the highest quality and will be easy to maintain in the future, and that's why they may ask you to perform small or even large changes. If you need a clarification, do not hesitate to ask.
Here are a few labels that reviewers may add to your PR to track its status. In general, this will come in addition to comments from the reviewers, with specific requests.
- needs: fixing indicates the PR needs a fix, as discussed in the comments.
- needs: documentation indicates the PR introduces changes that should be documented before it can be merged. This label may be used to reflect that the corresponding checkbox is not yet checked in the PR template (so that we don't forget when we intend to merge the PR).
- needs: changelog entry indicates the PR introduces changes that should be documented in the [user changelog][user-changelog]. Similarly to the previous label, this may be used to reflect that the corresponding checkbox is not yet checked in the PR template.
- needs: test-suite update indicates that tests should be added to the test-suite / modified to ensure that the changes are properly tested. Similarly to the previous two labels, this may be used to reflect that the corresponding checkbox is not yet checked in the PR template.
More generally, such labels should come with a description that should allow you to understand what they mean.
If you have changes to perform before your PR can be merged, you might want to do them in separate commits at first to ease the reviewers' task, but we generally appreciate that they are squashed with the commits that they fix before merging. This is especially true of commits fixing previously introduced bugs or failures.
The documentation is usually a good place to start contributing, because you can get used to the pull request submitting and review process, without needing to learn about the code source of Coq at the same time.
The official documentation is formed of two components:
The sources of the reference manual are located in the
doc/sphinx directory. They are written in rst
(Sphinx) format with some Coq-specific extensions, which are
documented in the README in the above directory.
This README was written to be read from begin to end. As soon as your
edits to the documentation are more than changing the textual content,
we strongly encourage you to read this document.
The documentation of the standard library is generated with coqdoc from the comments in the sources of the standard library.
The README in the doc directory contains more
information about the documentation's build dependencies, and the
make targets.
You can browse through the list of open documentation issues using the kind: documentation label, or the user documentation GitHub project (you can look in particular at the "Writing" and "Fixing" columns).
Contributing to the standard library is also made easier by not having to learn about Coq's internals, and its implementation language.
Due to the compatibility constraints created by the many projects that depend on it, proposing breaking changes, will usually require to go through a specific process, with a deprecation phase. Additions, such as contributing new lemmas on existing definitions, and clean-ups of existing proofs are easier contributions to start with. In case of doubt, ask in an issue before spending too much time preparing your PR.
If you create a new file, it needs to be listed in
doc/stdlib/index-list.html.
Add coqdoc comments to extend the standard library documentation. See the coqdoc documentation to learn more.
You can start reviewing PRs as soon as you feel comfortable doing so (anyone can review anything, although some designated reviewers will have to give a final approval before a PR can be merged, as is explained in the next sub-section).
Reviewers should ensure that the code that is changed or introduced is
in good shape and will not be a burden to maintain, is unlikely to
break anything, or the compatibility-breakage has been identified and
validated, includes documentation, changelog entries, and test files
when necessary. Reviewers can use needs: labels, or change requests
to further emphasize what remains to be changed before they can approve
the PR. Once reviewers are satisfied (regarding the part they
reviewed), they should formally approve the PR, possibly stating what
they reviewed.
That being said, reviewers should also make sure that they do not make the contributing process harder than necessary: they should make it clear which comments are really required to perform before approving, and which are just suggestions. They should strive to reduce the number of rounds of feedback that are needed by posting most of their comments at the same time. If they are opposed to the change, they should clearly say so from the beginning to avoid the contributor spending time in vain. They should avoid making nitpick comments when in fact, they have larger concerns that should be addressed first (these larger concerns should then be made very clear).
Furthermore, when reviewing a first contribution (GitHub highlights first-time contributors), be extra careful to be welcoming, whatever the decision on the PR is. When approving a PR, consider thanking the newcomer for their contribution, even if it is a very small one (in cases where, if the PR had come from a regular contributor, it would have felt OK to just merge it without comment). When rejecting a PR, take some extra steps to explain the reasons, so that it doesn't feel hurtful. Don't hesitate to still thank the contributor and possibly redirect them to smaller tasks that might be more appropriate for a newcomer.
Beyond making suggestions to a PR author during the review process, you may want to collaborate further by checking out the code, making changes, and pushing them. There are two main ways of doing this:
- Pull requests on pull requests: You can checkout the PR branch (GitHub provides the link to the remote to pull from and the branch name on the top and the bottom of the PR discussion thread), checkout a new personal branch from there, do some changes, commit them, push to your fork, and open a new PR on the PR author's fork.
- Pushing to the PR branch: If the PR author has not unchecked the "Allow edit from maintainers" checkbox, and you have write-access to the repository (i.e. you are in the @coq/contributors team), then you can also push (and even force-push) directly to the PR branch, on the main author's fork. Obviously, don't do it without coordinating with the PR author first (in particular, in case you need to force-push).
When several people have co-authored a single commit (e.g. because someone fixed something in a commit initially authored by someone else), this should be reflected by adding "Co-authored-by:" tags at the end of the commit message. The line should contain the co-author name and committer e-mail address.
Our CODEOWNERS file associates a team of maintainers to each component. When a PR is opened (or a draft PR is marked as ready for review), GitHub will automatically request reviews to maintainer teams of affected components. As soon as it is the case, one available member of a team that was requested a review should self-assign the PR, and will act as its shepherd from then on.
The PR assignee is responsible for making sure that all the proposed changes have been reviewed by relevant maintainers (at least one reviewer for each component that is significantly affected), that change requests have been implemented, that CI is passing, and eventually will be the one who merges the PR.
The PR assignee may use their own judgement to decide to merge a PR that has not received reviews from all maintainers of affected components, depending on how large or controversial the changes to these components are. It is also admissible to have an assignee who is not a maintainer of any of the affected components, in case relevant maintainers are not available, and as long as the assignee has push right and is able to understand the changes in the PR.
If you have already frequently contributed to a component, we would be happy to have you join the maintainer team.
-
Before merging, the assignee must also select a milestone for the PR (see also Section Release management).
-
When a PR has overlays, then:
- the overlays should have been merged before the PR can be merged; the overlays should then be cleaned up and CI relaunched without them to ensure everything is fine before merging.
We are always happy to have more people involved in the PR reviewing and merging process, so do not hesitate to propose yourself if you already have experience on a component.
Maintainers can leave at any time but you should always announce it to other maintainers.
TBD, likely to follow Coq releases
The RM role does not include the task of making Coq available through the various package managers out there: several contributors (most often external to the development team) take care of this, and we thank them for this. If your preferred package manager does not include Coq, it is a very worthy contribution to make it available there. But be careful not to let a package get outdated, as this could lead some users to install an outdated version of Coq without even being aware of it. Beyond packaging Coq, you might want to consider packaging the rest of Coq packages available to users through the Coq Platform. In this case, it would be helpful if you try to favor the same versions as in the Coq Platform.
The Windows and macOS installers are created as part of the preparation of the Coq Platform.
-
You can find developer resources in the
devdirectory, and more specifically developer documentation indev/doc. The README in thedevdirectory lists what's available.For example,
dev/doc/README.mdis a beginner's guide to hacking Coq, and documentation on debugging Coq can be found indev/doc/debugging.md. -
When it makes sense, the documentation is kept even closer to the sources, in README files in various directories (e.g. the test-suite README or the refman README).
The standard library depends on Coq itself.
Run make to build everything, then make install to install.
Continuous integration (CI) testing is key in ensuring that the
master branch is kept in a well-functioning state at all times, and
that no accidental compatibility breakages are introduced. Our CI is
quite extensive since it includes testing many external projects, some
of them taking more than an hour to compile. However, you can get
partial results much more quickly (when our CI is not overloaded).
The main documentation resource on our CI is the README.
When CI has a few failures which look spurious, restarting the corresponding jobs is a good way to ensure this was indeed the case. Most failed jobs can be restarted directly from the "Checks" tab on GitHub.
TBD
Lots of resources about git, the version control system, are available on the web, starting with the official website.
We recommend a setup with two configured remotes, one for the official
Coq repository, called upstream, and one for your fork, called
origin. Here is a way to do this for a clean clone:
git clone https://github.com/coq-community/stdlib -o upstream
cd stdlib
git remote add origin [email protected]:$YOURNAME/stdlib
# Make sure you click the fork button on GitHub so that this repository exists
cp dev/tools/pre-commit .git/hooks/ # Setup the pre-commit hookThen, if you want to prepare a fix:
# Make sure we start from an up-to-date master
git checkout master
git pull --ff-only # If this fails, then your master branch is messy
git checkout -b my-topic-branch
# Modify some files
git add .
# Every untracked or modified file will be included in the next commit
# You can also replace the dot with an explicit list of files
git commit -m "My commit summary.
You can add more information on multiple lines,
but you need to skip a line first."
git push -u origin my-topic-branch
# Next time, you push to this branch, you can just do git pushWhen you push a new branch for the first time, GitHub gives you a link to open a PR.
If you need to fix the last commit in your branch (typically, if your
branch has a single commit on top of master), you can do so with
git add .
git commit --amend --no-edit
If you need to fix another commit in your branch, or if you need to
fix a conflict with master, you will need to learn about git rebase.
GitHub provides a short introduction to git rebase.
GitHub has extensive documentation about everything you
can do on the platform, and tips about using git as well. See in
particular, how to configure your commit e-mail
address and how to open a PR from a
fork.
"Watching" this repository can result in a very large number of notifications. We recommend you, either, configure your mailbox to handle incoming notifications efficiently, or you read your notifications within a web browser. You can configure how you receive notifications in your GitHub settings, you can use the GitHub interface to mark as read, save for later or mute threads. Nowadays, you have also the option to watch only part of the activity (only issues, only PRs, only releases, etc.).
Draft PRs are a mechanism proposed by GitHub to open a pull request before it is ready for review.
Opening a draft PR is a way of announcing a change and seeking early feedback without formally requesting maintainers' reviews. Indeed, you should avoid cluttering our maintainers' review request lists before a change is ready on your side.
When opening a draft PR, make sure to give it a descriptive enough title so that interested developers still notice it in their notification feed. You may also advertise it by talking about it in our developer chat. If you know which developer would be able to provide useful feedback to you, you may also ping them.
If a PR was opened as ready for review, but it turns out that it still needs work, it can be transformed into a draft PR.
In this case, previous review requests won't be removed automatically. Someone with write access to the repository should remove them manually. Afterwards, upon marking the PR as ready for review, someone with write access will have to manually add the review requests that were previously removed.
We have a Discourse forum (see in particular the Coq development category) and a Zulip chat (see in particular the Coq devs & plugin devs stream). Feel free to join any of them and ask questions. People are generally happy to help and very reactive.
Obviously, the issue tracker is also a good place to ask questions, especially if the development processes are unclear, or the developer documentation should be improved.