@Théo Zimmermann How easy would it be to get coqbot to ask for a fresh CI before merging? Say one ran a few days ago?
Relatively easy I think. The most difficult part would be to decide what is a good threshold to define CI staleness. Also, we should provide a way of forcing a merge despite the staleness.
Relatively easy I think. The most difficult part would be to decide what is a good threshold to define CI staleness. Also, we should provide a way of forcing a merge despite the staleness.
A time threshold will never be perfect, since breaking changes can always be merged arbitrarily close together. I therefore think that a CI that finished 3 days ago probably wouldn't mind a refresher.
I think that the optimal solution (but also the one that will take the most effort to get right), would be a merge queue. That way coqbot would be in charge of checking each PR can be merged with no problems on the CI.
That however could become very annoying for people if we don't implement it well.
forcing a refresh could be very annoying too
I'd probably just go back to the merge script if the bot doesn't feel like merging
Gaëtan Gilbert said:
forcing a refresh could be very annoying too
That's also my fear.
Something that would be maybe a little more bearable and would take us one step closer to a merge queue would be a "Restart CI and merge" feature.
isn't it what bors is for?
I mean, maybe there is a way for coqbot merge now to just call bors?
Nowadays, you don't even need bors anymore for that. GitHub has implemented the merge queue feature directly.
coqbot uses GitHub merge button internally, so it could just as well use GitHub's merge queue.
However, my initial worry of using merge queues is still there. We frequently have to bypass red CI checks and if we cannot do that anymore, we're going to have a problem.
Though, we could do an experiment and see what happens.
At least we need a way to bypass the CI checks. Imagine a situation where master does not compile because of a remote change and we can't push anything into it, even to fix it...
Well, in theory there would always be the possibility of first pushing the change disabling the failing test, but yes, I agree that this is going to be problematic if there is no bypassing mechanism.
https://docs.github.com/en/pull-requests/collaborating-with-pull-requests/incorporating-changes-from-a-pull-request/merging-a-pull-request-with-a-merge-queue
apparently there is a button to override the protections
but I could not find a way to say "ignore that specific failure", but maybe that could be for coqbot? I mean coqbot merge after CI [ignore job1 jobn]
and coqbog merge now
to forcibly merge
We could ignore specific failures after running CI. But if we rely on the GitHub merge queue, then I don't think we can.
Last updated: Dec 07 2023 at 14:02 UTC