Stream: Coq devs & plugin devs

Topic: coqbot should mention stale CI


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Apr 04 2022 at 16:37):

That however could become very annoying for people if we don't implement it well.

view this post on Zulip Gaëtan Gilbert (Apr 04 2022 at 17:12):

forcing a refresh could be very annoying too

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Apr 05 2022 at 07:14):

isn't it what bors is for?

view this post on Zulip Enrico Tassi (Apr 05 2022 at 07:15):

I mean, maybe there is a way for coqbot merge now to just call bors?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Théo Zimmermann (Apr 05 2022 at 08:56):

Though, we could do an experiment and see what happens.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Feb 05 2023 at 21:03 UTC