Stream: math-comp devs

Topic: using coqbot to rebase

Cyril Cohen (Sep 03 2020 at 12:08):

@Théo Zimmermann we use coqbot in math-comp github PR, I think the only thing it does is to add the label "needs: rebase" sometimes. Can we use it to say "@coqbot: rebase now", in order to rebase a PR which has a potentially trivial rebase?

Cyril Cohen (Sep 03 2020 at 12:10):

(I often just do git checkout X; git pull --rebase upstream master; git push -f origin X)

Théo Zimmermann (Sep 03 2020 at 12:14):

In principle, coqbot doesn't add the needs: rebase label when there are conflicts that can be auto-solved. Is this because your git config has some additional parameters that make some conflicts be solved automatically?

Cyril Cohen (Sep 03 2020 at 12:14):

precisely

Cyril Cohen (Sep 03 2020 at 12:15):

(gitattribute merge union strategy for CHANGELOG_UNRELEASED.md)

Cyril Cohen (Sep 03 2020 at 12:15):

I'm not very concerned about the "needs: rebase" but I'd like to stop being the limiting factor for rebasing my own pull-requests

Cyril Cohen (Sep 03 2020 at 12:16):

hence the question about coqbot powers

Théo Zimmermann (Sep 03 2020 at 12:21):

I'm surprised coqbot didn't pick this strategy automatically from the .gitattributes file...

Théo Zimmermann (Sep 03 2020 at 12:23):

You wrote "Github does not support this yet though" in your PR introducing it. Does this mean that one needs some particular version of git or some local git configuration in addition for this to work?

Cyril Cohen (Sep 03 2020 at 12:25):

Nop, it just means github does not read this attribute.

Cyril Cohen (Sep 03 2020 at 12:26):

cf
Cyril Cohen said:

FTR I just merged https://github.com/math-comp/math-comp/pull/551.

It does not solve conflicts on github yet (cf https://github.com/isaacs/github/issues/487 and https://github.com/isaacs/github/issues/560, so it's likely to be supported in the future, given gitlab does... hopefully).

However, locally, I tested it on a few git rebase that would conflict, and it does not anymore. :tada: :tada:

Théo Zimmermann (Sep 03 2020 at 12:37):

FTR, it's totally possible to grant a "rebase now" feature request. It's just that I'm trying to figure out why the .gitattributes option is not already used when doing the git merge. Is this supposed to work only when using git rebase? coqbot does the git merge on the comand-line.

Cyril Cohen (Sep 04 2020 at 15:31):

@Théo Zimmermann I think git merge reads it as well, but we should not dare to ask @coqbot to merge with a CI not running because github does not detect the spuriousness of the conflict.
The purpose of @coqbot: rebase now would be to rebase and trigger the CI again without having to checkout locally etc

Théo Zimmermann (Sep 04 2020 at 21:57):

OK. Please open an issue on https://github.com/coq/bot so that I remember to implement this.

Last updated: Jun 01 2023 at 11:01 UTC