coqbot should not add "needs: full ci" after trivial rebase

[andres-erbsen]

coqbot should not add "needs: full ci" after trivial rebase. I've gotten used to gerrit allowing silent rebasing and it's so nice.

E.g. andres-erbsen force-pushed the ZModOffset branch from d02d498 to f98674d.

[SkySkimmer]

Not sure I agree.

Also how can coqbot recognize "trivial rebase"?

[JasonGross]

I think the simplest change to make here is that a force push should only cancel an existing full ci run when a new full ci run is started. A new lite CI should not cancel an existing full CI.

A more involved criterion might be that a rebase is trivial if the generated coq binaries and compiled OCaml libraries are either all identical to the base of the PR or all identical to the pre-rebase state; and also all .vo files of the prelude / standard library are either all identical to the base of the PR or all identical to the pre-rebase state; and also that no development on the CI failed on the PR without a corresponding failure on both current master and the previous PR base.

[SkySkimmer]

I think the simplest change to make here is that a force push should only cancel an existing full ci run when a new full ci run is started. A new lite CI should not cancel an existing full CI.

That sounds very risky, a force push can change anything.

A more involved criterion might be that a rebase is trivial if the generated coq binaries and compiled OCaml libraries are either all identical to the base of the PR or all identical to the pre-rebase state; and also all .vo files of the prelude / standard library are either all identical to the base of the PR or all identical to the pre-rebase state; and also that no development on the CI failed on the PR without a corresponding failure on both current master and the previous PR base.

That's not going to happen in the vast majority of cases so it's a waste of time trying to implement it.

[JasonGross]

That sounds very risky, a force push can change anything.

It's not risky. A force push will still add "needs: full ci" and will still start a fresh lite CI. Perhaps coqbot can comment with the link to the existing/previous full CI run in progress. It is up to the devs what to do with that.

[andres-erbsen]

https://gerrit-review.googlesource.com/Documentation/config-labels.html

A new patch set is considered to be trivial rebase if the commit message is the same as in the previous patch set and if it has the same diff (including context lines) as the previous patch set. This is the case if the change was rebased onto a different parent and that rebase did not require git to perform any conflict resolution, or if the parent did not change at all (aka the change kind of the commit is NO_CHANGE).

This predicate can be used to enable sticky approvals, reducing turn-around for trivial rebases prior to submitting a change.

For the pre-installed Code-Review label this predicate is used by default.

[SkySkimmer]

That sounds reasonable

[Zimmi48]

If we were to implement this, we should keep in mind that the previous full CI before the force-push may not have been fully green and this won't be visible anymore as GitHub will remove the link to the previous pipeline.
So we should either figure a way to still show the CI results of the previous pipeline, or only skip the needs: full ci label in case the previous pipeline was fully green (and the rebase is trivial).