Stream: Coq devs & plugin devs

Topic: coqbot behaving strangely?


view this post on Zulip Pierre-Marie Pédrot (Sep 03 2020 at 09:37):

Recently I've been seeing strange behaviours from the CI feedback on github.

view this post on Zulip Pierre-Marie Pédrot (Sep 03 2020 at 09:37):

Sometimes it doesn't update properly, e.g. https://github.com/coq/coq/pull/12973

view this post on Zulip Pierre-Marie Pédrot (Sep 03 2020 at 09:38):

This PR still displays as a failure although the CI was restarted and successfully finished.

view this post on Zulip Pierre-Marie Pédrot (Sep 03 2020 at 09:38):

Dunno if related, but the UI also changed since it requires two clicks to get to the gitlab page.

view this post on Zulip Pierre-Marie Pédrot (Sep 03 2020 at 09:39):

Clicking on the job from Github used to lead directly to the gitlab page, but now it first goes through some github-specific info page.

view this post on Zulip Pierre-Marie Pédrot (Sep 03 2020 at 09:39):

Is this a known problem ? (@Théo Zimmermann ?)

view this post on Zulip Hugo Herbelin (Sep 03 2020 at 09:50):

Same here: https://github.com/coq/coq/pull/12949 and https://github.com/coq/coq/pull/12946, but after having restarted manually failing gitlab jobs. The gitlab page says that the CI is ok but the PR page still reports failures.

view this post on Zulip Théo Zimmermann (Sep 03 2020 at 10:21):

Regarding:

Dunno if related, but the UI also changed since it requires two clicks to get to the gitlab page.

See: https://coq.zulipchat.com/#narrow/stream/243318-coqbot-devs.20.26.20users/topic/Checks
The problem observed by @Hugo Herbelin on PR #12949 is also due to this.

The other two (#12973 and #12946), I'll look into them.

view this post on Zulip Théo Zimmermann (Sep 03 2020 at 19:30):

I've fixed some issue related to retried jobs. Let me know if you spot any new occurrence.

view this post on Zulip Hugo Herbelin (Sep 04 2020 at 19:08):

Thanks!


Last updated: Oct 16 2021 at 02:03 UTC