coq
Make coqbot workaround the GitHub→GitLab 30' lag for syncing the main branches?
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: https://github.com/coq-community/docker-coq/pull/50#issuecomment-1165749733
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 agoat 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:
- https://github.com/coq-community/docker-coq/pull/50
- https://github.com/coq/coq/pull/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?)
What about entirely disabling the mirroring for projects which choose to use coqbot for this task?
@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!
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.