Skip to content

Update PR instructions in CONTRIBUTING.md #31

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jcailler wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Update PR instructions in CONTRIBUTING.md #31

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ coqproofs
*.glob
*.vo[ks]
*.vo
GIT_TIPS.md

*.v
!goeland.v
Expand Down
51 changes: 39 additions & 12 deletions CONTRIBUTING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ wish to contribute to Goéland, you should start by
you can work on on your feature/bug fix/enhancement in your local repository.

Once you deem your work satisfactory, you should [open a pull
request](https://github.com/GoelandProver/Goeland/compare) **targeting
master**. Then, one of the maintainer will review your code as soon as
request](#working-with-pull-requests) targeting
master. Then, one of the maintainer will review your code as soon as
possible. If you have no feedback for a few days, do not hesitate to ping one of
them. The current maintainers are: @jcailler, @jrosain.

Expand All @@ -20,8 +20,8 @@ maintainers will trigger the CI when he sees fit. You may check soundness
locally by running the `ci-soundness` target of the [devtools](devtools)
folder. Note that it is **not** the maintainer's responsibility to make your
modifications compatible with the master's branch. If there are any conflicts,
you are expected to solve them by *rebasing your branch on top of upstream's
master*.
you are expected to solve them by rebasing your branch on top of upstream's
master.

If you are solving a bug referenced in the issue tracker, do not forget to link
it in the PR.
Expand All @@ -41,12 +41,39 @@ flag in order for them to panic and you to have a backtrace.

## For Maintainers

By default, a pull request that modifies the go source code has the `needs:ci` label. You
may trigger CI jobs by adding the label `request:ci`, which will remove the `needs:ci` if
it succeeds. Every time a new push is done on the pull request's branch, the `needs:ci`
label will reappear. Try to never remove this label by hand, it is good practice to
request a successful full ci run before merging the PR into the master's branch. Moreover,
it is your responsibility to put the right `part:` and `kind:` labels.
By default, a pull request that modifies the go source code has the `needs:ci`
label. You may trigger CI jobs by adding the label `request:ci`, which will
remove the `needs:ci` if it succeeds. Every time a new push is done on the pull
request's branch, the `needs:ci` label will reappear. Avoid removing this label
by hand, and always prefer requesting the CI.

Once you approve the modifications, you should add the target milestone (i.e.,
which version of Goéland should include the patch) before merging.
It is the maintainer’s responsibility to:
- add the appropriate `part:` and `kind:` labels,
- approve changes once ready,
- assign a milestone indicating the target Goéland release (i.e., which version of Goéland should include the patch) before merging.


## Working with Pull Requests

Before opening a pull request, make sure your branch is up-to-date with the master's branch of `GoelandProver/Goeland` or at least mergeable without conflicts. You can update your branch using:

```bash
git fetch remote/master
git rebase remote/master
```

where `remote` is the name of the remote fetching `git@github.com:GoelandProver/Goeland.git` (which can be found using `git remote -v`)

Copy link
Member

@jrosain jrosain Aug 29, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel like a transition is missing between these two paragraphs. Maybe something like: "If you want to open a pull request, you should roughly follow these steps:"

1. Check that the branch with your new features/bug fixes is up-to-date.
2. Open a pull request [here](https://github.com/GoelandProver/Goeland/compare) targeting `master`.
3. Give an explicit name to your pull request, e.g., `Fix nil pointer exception when skolemizing` or `Add a library of maps`.
4. If your pull request is a bug fix, be sure to add `Closes: #???` where `#???` is the issue you are closing/fixing.
5. In any case, describe briefly what you did in the code and what are the technical points that might be of interest / things you are not sure about on the design you chose.
6. If you have updated the test-suite, list all the updates you did.
7. In particular, if you fixed a bug, you should have updated the test suite with the problem `.p` where the bug appeared (or a minimized version) in the `devtools/test-suite/bugs` folder and named it `bug_???.p` (or `bug_???-n.p` if there are multiple bugs).
8. If you introduce a new feature, you might add problems in the `devtool/test-suite/basic` or `devtool/test-suite/proofs` folders, and update the unit tests.
9. Once everything is clear, you can submit your PR and wait until a reviewer gets back to you.

Maintainers may ask you to squash your commits to simplify the history. However, squashing is not always required — in some cases, preserving the commit history is preferred. Wait for a maintainer's guidance before squashing.

Subsequently, if you have any further question, the reviewer will answer them.