Make coqbot workaround the GitHub→GitLab 30' lag for syncing the main branches?

[erikmd]

Context

I remember discussing this issue a long time ago with @Zimmi48 and it seemed "minor" (and/or not essential for maintaining coq/coq), but it actually appeared blocking to me since this comment: rocq-community/docker-coq#50 (comment)

Cc @Alizter @JasonGross also FYI

Current behavior

• coqbot is extremely nice for syncing GitHub PR branches → GitLab branches named pr-*

• However when a repository such as https://github.com/coq-community/docker-coq strongly relies on continuous deployment at merge time in the default branch, it is very annoying to face with this "documented sync lag" pull_mirror_interval_seconds.

• Namely, the repository is automatically synced only every 30' (it is easy to notice this by monitoring the text Successfully updated N minutes ago at URL https://gitlab.com/coq-community/docker-coq/-/branches)

• Furthermore, a manual sync is only possible every 5' as documented here:
  https://docs.gitlab.com/ee/user/project/repository/mirror/#update-a-mirror

Expected behavior

It would be nice if coqbot can automatically push the default branch (e.g. master or main or a set of user-specified branches) to GitLab as soon as it detects a push to this/these branches in GitHub.

As a result, with this feature, these two PRs could be merged quasi-simultaneously in this order:

1. feat: Adapt to https://github.com/coq/coq/pull/15560 rocq-community/docker-coq#50
2. [build] Consolidation of build system infrastructure rocq#15560

Misc notes

Regarding the potential "risk" that should be tested:

• If coqbot can push master from github to gilab before the automatic mirroring, one should check that this bot push won't prevent the upcoming, automatic mirroring of (all other) branches.
• but I guess this shouldn't occur if coqbot only dooes fast-forward pushes of that branch (unlike pushes to pr-* that are typically done with --force)
• (and… what would happen if coqbot's push and gitlab's auto-sync are almost simultaneous?)

[Zimmi48]

What about entirely disabling the mirroring for projects which choose to use coqbot for this task?

[erikmd]

@Zimmi48

What about entirely disabling the mirroring for projects which choose to use coqbot for this task?

Yes of course, if coqbot could perform the "fast-forward push mirroring of all branches" itself, why not indeed!

[Zimmi48]

This should be easy to implement because all the bricks are already available. We should probably add a configuration parameter mirror = true in coqbot.toml to activate the feature, document that users should disable GitLab's own mirroring feature when activating this one, and tweak the pushing function to do a fast-forward push instead of a force-push.

[erikmd]

OK @Zimmi48, looks great !