coqbot can show light pipeline as cancelled when full pipeline is running.

[Zimmi48]

Calling the @coqbot run full CI now command may lead to the GitLab pipeline appearing like this while the full pipeline is running:

This is due to GitLab having sent the "pending" and "running" webhooks before the "cancelled" event for the previous pipeline. coqbot treats each of these events independently and doesn't check that the "cancelled" event corresponds to what is currently displayed as the running pipeline (and even if it did, the two events could be treated asynchronously, resulting in a race condition leading to the same result).

[SkySkimmer]

Is there a way to tell that the cancelled pipeline is not the most recent for that branch? In which case we would not forward the even to github.

[Zimmi48]

That may not be the simplest way to do this, but something we could consider is:

• create a GitLab pipeline on GitHub Checks as soon as we have pushed to GitLab (or even just before pushing to guarantee that it will be there first)
• attach an "external ID" to this pipeline which corresponds to the pushed merge commit (which will uniquely identify the pipeline)
• when a pipeline event is received from GitLab, check what is the external ID of the current GitHub Check and ignore if it doesn't match.

I remember that we are already using external IDs somewhere, so we would have to check if this is compatible. But external IDs are arbitrary strings, so we could pack two or more values in a single string if necessary.

I won't have time to look into implementing this myself before a few months, so anyone else is welcome to take this.