Creating and Reviewing Pull Requests (PRs)

General information about PRs

PRs to MathComp can be created in the standard way, as documented, say, here on github.com.

If you read a PR and have an opinion about it, it is fine to submit even a partial comment ASAP.

Checklist for reviewing a PR

What to do?

1. Perform the "Bureaucratic" and "Contents" checks explained below.
2. Write a review about the contents of the changed files, asking for changes if necessary.
3. (Optional) Contribute by suggesting more changes or even commits and PRs of your own.
4. If help is needed, it is fine to tag others and ask for advice.

Bureaucratic checks

• Is the PR rebased or at least mergable with master? Do not use github interface to solve conflicts!
• Is the history "tidy" (i.e., it consists of an optimum number of meaningful commits)?
  • History is linear, i.e., there are no merges.
  • Each commit compiles.
  • Commits are atomic, i.e. they don't contain unrelated changes.
  • Each commit has a good log message.
  • Otherwise, adjust with an interactive rebase (and a push-force).
  • The default merge policy is to perform merge pull requests, i.e., PRs are not squashed by default.
• Are the changelog and the documentation present and complete?
• Is there a milestone?
• Does the PR compile without warnings? (when in doubt, check locally, CI is bad at displaying warnings)
• Are the automatic checks done by the CI successful?
  • Otherwise, prepare an overlay as described in How-to-add-overlays-for-PRs.

Contents checks

• Are the changelog and the documentation understandable?
• Is the naming convention consistent locally and with the library?
• Do the proof scripts abide by the contributing guide?
• Are the modifications located in the right part of the section/file/package/library?
• Are the results general/specific enough? Are they superseeded by material from the library?
  • If necessary, checkout the contents in a local workdir and try to find limits and corner cases.
• Check if updates meet all reviewers' recommendations and that nothing non-reviewed has been introduced.
• If all checks are successful:
  • Merge by creating a merge commit.
  • Otherwise, identify what is missing.

About the distinction assignee/reviewer

Ideally, each PR should have an assignee in charge of finding reviewers.

Advanced topics

Efficiency concerns may arise when manipulating more than one pull request on a single machine, in which case it might be worth using git's worktrees and nix-shell to save disk space and compilation time. This tutorial explains a workflow using these tools.