Ali Caglayan (Apr 04 2022 at 16:01): Ali Caglayan (Apr 04 2022 at 16:01):@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?
Théo Zimmermann (Apr 04 2022 at 16:34):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.
Théo Zimmermann (Apr 04 2022 at 16:34):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.
Ali Caglayan (Apr 04 2022 at 16:37):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.
Ali Caglayan (Apr 04 2022 at 16:37):That however could become very annoying for people if we don't implement it well.
Gaëtan Gilbert (Apr 04 2022 at 17:12):forcing a refresh could be very annoying too
Gaëtan Gilbert (Apr 04 2022 at 17:12):I'd probably just go back to the merge script if the bot doesn't feel like merging
Théo Zimmermann (Apr 05 2022 at 07:12):Gaëtan Gilbert said:
forcing a refresh could be very annoying too
That's also my fear.
Théo Zimmermann (Apr 05 2022 at 07:13):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.
Enrico Tassi (Apr 05 2022 at 07:14):isn't it what bors is for?
Enrico Tassi (Apr 05 2022 at 07:15):I mean, maybe there is a way for coqbot merge now to just call bors?
Théo Zimmermann (Apr 05 2022 at 08:54):Nowadays, you don't even need bors anymore for that. GitHub has implemented the merge queue feature directly.
Théo Zimmermann (Apr 05 2022 at 08:55):coqbot uses GitHub merge button internally, so it could just as well use GitHub's merge queue.
Théo Zimmermann (Apr 05 2022 at 08:56):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.
Théo Zimmermann (Apr 05 2022 at 08:56):Though, we could do an experiment and see what happens.
Pierre-Marie Pédrot (Apr 05 2022 at 09:06):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...
Théo Zimmermann (Apr 05 2022 at 09:08):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.
Enrico Tassi (Apr 05 2022 at 11:08):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
Enrico Tassi (Apr 05 2022 at 11:17):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
Théo Zimmermann (Apr 05 2022 at 12:20):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: May 28 2023 at 13:30 UTC