race condition when PRs are closed (almost) simultaneously

[jcommelin]

Over at leanprover-community/mathlib we use the bors bot (bors-ng) to merge PRs for us. (CI takes > 1 hour, and we have 10 - 20 PRs per day, so we need some sort of way to run CI on multiple PRs at once.)

If several PRs are marked as ready-to-merge, and the simultaneously pass the CI test, then bors will merge all of them into master and close the PRs.

However, if PR X depends on Y and Z, and both Y and Z are in the same batch that bors is closing, this seems to cause a race condition for sync-task-issues.

See the edit history of the top post of the following PR for an example:
leanprover-community/mathlib3#4268

[jonabc]

ah, yeah I see what you're saying. I'm not sure up front of the best way to solve this due to separate runs of the action not knowing about each other. If you have any suggestions I'm happy to hear them, otherwise I'm going to have to think about this.

Maybe adding a random-ish small sleep in the action would work around this?

- run: sleep $((1 + RANDOM % 5))

[jcommelin]

I guess such a sleep might solve 99% of the problems 👍

I don't know enough of how github actions work, and what data is available when one of them runs, but suppose that we are in the scenario that I sketched above. X depends on Y and Z, and at some point Y and Z are both closed. Then we get some race, and suppose that Z wins by a tiny margin, and it checks off the dependency on Z, a little while later Y is running, and it wants to check off Y. Can that action also check the status of all other dependencies that are mentioned in that post? Because then Y would also see that Z has been closed, and check off Z again (which is not a problem).

Anyway, I think the small sleep is a pragmatic solution, so that would be great!