Fabian Kunze (Dec 02 2020 at 13:27): Fabian Kunze (Dec 02 2020 at 13:27):It seems that gitlab ci does not start on my PRs to coq/coq or intermediate PR commits.
Also, I'm not able to restart it from the GUI. I see a cancel button, but it fails.
(An example is this pipeline: https://gitlab.com/coq/coq/-/pipelines/224243299 )
-In the short term: could someone start this pipeline and explain to me how I can distinguish between a real fail and me just loosing in will-my-pipeline-start-lottery? It's quite frustrating.
-In the long term: Is there a way to improve the experience when opening PRs so that Icontributors do not have to guess if my PR is really broken or CI on gitlab did just not run properly?
Guillaume Melquiond (Dec 02 2020 at 13:29):Look at the red flag. It states "pipeline job activity limit exceeded". There is nothing you can do right now. No point in restarting it, because the limit will still be exceeded.
Fabian Kunze (Dec 02 2020 at 13:31):Do I need to intervene at some point or is it scheduled to start once space is free?
Fabian Kunze (Dec 02 2020 at 13:33):or is a quota reached and there is no money left?
Guillaume Melquiond (Dec 02 2020 at 13:33):I never had to restart to it, so I tend to think it is the latter, i.e., auto start.
Enrico Tassi (Dec 02 2020 at 13:38):There is some silly bug, and if you cancel + restart the pipeline is actually run.
Théo Zimmermann (Dec 02 2020 at 13:38):No point in restarting it, because the limit will still be exceeded.
That's actually not true, probably due to a GitLab bug.
Théo Zimmermann (Dec 02 2020 at 13:38):As Enrico said, you can do the cancel + restart danse on GitLab (but for this you need to have the access right in the GitLab org).
Enrico Tassi (Dec 02 2020 at 13:38):sudo gitlab run pipeline
Théo Zimmermann (Dec 02 2020 at 13:38):Or you can click on "Re-run" in the GitHub Checks tab (for this you only need to have write access in the GitHub repo).
Théo Zimmermann (Dec 02 2020 at 13:40):@Fabian Kunze I have just invited you to join our @coq/contributors team, which means that as soon as you accept the invitation, you will have write-access in the GitHub repo.
Théo Zimmermann (Dec 02 2020 at 13:40):The usual warnings: while our main branches are protected, there is nothing preventing you to push a branch to the repo now. Please don't do it. Be careful to always push branches to your fork.
Fabian Kunze (Dec 02 2020 at 13:41):thanks, I called the repo "upstream" to avoid those things :)
Enrico Tassi (Dec 02 2020 at 13:42):@Théo Zimmermann does osx CI save the test suite logs?
Enrico Tassi (Dec 02 2020 at 13:42):as we do on unix?
Théo Zimmermann (Dec 02 2020 at 13:42):Not as artifacts, no. But it prints them out in the log IIRC.
Enrico Tassi (Dec 02 2020 at 13:42):I have a silly failure, grep related, here: https://github.com/coq/coq/pull/13523/files
Théo Zimmermann (Dec 02 2020 at 13:42):Fabian Kunze said:
thanks, I called the repo "upstream" to avoid those things :smile:
Good strategy (this is mine too)!
Enrico Tassi (Dec 02 2020 at 13:43):@Fabian Kunze what was the drill about grep then?
Fabian Kunze (Dec 02 2020 at 13:43):it was not grep, but it was that i depended on make-internals regarding the order of recipes. (and on mac, they where resolved in another order)
Fabian Kunze (Dec 02 2020 at 13:43):i changed that
Guillaume Melquiond (Dec 02 2020 at 13:44):So, which is it? Does the pipeline start automatically? Or is there a good samaritan who always restarts mine?
Enrico Tassi (Dec 02 2020 at 13:44):ok, good for you. here I'm still lost
Théo Zimmermann (Dec 02 2020 at 13:44):I often do restart pipelines from other people.
Théo Zimmermann (Dec 02 2020 at 13:45):And I'm not the only one.
Enrico Tassi (Dec 02 2020 at 13:45):I do restart all the ones I see stuck
Théo Zimmermann (Dec 02 2020 at 13:45):And pipelines do get started automatically when activity levels are not so high of course.
Enrico Tassi (Dec 02 2020 at 13:45):bein doing that for the last 2 weeks (release frenziness)
Théo Zimmermann (Dec 02 2020 at 13:46):I'll try to find some time to have coqbot automatically cancel outdated pipelines and restart the ones that get stuck.
Théo Zimmermann (Dec 02 2020 at 13:47):I'm reluctant to do the latter without the former, because if we go well over the limit, it's likely to become suspicious to GitLab.
Last updated: Jun 11 2023 at 00:30 UTC