Pierre-Marie Pédrot (Sep 03 2020 at 09:37): Pierre-Marie Pédrot (Sep 03 2020 at 09:37):Recently I've been seeing strange behaviours from the CI feedback on github.
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
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.
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.
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.
Pierre-Marie Pédrot (Sep 03 2020 at 09:39):Is this a known problem ? (@Théo Zimmermann ?)
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.
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.
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.
Hugo Herbelin (Sep 04 2020 at 19:08):Thanks!
Last updated: Jun 04 2023 at 19:30 UTC