Feature: check PRs for merge conflicts about bot

[ejgallego]

Maybe this is the right time to introduce an async queue in the bot? You could trigger the check event at every push to master, but indeed place it in a work queue with delay. This way the timer is not associated to the event.

Even better would be for the both to have access to the trees [and maybe run git by itself], but that looks more complicated.

[ejgallego]

One further advantage of having a queue is that newer jobs can cancel / override older ones.

[by the way, such kind of queue is what's needed for asyncronous proof processing :D]

[Zimmi48]

The bot runs git already to be able to push to GitLab so we could indeed check locally for the conflicts, but this would require pulling all PRs, so it seems more sensible to use the info already computed by GitHub...

[Zimmi48]

An async queue would be something like what is provided by https://github.com/c-cube/lwt-pipe?

[ejgallego]

An async queue would be something like what is provided by https://github.com/c-cube/lwt-pipe?

Indeed, I think so !

[Zimmi48]

In the end, this was implemented by using an external Action.