Stream: CUDW 2020

Topic: Gitlab Ci for coq/coq: How to win lottery?


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

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

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

view this post on Zulip Fabian Kunze (Dec 02 2020 at 13:33):

or is a quota reached and there is no money left?

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

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:38):

There is some silly bug, and if you cancel + restart the pipeline is actually run.

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

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

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:38):

sudo gitlab run pipeline

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

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

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

view this post on Zulip Fabian Kunze (Dec 02 2020 at 13:41):

thanks, I called the repo "upstream" to avoid those things :)

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:42):

@Théo Zimmermann does osx CI save the test suite logs?

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:42):

as we do on unix?

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 13:42):

Not as artifacts, no. But it prints them out in the log IIRC.

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:42):

I have a silly failure, grep related, here: https://github.com/coq/coq/pull/13523/files

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

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:43):

@Fabian Kunze what was the drill about grep then?

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

view this post on Zulip Fabian Kunze (Dec 02 2020 at 13:43):

i changed that

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

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:44):

ok, good for you. here I'm still lost

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 13:44):

I often do restart pipelines from other people.

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 13:45):

And I'm not the only one.

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:45):

I do restart all the ones I see stuck

view this post on Zulip Théo Zimmermann (Dec 02 2020 at 13:45):

And pipelines do get started automatically when activity levels are not so high of course.

view this post on Zulip Enrico Tassi (Dec 02 2020 at 13:45):

bein doing that for the last 2 weeks (release frenziness)

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

view this post on Zulip 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: Apr 19 2024 at 17:02 UTC